Pi Squared
HomeAbout UsCareersDeveloperResourcesBlog
  • Pi Squared
  • VSL Devnet
  • Pi Squared Docs
  • Verifiable Settlement Layer
    • Overview
    • Architecture
    • Applications
  • K Framework
    • Overview
    • Formal Semantics
  • LLVM-K Backend
  • Proof of Proof
    • Overview
  • Architecture
  • Math Proof Generation
  • Math Proof Checker
  • ZK Proof Generation
  • Applications
Powered by GitBook
On this page
  • Generating ZK Proofs with zkVMs
  • Benefits
  • Limitations
  • Generating ZK Proofs using Block Model (BM) Circuits
  • Benefits
  • Trade-offs
  • Comparison

Was this helpful?

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:

  1. By running the proof checker inside a zkVM

  2. 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

PreviousMath Proof CheckerNextApplications

Last updated 2 days ago

Was this helpful?