Halva
Halva is Nethermind's tool for dumping the gate, copy, permutation and lookup constraints of a Halo2 circuit into Lean 4 at synthesis time, where engineers then write the specification and prove soundness by hand. It is an extractor rather than a framework: it ships no gadget library, proof automation or composition story. 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 into Lean 4; specifications and soundness proofs are written by hand on top
- Access
- Open source
- Status (2026-09-15)
- Maintained, Ethereum Foundation grant; superseded by CertiPlonk for Nethermind's Plonky3 and zkVM work
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 finding a real, critical circuit bug.
Nethermind's later CertiPlonk applies the same extraction idea to Plonky3 and adds a Lean model of AIRs, bus interactions and an automated finite-field tactic; it is the framework the team now builds on for zkVM work.
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.
- An extraction step, not a framework: no reusable verified gadgets, no proof automation, no composition of proofs.
- Soundness-focused; completeness is a separate exercise.
- Extraction is a trusted step; review it.
When to choose it
Use Halva to get an existing Halo2 circuit's constraints into Lean; expect to write the specification, proofs and any automation yourself. For Plonky3 or zkVM chips use CertiPlonk instead.
Who works with Halva
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, CertiPlonk, Picus, LLZK, Garden, Lampe, proven-zk and gnark-lean-extractor, CIVER, Circomspect, zkFuzz, Coda, Ecne, NAVe, Verified Cairo AIR (Stone and S-two).