What is Proof of Proof?
Last updated
Last updated
TL;DR: Proof of Proof turns any program execution into a mathematical proof, and then turns that into a zero-knowledge proof. It’s language-agnostic, verifiable by design, and compatible with all major zkVMs.
Proof of Proof is Pi Squared’s verifiable computing framework that enables correct-by-construction proofs for any program, written in any programming language, running on any virtual machine or instruction set.
It provides a clean separation of concerns across three core pillars:
The Proof of Proof system allows us to transform any valid execution trace of a program into a verifiable mathematical proof, and then into a succinct, cryptographic zero-knowledge proof. This makes it not only secure but also efficient.
Below is a simplified breakdown of how Proof of Proof works under the hood:
Define the language (once)
Run the program and capture its behavior
The K framework runs the program and emits an execution trace—a record of how it transitioned from start to finish.
Generate a mathematical proof
Using matching logic and the K-defined semantics, we automatically construct a machine-checkable proof that validates this execution.
Compress that proof with zero-knowledge
The math proof is too large for practical use, so we compress it into a zero-knowledge proof using zkVMs like RISC Zero or SP1. This ZK proof basically says: “There exists a valid math proof of this execution”—without revealing the proof itself.
Verify it anywhere
The zero-knowledge proof can be verified on-chain, in a decentralized system, or by anyone, quickly and independently.
To better understand each stage, it's important to first review the fundamental technologies that underpin Proof of Proof.
Most programs are written in languages like JavaScript, Rust, or Solidity, but how do we describe what those programs actually mean in a rigorous way?
That’s where formal semantics comes in. It gives us a precise, mathematical definition of a programming language. Instead of relying on a human-readable spec or an ad hoc compiler behavior, formal semantics tells us exactly how every construct in a language behaves.
The K framework is the backbone of this idea. It's a meta-language, which simply means it’s a language used to define other languages. You can define the full syntax and behavior of any programming language in K, and it will automatically generate a list of tools including an interpreter, a symbolic execution engine, a proof generator, etc.
Once a language is defined in K, it can plug directly into the Proof of Proof pipeline, no matter if it’s C, Python, EVM, or something new.
Underneath the K framework lies a formal logic called matching logic. It’s the system that allows us to turn computation into math.
In simpler terms, this means:
Every programming language defined in K becomes a PL math theory in matching logic.
Every execution of a program becomes a claim—a logical statement that says, “Starting from state A, the program ends in state B.”
Proof of Proof uses a fixed set of logical rules to generate a mathematical proof that this claim is valid.
This is the first big leap: transforming arbitrary code into something math can reason about. Importantly, matching logic is expressive enough to handle all languages and paradigms, yet its core checker is just a few hundred lines of code.
Math proofs are great for correctness, but they’re often too large or detailed to be practical. That’s where zero-knowledge (ZK) proofs come in.
With ZK cryptography, we can compress those large mathematical proofs into short, verifiable statements. Instead of checking the whole proof, you verify a small ZK proof that proves that a proof exists.
Proof of Proof supports multiple ZK systems, such as SNARKs, STARKs and zkVMs like RISC Zero, SP1, and others.
These systems act like virtual machines that run in zero-knowledge. You write or define a computation, and the zkVM outputs a cryptographic proof that it ran the computation correctly without revealing the computation itself.
By translating our math proofs into ZK-compatible circuits, we unlock scalability, privacy, and decentralized verification which are all critical components for any trustless system.
We coined the term Proof of Proof to reflect the layered nature of what we’re building.
In most ZK systems, the focus is on proving that a computation happened correctly. But Proof of Proof goes a level deeper. It starts by generating a mathematical proof of a program’s execution, then uses cryptography to produce a ZK proof of that proof.
That’s where the name comes from: it’s a zero-knowledge proof of a mathematical proof.
This layered structure gives us stronger guarantees that:
The mathematical proof is human-readable and machine-checkable.
The ZK proof is succinct, private, and verifiable by anyone.
By separating computation, proof generation, and cryptographic compression, we get correctness by design, scalability, and language-independence—all in one.
Every programming language is first defined using formal semantics in the. This tells us what it means for any program in that language to execute correctly.
