Simply put, Pi Squared means ZK proofs of mathematical proofs.

Computational claims are first handled by appropriate K tools, resulting in mathematical proofs that attest to their absolute correctness. While mathematical proofs can be too large to serve as correctness certificates for computational claims, they can be locally checked by a small, universal proof checker that produces ZK proofs; that is, ZK proofs of mathematical proofs. Pi Squared = Proof of Proof.

Since computational claims can be in particular program execution claims, Pi Squared presents a unique approach toward verifiable computing, by simply invoking the K execution tool KRun (see the diagram above) to generate the mathematical proofs for program execution. Since computational claims can also be in particular property correctness claims, Pi Squared presents a unique approach toward formal verification, by simply invoking the K formal verification tool KProve to generate the mathematical proofs for formal verification. But, Pi Squared can additionally generate ZK proofs, which makes it the first and ultimate Universal Settlement Layer.

Pi Squared, as a Universal Settlement Layer, will apply to all execution and DA systems across all platforms. Pi Squared is language and VM-agnostic because it produces ZK proofs for mathematical proofs that are directly based on the formal semantics of programming languages and/or VMs. As a result, Pi Squared works for any execution environment and is compatible with any execution layers or consensus/DA layers. Our core technology is based on 50+ years of study on formal semantics that is sadly ignored by the current verifiable computing practices. Just as TCP/IP is the enabler of the Internet, Pi Squared and its core, small, universal mathematical proof checker is the enabler for the second-generation verifiable computing, Verifiable Computing 2.0, where languages and VMs are integrated into a universal computing space with full interoperability; where the trust base of the verifiable-computing correctness certificates is reduced to an absolute minimum; where the need for traditional yet notoriously buggy language implementations such as compilers, transpilers, or interpreters is completely eliminated; and where maintaining language changes/updates is as easy as plug-and-play.