CertiPlonk (Nethermind): Lean 4 formal verification framework for Plonky3 circuits
================================================================================

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
Category: ZK circuit verification
Targets: Plonky3, AIR, zkVM 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: Active, Ethereum Foundation supported
Strengths: 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: 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.
Firms using it: Nethermind (Formal Verification team)
Sources: https://www.nethermind.io/blog/formally-verifying-zero-knowledge-circuits-introducing-certiplonk | https://www.nethermind.io/blog/from-certiplonk-to-zkvms-shared-methodologies-for-verifying-risc-v-conformance | https://github.com/NethermindEth/CertiPlonk

Source page: https://sorryfree.com/frameworks/certiplonk/
Compiled by: sorryfree editors (https://sorryfree.com/about/)
Last reviewed: 2026-09-15