ZK circuit formal verification frameworks: Clean, zkLean, Halva, Picus, LLZK and others compared
================================================================================

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.

Clean: zkSecurity (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 — Active, funded by an Ethereum Foundation Verified zkEVM grant
sp1-lean: Succinct, with Nethermind — SP1 Hypercube, RISC-V (RV64) chips, AIR — Lean 4 on Clean; chip constraints proved sound against the Sail RISC-V model — Active
zkLean: Galois — R1CS, Lookups, MLE lookups, RAM (Jolt-style) — Lean 4, Hoare-triple style via Std.Do; soundness of extracted circuits — Active, Ethereum Foundation funded
Halva: Nethermind — Halo2, PLONKish — Extract gates, copy, permutation and lookup constraints at synthesis time; soundness proofs in Lean 4 — Active, Ethereum Foundation grant
Picus: Veridise — Circom, R1CS, gnark, Halo2 (via LLZK), Plonky3 (via LLZK) — SMT (cvc5, Z3 with finite-field theory) uniqueness checking; fully automatic, no proofs to write — Maintained; the Circom version is documented as legacy, LLZK-based Picus is current
LLZK: Veridise (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) — Active, v1.0 released 2026-04-08
Garden: Formal Land — Circom, Plonky3, LLZK — Rocq (Coq) proofs of determinism, functional correctness and completeness — Active
Lampe: Reilabs — Noir, ACIR — Semantics-first extraction of Noir programs into Lean 4, then property proofs — Active
proven-zk and gnark-lean-extractor: Reilabs — gnark, R1CS — Extract gnark circuits to Lean 4; prove properties with the proven-zk library — Maintained
CIVER: COSTA 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 — Research, maintained; R1CS, PLONK and ACIR support planned
Circomspect: Trail of Bits — Circom — Static analysis of Circom source for unconstrained signals and unsafe patterns; SARIF output — Maintained
zkFuzz: Hideaki Takahashi (Koukyosyumei) — Circom — Fuzzing for trace-constraint consistency (TCCT) violations between witness generation and constraints — Active research (IEEE S&P 2026)
Coda: Junrui Liu, Işıl Dillig et al. (UT Austin, Veridise) — Circom-style circuits reimplemented in Coda — Refinement-typed circuit language generating Coq proof obligations — Research (2023), not actively developed
Ecne: Franklyn Wang (0xPARC) — R1CS — Rule-based propagation to prove output uniqueness of R1CS constraint sets — Low activity research tool
NAVe: Pedro Antonino, Namrata Jain — Noir, ACIR — cvc5 with finite-field SMT-LIB theories — 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 — 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.

Source page: https://sorryfree.com/categories/zk-circuits/
Compiled by: sorryfree editors (https://sorryfree.com/about/)
Last reviewed: 2026-09-13