What is PoP?

Pi Squared's Proof of Proof Tool

Simply put, Pi Squared denotes Zero-Knowledge proofs (ZKPs) of mathematical proofs.

Initially, computational claims are processed by appropriate K tools, generating mathematical proofs that attest to their absolute correctness. Although these mathematical proofs can be too large to act as certificates of correctness for computational claims, they can be locally verified by a small, universal proof checker that yields ZKPs, or in other words, ZKPs of mathematical proofs. Thus, Pi Squared embodies the concept of Proof of Proof.

Given that computational claims may specifically include program execution claims, Pi Squared proposes a unique strategy for verifiable computing. This is achieved by simply using the K execution tool, KRun, to generate the mathematical proofs for program execution. Moreover, as computational claims can also consist of property correctness claims, Pi Squared offers an exclusive approach to formal verification. This is done by merely employing the K formal verification tool, KProve, to generate the mathematical proofs for formal verification. Additionally, Pi Squared can generate ZKPs, making it the first and ultimate Universal Settlement Layer.

As a Universal Settlement Layer, Pi Squared is applicable to all execution and DA systems across all platforms. Pi Squared is both language and Virtual Machine (VM)-agnostic because it produces ZKPs for mathematical proofs that are directly founded on the formal semantics of programming languages and/or VMs. Consequently, Pi Squared is compatible with any execution environment and aligns with any execution layers or consensus/DA layers.

Our core technology is grounded in more than 50 years of research on formal semantics, which is unfortunately overlooked by the current verifiable computing practices. Just like TCP/IP enables the Internet, Pi Squared and its core, a small universal mathematical proof checker, paves the way for the second generation of verifiable computing, Verifiable Computing 2.0. In this environment, languages and VMs are integrated into a universal computing space with full interoperability; the trust base of verifiable computing correctness certificates is minimized; the need for notoriously faulty traditional language implementations such as compilers, transpilers, or interpreters is entirely eliminated; and maintaining language changes/updates become as simple as plug-and-play.

• Check out the Performance Benchmarking number

• Read the Pi Squared paper: Matching Logic Proofs Meet Succinct Cryptographic Proofs