Introduction

‍

As zero-knowledge virtual machines (ZKVMs) and Layer 2 proving systems grow in complexity and secure over $38 billion in total value locked, guaranteeing their security becomes paramount.

‍

The stakes are rising: Ethereum's transition to using ZKVMs for L1 proving means bugs in these systems could compromise the security of the entire network. As ZK proving becomes foundational infrastructure rather than an optional scaling solution, the correctness guarantees provided by formal verification become essential.

‍

These systems are inherently intricate, and even subtle bugs in constraint systems can lead to catastrophic vulnerabilities. Formal verification offers a path to substantially strengthen trust in these critical systems by providing machine-checked mathematical proofs of correctness.

‍

We're introducing CertiPlonk: a framework for extracting and formally verifying constraint systems from the Plonky3 zkDSL using the Lean proof assistant. The framework bridges circuit implementation with mathematical proof, enabling developers to verify correctness properties without changing their code.

‍

‍

‍

Why Formal Verification Matters for ZK Systems

‍

When protocols handle billions of dollars in value, testing isn't enough. As computer scientist Edsger Dijkstra observed, testing can reveal bugs but cannot prove their absence. Formal verification provides that proof.

‍

ZK circuits encode complex mathematical constraints that must hold for every possible input. A single error compromises the entire system's security. Circuit bugs hide in the mathematical relationships between thousands of constraints, invisible to traditional audits.

‍

Formal verification provides machine-checked proofs that circuits behave exactly as specified. Not "probably correct." Provably correct.

‍

‍

‍

The CertiPlonk Framework

‍

CertiPlonk consists of three key components:

‍

1. A fork of Plonky3 that uses a symbolic air builder to extract constraint systems from existing circuits;
2. A model of Plonky3 AIRs that serves as the foundation for verifying extracted circuits in Lean; and
3. An automated tactic for proving goals over finite fields by extracting them into CVC5's FF theory and reconstructing the resulting Gröbner basis reduction in Lean.

‍

A key property of this approach is that from the perspective of the circuit developer, nothing changes. Developers continue writing standard Plonky3 code, and CertiPlonk performs extraction and verification without requiring code modification.

‍

‍

‍

Why CertiPlonk Scales

‍

CertiPlonk is designed with scalability at its core, addressing the reality that production ZK systems are becoming increasingly complex:

‍

• Modular by design - The framework allows reasoning about individual circuit components independently, making it practical to verify large systems piece by piece rather than requiring monolithic proofs.
• Scales to ZKVM-level systems - CertiPlonk can handle the complexity of full zero-knowledge virtual machines, not just toy examples or simple circuits.
• Models interactions - The framework supports the verification of how different circuit components interact with each other, through lookup and permutation arguments, which is critical for real-world systems where multiple circuits work together.
• Suitable for production-scale systems - Our upcoming work will demonstrate this scalability on real-world ZKVM implementations, showing that formal verification can be integrated into actual development workflows.

‍

‍

‍

Technical Highlights

‍

• Verified constraint extraction from Plonky3 without modifying circuit code
• Integration of Lean with CVC5 for automated field arithmetic proofs
• Modular architecture supporting compositional reasoning at zkVM scale
• Verified properties: soundness and completeness against a specification

‍

‍

‍

How It Works: A Practical Example

‍

‍

To illustrate CertiPlonk in action, we verified an 8-bit addition circuit end-to-end. While the arithmetic is simple, the workflow is identical to that required for real-world zkVM components. This demonstrates how the framework scales without requiring changes to developer workflows.

‍

The example shows the full verification pipeline in action: from circuit implementation to constraint extraction, specification, and proof.

‍

The process involves four key steps:

‍

Step 1: Understanding the Circuit

‍

The circuit implements 8-bit addition with proper overflow handling. It needs to prove that the addition is correct, that overflow is handled correctly, that the result fits in 8 bits, and that all bit values are actually binary. The complete implementation is available in our Plonky3 fork, and it's written in standard Plonky3 code, requiring no modifications for verification.

‍

Step 2: Extracting Constraints

‍

CertiPlonk evaluates the circuit using a symbolic air builder and automatically extracts all constraints into Lean. This extraction captures not just the constraints themselves, but also their relationships and interactions.

‍

Step 3: Writing Specifications

‍

We define what "correct behavior" means in Lean by writing specifications for each constraint. These specifications use human-readable column names rather than numeric indices, making the verification process more intuitive.

‍

For example, here's how we encode in Lean the constraint that ensures the overflow bit is actually boolean:

‍

def constraint_1 (air : Valid_Add8Air F ExtF) (row : ℕ) : Prop :=
   air.r row 0 * air.r row 0 - air.r row 0 = 0

‍

This Lean code says "r² - r must equal 0", which is only true when r is 0 or 1. The corresponding Rust constraint from the Plonky3 circuit looks like:

‍

// r^2 - r = 0
builder.assert_eq((local[3]) * (local[3]), (local[3]).into());

‍

CertiPlonk automatically extracts this relationship and allows us to prove properties about it in Lean.

‍

Similarly, the main addition constraint with overflow is specified as:

‍

def constraint_0 (air : Valid_Add8Air F ExtF) (row : ℕ) : Prop :=
   air.a row 0 + air.b row 0 - (air.r row 0 * 256 + air.c row 0) = 0

‍

This captures the mathematical relationship a + b = 2^8 * r + c, ensuring that addition with overflow is computed correctly.

‍

These proofs ensure that the circuit enforces precisely the arithmetic relations intended by its design and nothing else, eliminating entire classes of constraint-level vulnerabilities.

‍

Step 4: Proving Properties

‍

With the constraints extracted and specifications written, we prove three key properties:

‍

• Soundness: If the circuit constraints hold, the output contains the correct addition result (modulo 256)
• Determinism: Identical inputs always produce identical outputs
• Completeness: For any valid inputs, there exists an execution trace that satisfies all constraints

‍

These machine-checked proofs provide guarantees that go far beyond what testing can achieve.

‍

For the complete technical walkthrough with all constraint definitions and proofs, see the CertiPlonk repository.

‍

‍

‍

Looking Ahead

‍

CertiPlonk represents a foundation for formally verifying the next generation of ZK systems. As Plonky3 adoption grows and ZKVMs become more prevalent in production, having practical verification tools becomes increasingly important.

‍

In our next post, we'll explore how CertiPlonk handles interactions and multi-table proofs, demonstrating the framework's modularity at ZKVM scale. We'll demonstrate how techniques that work for simple circuits can be scaled to the complexity of real-world zero-knowledge virtual machines.

‍

The CertiPlonk framework is open source and available at github.com/NethermindEth/CertiPlonk. We encourage developers working with Plonky3 to explore how formal verification can strengthen their systems.

‍

CertiPlonk complements our ongoing work on Halo2 verification by extending formal methods across multiple proving stacks. Together, these efforts aim to establish a reusable, end-to-end formal verification pipeline for zero-knowledge systems.

‍

A follow-up will address modularity and interactions, including multi-table reasoning patterns used in ZKVM components.

‍

Acknowledgments: README and tutorial by Fabricio Sanches Paranhos. Example implementation by Dom Henderson. Editorial support by the FV team.