ZK Proof Generation
Once a mathematical proof of a program's behavior has been generated and verified, the next step is to turn that proof into a zero-knowledge (ZK) proof. This section covers two approaches we use to generate ZK proofs for verified executions:
By running the proof checker inside a zkVM
By compiling the proof into a custom circuit using our block model (BM)
Each method comes with its own trade-offs in terms of performance, flexibility, and implementation complexity.
Generating ZK Proofs with zkVMs
A zkVM is a virtual machine that can produce ZK proofs for arbitrary programs. By compiling our proof checker to run inside a zkVM, we can reuse its infrastructure to generate ZK proofs of verified program execution with minimal changes to our workflow.
In this setup:
The proof checker is written as a guest program and runs inside the zkVM.
The zkVM proves that the proof checker correctly validates a given mathematical proof (e.g., a Metamath or block model proof).
This results in a succinct and verifiable certificate attesting to the correctness of the program's execution.
We’ve implemented this in several zkVMs, including Risc Zero, SP1, zkWASM, Jolt, Cairo, Lurk, and Nexus. For zkVMs with shared language support (like Rust), we used a common library to keep the checker consistent across platforms.
Benefits
Portable across many zkVMs.
Great for rapid prototyping and proof-of-concept implementations.
Supports arbitrary programs written in high-level languages.
Limitations
zkVMs introduce overhead due to general-purpose memory models and instruction tracking.
For large proofs, memory usage and runtime can become bottlenecks.
Proof generation time can take minutes for simple programs and even longer for complex ones.
Generating ZK Proofs using Block Model (BM) Circuits
To maximize efficiency, we also offer a more specialized path: compiling mathematical proofs directly into zero-knowledge circuits using a format we call the block model.
In the block model:
Proofs are organized into a set of independent blocks.
Each block has a set of premises and conclusions.
A block is valid if all its premises are satisfied by conclusions from other blocks.
This structure is unordered and data-parallel, meaning we can verify each block independently and in any order. This makes it highly compatible with circuit-based ZK systems and enables efficient folding and batching of proofs.
We implemented this using techniques from modern SNARK and STARK systems, converting blocks into arithmetic circuits (e.g., R1CS or AIR). Each block rule is turned into a subcircuit, and large proofs are split into segments and folded recursively into a single succinct proof.
Benefits
Offers up to 1400× speedup compared to zkVM-based proof generation.
No overhead from virtual machines, memory models, or instruction sequencing.
Ideal for large proofs and production-scale deployments.
Trade-offs
Requires custom circuit design and tuning.
Less flexible than zkVMs for arbitrary code execution.
Comparison
Approach
Best For
Performance
Setup Complexity
zkVM-based
Fast iteration, high flexibility
Medium
Low
Block model circuits
High-performance, large-scale ZK applications
High
Medium–High
Last updated
Was this helpful?