Architecture

In this guide, we look more closely at the architecture of Proof of Proof and how it works end-to-end.

Below is a simplified breakdown of how Proof of Proof works under the hood:

1

Define the formal semantics (once)

Use the K framework to define the formal semantics of the programming language, virtual machine, or instruction set architecture. This formal definition describes how every program in the language should behave. It only needs to be created once for each language.

2

Execute the program and obtain the computing result

Run the program using the K framework. This produces the output of the computation, along with detailed logs that show how the formal semantics guided each step of the execution.

3

Generate a mathematical proof

Using the execution logs (called a proof hint) and the formal semantics, generate a full mathematical proof that confirms the result is correct. This proof is complete, rigorous, and can be automatically verified by a small tool called the math proof checker.

4

Generate a zero-knowledge proof

Feed the math proof into a math proof checker, then use that process to create a zero-knowledge proof. This ZKP proves that a valid math proof exists without revealing the proof itself. Since ZKPs are typically much smaller than full math proofs, this step essentially compresses the original proof.

5

Verify proofs anywhere

Both the math proof and the ZKP can be independently verified by anyone. Each acts as a verifiable certificate that confirms the correctness of the original computation.

The trade-off here is the classic one between time and space:

• Math proofs are quicker to generate but take up more space.

• ZKPs are smaller but take more time to generate.

Regardless of which one you use, both provide strong guarantees of correctness and can be verified anywhere.

The final certificate of the Proof of Proof workflow is a ZKP that shows the existence of a math proof, which in turn shows the correctness of the computing result.

Now, let us look more closely at the architecture and workflow of Proof of Proof from the beginning to the end, illustrated by the figure below.

Figure 1: The Proof of Proof workflow

The above architecture and workflow can be understood by looking at its three main components and phases, represented as three large boxes. We elaborate on each of them below.

K and proof hint generation

The first component and phase of Proof of Proof involves an enhanced version of the K framework. This instrumented version is used to execute any program based on the formal semantics of its programming language. During this phase, three key outputs are produced:

1

Computing result

This is the result of running the program using the K framework. It's the same output you would expect from executing the program normally, but it's generated by strictly following the formal semantics defined in K.

2

Mathematical theory of the programming language

Every programming language used with Proof of Proof must have its formal semantics defined in K. This formal semantics serves as a mathematical theory of the language. It completely and rigorously describes how all programs written in that language should behave.

Think of this formal semantics as similar in spirit to foundational mathematical systems like Peano arithmetic or Zermelo–Fraenkel set theory.

• The K framework uses this mathematical theory to simulate program execution.

• Proof of Proof uses the same theory to generate verifiable certificates that prove the correctness of the computation.

3

Math proof hint (execution trace)

As the K framework runs the program, it produces detailed logs known as the math proof hint. These logs are critical because they trace exactly how the program transitions from one state (or configuration) to the next.

In K, a formal semantics consists of rewrite rules—these rules define how one configuration is transformed into another. The math proof hint captures this entire execution trace by:

• Recording each step in the sequence of configuration transitions

• Linking every step back to the specific rewrite rule in the formal semantics that caused it

This trace forms the foundation for constructing a full mathematical proof in the next phase.

At the end of this phase, three deliverables are passed on to the next step:

• The computing result

• The mathematical theory (formal semantics) of the programming language

• The math proof hint (execution trace)

These form the input for the next phase, where a complete and verifiable mathematical proof is automatically generated.

Math proof generation

The second phase of Proof of Proof is focused on generating a complete mathematical proof that confirms the correctness of the program’s execution.

1

Create sub-proofs for each step

During this phase, Proof of Proof takes the execution trace from K and generates a sub-proof for each individual transition between configurations. Each transition is one step that K performed when executing the program.

2

Merge into a final proof

All of these sub-proofs are then merged into a single, comprehensive math proof. This final proof shows, step by step, how the program execution follows logically from the formal semantics of the programming language.

3

Use Matching Logic and Proof Calculus

The math proofs are built using a fixed system called the Proof Calculus, which is based on a formal logic known as matching logic.

• This system provides a consistent method for constructing and verifying proofs.

• All math proofs built using this calculus can be checked in the same way—by validating that each proof step follows the rules defined by the Proof Calculus.

4

Verify with the math proof checker

To verify a proof, a tool called the math proof checker is used. This is an implementation of the verification algorithm defined by the Proof Calculus. It checks that every step in the proof is valid.

Deliverable of this phase The main output here is the math proof, which is a detailed, step-by-step derivation of the computing result, built directly from the formal semantics of the programming language.

One of the key strengths of this approach is that it reduces the trust base to an absolute minimum.

What you must trust:

• The formal semantics of the programming language (defined in K)

• The math proof checker (which verifies the proof steps)

What you don’t need to trust:

• The math proof itself (it’s automatically checked)

• The proof generation process (including K), since they are only used to discover the proof, not verify it

In this setup, K acts as a proof searcher, not a source of truth. The correctness of the result relies solely on the formal semantics and the math proof checker.

Zero-knowledge proof generation

The third phase of Proof of Proof is about generating zero-knowledge proofs (ZKPs). These proofs confirm that a valid math proof exists, without revealing the proof itself.

There are three key components involved in this process:

• PI: the math proof

• mpc: the math proof checker

• pi: the zero-knowledge proof

These components are related in the following way:

1

PI is valid if and only if mpc(PI) = accept

This means the math proof is correct if the math proof checker accepts it. This is an absolute guarantee.

2

pi is valid if and only if PI is valid, with a negligibly small chance of error

In other words, the ZK proof pi is convincing evidence that PIis valid. While not absolute like (1), the error probability is extremely low in practice.

Proof of Proof is a flexible framework. It allows customization in:

• How the math proof PI is serialized and formatted

• How the math proof checker mpc is implemented

• How the ZK proof pi is generated

To illustrate this, two independent workflows are supported:

1

Using any existing zkVM

• You can choose a standard format for encoding math proofs, such as Metamath.

• You implement the math proof checker (mpc) inside a zkVM.

• In this setup:

  • The public input to the zkVM is the part of PI that defines the formal semantics and the computing result.

  • The private witness is the part of PI that contains the detailed proof steps from the Proof Calculus.

This separation between math proof generation and ZK proof generation allows for semantic and mathematical optimizations before ZK-specific constraints come into play.

2

Using a specialized circuit: The Block Model

• For more efficiency, we designed the Block Model, a specialized approach for organizing and verifying math proofs.

• In the Block Model:

  • The math proof is divided into independent blocks.

  • Each block contains a set of premises and conclusions.

  • This allows for parallel and independent processing of blocks.

The Block Model is highly compatible with circuit-based ZK systems and enables:

• Efficient folding of ZKPs

• Effective batching of multiple proofs

By supporting both general-purpose zkVMs and optimized circuits like the Block Model, Proof of Proof offers a powerful and adaptable approach to verifiable computation.