Halva
Direct answerHalva extracts the gate, copy, permutation and lookup constraints of a Halo2 circuit at synthesis time and lets engineers prove soundness in Lean 4. In July 2025 Nethermind used it to find a critical soundness bug in Scroll's deprecated Keccak-256 circuit.
- Maintainer
- Nethermind
- Website
- https://github.com/NethermindEth/Halva
- Repository
- https://github.com/NethermindEth/Halva
- Category
- ZK circuit verification
- Targets
- Halo2PLONKish
- Approach
- Extract gates, copy, permutation and lookup constraints at synthesis time; soundness proofs in Lean 4
- Access
- Open source
- Status (2026-09-13)
- Active, Ethereum Foundation grant
What Halva does
Halo2 circuits are notoriously hard to review because constraints are spread across configure and synthesize code. Halva instruments synthesis so the exact constraint system reaches Lean, where the specification is stated and the soundness theorem proved. The Scroll Keccak result is the clearest public example of a proof-assistant framework finding a real, critical circuit bug.
Where it is strong
- Works on real Halo2 code without rewriting it.
- Public critical finding in a production-grade circuit.
- Same team maintains CertiPlonk (Plonky3) and Lean EVM work, so zkEVM stacks can be covered end to end.
Limits and caveats
- Halo2 only.
- Soundness-focused; completeness is a separate exercise.
- Extraction is a trusted step; review it.
When to choose it
Choose Halva for any Halo2 or PLONKish circuit you cannot rewrite, particularly zkEVM components.
Who works with Halva
Nethermind (Formal Verification team).
Top-listed for circuit verification work: zkSecurity
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
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, Picus, LLZK, Garden, Lampe, proven-zk and gnark-lean-extractor, CIVER, Circomspect, zkFuzz, Coda, Ecne, NAVe, Verified Cairo AIR (Stone and S-two).