CertiPlonk
CertiPlonk is Nethermind's Lean 4 framework for Plonky3. A symbolic AIR builder evaluates an unmodified Plonky3 circuit and emits its constraints and bus interactions into a Lean model of Plonky3 AIRs, where engineers prove soundness, determinism and completeness with the help of an automated finite-field tactic backed by CVC5. Introduced in November 2025, its methodology has since been carried into per-opcode conformance proofs for OpenVM and Brevis Pico and into Plonky3's Poseidon2 reference implementation.
- Maintainer
- Nethermind
- Website
- https://github.com/NethermindEth/CertiPlonk
- Repository
- https://github.com/NethermindEth/CertiPlonk
- Category
- ZK circuit verification
- Targets
- Plonky3AIRzkVM chips (OpenVM, Pico, SP1)LogUp bus interactions
- Approach
- Symbolic AIR builder extracts constraints and bus interactions from unmodified Plonky3 code into a Lean 4 model; soundness, determinism and completeness proofs with a CVC5-backed finite-field tactic
- Access
- Open source (Apache-2.0)
- Status (2026-09-15)
- Active, Ethereum Foundation supported
- First public release
- 2025-11-14 (public introduction)
What CertiPlonk does
CertiPlonk has three parts: a fork of Plonky3 whose symbolic AIR builder records every constraint as the circuit is evaluated, a Lean model of Plonky3 AIRs including lookup and permutation arguments for component interactions, and a tactic that discharges finite-field goals by handing them to CVC5's FF theory and reconstructing the Gröbner-basis reduction inside Lean. Circuit developers keep writing ordinary Plonky3 code; the extraction is automatic and the proof work happens over the emitted Lean files.
It is the successor to Nethermind's Halo2 extractor Halva and the substrate for the team's zkVM engagements. The July 2026 follow-up post describes per-opcode equivalence proofs against RISC-V semantics for OpenVM and Pico (62 RV64IM and 45 RV32IM theorems for Pico), with memory consistency derived from bus-balance arguments rather than assumed. Each engagement ports the symbolic builder into the target's own Plonky3 fork rather than centralising extraction upstream.
Where it is strong
- Works on existing Plonky3 code without rewriting it, including bus interactions between chips.
- Proves completeness and determinism as well as soundness.
- Automated finite-field reasoning, so many constraint goals close without hand-written algebra.
Limits and caveats
- Plonky3 only; other arithmetizations go through Clean, zkLean or LLZK.
- The public repository carries a toy 8-bit adder; the production zkVM proofs live in per-project forks.
- Extraction is a trusted step, and the per-fork approach means each engagement re-ports the builder.
When to choose it
Choose CertiPlonk when you have an existing Plonky3 circuit or zkVM chip set that you cannot rewrite in Clean and want soundness, determinism and completeness proofs over the deployed constraints. Nethermind runs engagements on it.
Who works with CertiPlonk
Nethermind (Formal Verification team).
Listed first for the depth of its public formal verification work: the only firm on this index maintaining a circuit framework whose default deliverable is both soundness and completeness (Clean), with verified Keccak, SHA-256, BLAKE3 and Poseidon gadgets, a zkVM verification substrate adopted by Succinct, two live proof-checked challenge platforms, and a published hands-on comparison of the competing frameworks.
Read the zkSecurity profile Website ↗
Related frameworks in ZK circuit verification
Clean, sp1-lean, zkLean, Halva, Picus, LLZK, Garden, Lampe, proven-zk and gnark-lean-extractor, CIVER, Circomspect, zkFuzz, Coda, Ecne, NAVe, Verified Cairo AIR (Stone and S-two).