Halva: Nethermind's Lean 4 verification of Halo2 circuits
=========================================================

Halva 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
Category: ZK circuit verification
Targets: Halo2, PLONKish
Approach: Extract gates, copy, permutation and lookup constraints at synthesis time; soundness proofs in Lean 4
Access: Open source
Status: Active, Ethereum Foundation grant
Strengths: 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: Halo2 only. | Soundness-focused; completeness is a separate exercise. | Extraction is a trusted step; review it.
Firms using it: Nethermind (Formal Verification team)
Sources: https://www.nethermind.io/blog/formal-verification-of-halo2-circuits-in-lean | https://github.com/NethermindEth/Halva

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