# 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

Last updated