Core technologies
Last updated
Was this helpful?
Last updated
Was this helpful?
Proof of Proof is built upon three core technologies:
Core technologies behind Proof of Proof
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.
Formal semantics and the K framework
Learn how it provides a rigorous way to define programming languages, capturing the precise meaning of programs.
Matching logic
Understand the logical foundation that allows us to translate program executions into mathematical proofs.
Zero-knowledge proofs and zkVMs
Explore the cryptographic tools that enable us to compress and efficiently verify the mathematical proofs.