# Architecture
Below is a simplified breakdown of how Proof of Proof works under the hood:
{% stepper %}
{% step %}
**Define the formal semantics (once)**
Use the [K framework ](broken://pages/1e2ZKnPRUbe59ixbIjz0)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.
{% endstep %}
{% step %}
**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.
{% endstep %}
{% step %}
**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.
{% endstep %}
{% step %}
**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.
{% endstep %}
{% step %}
**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.
{% endstep %}
{% endstepper %}
{% hint style="info" %}
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.
{% endhint %}
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:
{% stepper %}
{% step %}
**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.
{% endstep %}
{% step %}
**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.
{% endstep %}
{% step %}
**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.
{% endstep %}
{% endstepper %}
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.
{% stepper %}
{% step %}
**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.
{% endstep %}
{% step %}
**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.
{% endstep %}
{% step %}
**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.
{% endstep %}
{% step %}
**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.
{% endstep %}
{% endstepper %}
**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.
{% hint style="success" %}
What you **must** trust:
* The **formal semantics** of the programming language (defined in K)
* The **math proof checker** (which verifies the proof steps)
{% endhint %}
{% hint style="danger" %}
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
{% endhint %}
> 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:
{% stepper %}
{% step %}
**`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.
{% endstep %}
{% step %}
**`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 `PI`is valid. While not absolute like (1), the error probability is extremely low in practice.
{% endstep %}
{% endstepper %}
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:
{% stepper %}
{% step %}
**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.
{% endstep %}
{% step %}
**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
{% endstep %}
{% endstepper %}
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.
---
# Agent Instructions: Querying This Documentation
If you need additional information that is not directly available in this page, you can query the documentation dynamically by asking a question.
Perform an HTTP GET request on the current page URL with the `ask` query parameter:
```
GET https://docs.fast.xyz/proof-of-proof-archived/architecture.md?ask=
```
The question should be specific, self-contained, and written in natural language.
The response will contain a direct answer to the question and relevant excerpts and sources from the documentation.
Use this mechanism when the answer is not explicitly present in the current page, you need clarification or additional context, or you want to retrieve related documentation sections.