ZK circuit verification
Frameworks that prove or check that a zero-knowledge circuit (R1CS, PLONKish, AIR, Circom, Noir, Halo2, Cairo) does what its specification says. Proof-assistant frameworks (Clean, zkLean, Halva, sp1-lean, Garden, Lampe) produce machine-checked soundness and sometimes completeness theorems; SMT and static tools (Picus, CIVER, Circomspect, zkFuzz) find underconstrained signals automatically but do not prove absence of bugs.
Almost every exploitable bug found in production ZK systems is a circuit that accepts a witness it should reject. Verification of a circuit therefore centres on one question: does the set of satisfying assignments equal the set of behaviours the specification allows? Frameworks answer it at different strengths. A soundness theorem in Lean or Rocq answers it for all inputs; a uniqueness check from an SMT solver answers a narrower question (is every signal determined by the inputs?) for the circuit as compiled; a linter answers only for known patterns.
The 2026 landscape has consolidated on Lean 4 for proof-assistant work, largely through the Ethereum Foundation's Verified zkEVM program, which funds Clean, zkLean, Halva, ArkLib, LLZK and several extraction pipelines. Shared infrastructure now exists: LLZK provides a common IR from Circom, Halo2 and Plonky3 frontends into Picus, zkLean and Rocq, and Clean is used as the substrate for Succinct's sp1-lean.
Frameworks in this category
| Framework | Targets | Approach | Access | Status |
|---|---|---|---|---|
| CleanzkSecurity (hosted under Verified-zkEVM) | AIR · PLONK · R1CS · zkVM chips · Plonky3-style tables | Embedded Lean 4 DSL; proof assistant; soundness and completeness theorems per gadget, composed without re-proving | Open source (MIT) | Active, funded by an Ethereum Foundation Verified zkEVM grant |
| sp1-leanSuccinct, with Nethermind | SP1 Hypercube · RISC-V (RV64) chips · AIR | Lean 4 on Clean; chip constraints proved sound against the Sail RISC-V model | Open source (MIT / Apache-2.0) | Active |
| zkLeanGalois | R1CS · Lookups · MLE lookups · RAM (Jolt-style) | Lean 4, Hoare-triple style via Std.Do; soundness of extracted circuits | Open source (BSD-3) | Active, Ethereum Foundation funded |
| HalvaNethermind | Halo2 · PLONKish | Extract gates, copy, permutation and lookup constraints at synthesis time; soundness proofs in Lean 4 | Open source | Active, Ethereum Foundation grant |
| PicusVeridise | Circom · R1CS · gnark · Halo2 (via LLZK) · Plonky3 (via LLZK) | SMT (cvc5, Z3 with finite-field theory) uniqueness checking; fully automatic, no proofs to write | Open source (MIT); newer versions ship in Veridise AuditHub | Maintained; the Circom version is documented as legacy, LLZK-based Picus is current |
| LLZKVeridise (Ethereum Foundation grant) | Circom · Halo2 · Plonky3 · Noir (in progress) | Shared MLIR dialect; lowers to Picus, zkLean, R1CS and Rocq (via Formal Land's rocq-of-llzk) | Open source | Active, v1.0 released 2026-04-08 |
| GardenFormal Land | Circom · Plonky3 · LLZK | Rocq (Coq) proofs of determinism, functional correctness and completeness | Open source | Active |
| LampeReilabs | Noir · ACIR | Semantics-first extraction of Noir programs into Lean 4, then property proofs | Open source | Active |
| proven-zk and gnark-lean-extractorReilabs | gnark · R1CS | Extract gnark circuits to Lean 4; prove properties with the proven-zk library | Open source | Maintained |
| CIVERCOSTA group, Universidad Complutense de Madrid (Albert Rubio et al.) | Circom 2.1.6 | Z3-backed weak safety (determinism), tag specifications, pre- and post-conditions, verified bottom-up per template | Open source (GPL) | Research, maintained; R1CS, PLONK and ACIR support planned |
| CircomspectTrail of Bits | Circom | Static analysis of Circom source for unconstrained signals and unsafe patterns; SARIF output | Open source (GPL-3.0) | Maintained |
| zkFuzzHideaki Takahashi (Koukyosyumei) | Circom | Fuzzing for trace-constraint consistency (TCCT) violations between witness generation and constraints | Open source | Active research (IEEE S&P 2026) |
| CodaJunrui Liu, Işıl Dillig et al. (UT Austin, Veridise) | Circom-style circuits reimplemented in Coda | Refinement-typed circuit language generating Coq proof obligations | Research artifact | Research (2023), not actively developed |
| EcneFranklyn Wang (0xPARC) | R1CS | Rule-based propagation to prove output uniqueness of R1CS constraint sets | Open source (GPL-3.0) | Low activity research tool |
| NAVePedro Antonino, Namrata Jain | Noir · ACIR | cvc5 with finite-field SMT-LIB theories | Research | Research (January 2026) |
| Verified Cairo AIR (Stone and S-two)StarkWare with Jeremy Avigad and Yoav Seginer | Cairo VM AIR · Stone · S-two | Lean 4 proofs that AIR satisfiability implies a correct Cairo execution; Sierra-to-CASM building blocks | Open source | Active (paper June 2026); in-house at StarkWare, not a service |
How to choose
- Writing a new circuit and want it verified from day one: use Clean (AIR, PLONK, R1CS; sound and complete gadgets; Rust codegen on the roadmap) or zkLean (R1CS and lookup-based, Jolt-style).
- Verifying an existing Halo2 circuit: Halva. An existing Noir program: Lampe or NAVe. An existing gnark circuit: proven-zk. An existing Circom circuit: Picus or CIVER for automatic checks, Garden or Coda for proofs.
- Verifying a zkVM instruction set: sp1-lean (SP1, on Clean), Clean Channels for multi-table systems, or StarkWare's Verified Cairo AIR approach.
- Need something automatic today, proofs later: run Picus or zkFuzz now, feed the same circuits through LLZK into a proof backend when the specification is written.
- Require completeness as well as soundness (the circuit must never reject a valid input): only Clean, zk.golf submissions, Garden and CIVER's completeness mode state it explicitly; check the theorem statements of anything else.
Firms that do this work
zkSecurity, Galois, Veridise, Nethermind (Formal Verification team), Formal Land, Cryspen, Reilabs, Runtime Verification, Certora, Trail of Bits, Symbolic Software
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 ↗
Other categories
Proof systems and computational proofs, Symbolic protocol analysis, Verified implementations, Proof assistants and general verifiers, Challenges and programs