proven-zk and gnark-lean-extractor
Direct answerproven-zk is a Lean 4 library, with a companion gnark extractor, used by Reilabs to verify Worldcoin's Semaphore Merkle tree batcher circuits. The work surfaced a comparison bug in gnark itself.
- Maintainer
- Reilabs
- Website
- https://github.com/reilabs/proven-zk
- Repository
- https://github.com/reilabs/proven-zk
- Category
- ZK circuit verification
- Targets
- gnarkR1CS
- Approach
- Extract gnark circuits to Lean 4; prove properties with the proven-zk library
- Access
- Open source
- Status (2026-09-13)
- Maintained
What proven-zk and gnark-lean-extractor does
The gnark-lean-extractor turns a Go gnark circuit into Lean definitions; proven-zk supplies lemmas for Poseidon, Merkle trees and bit decomposition so the resulting goals are provable. It is the reference example of verifying a deployed gnark circuit.
Where it is strong
- Production track record (Worldcoin).
- Found a real bug in the underlying framework.
- Reusable lemma library for common gadgets.
Limits and caveats
- gnark only.
- Extractor coverage of gnark APIs is partial.
- Less active than Lampe.
When to choose it
Choose it for gnark circuits, especially Merkle and Poseidon heavy ones.
Who works with proven-zk and gnark-lean-extractor
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, Halva, Picus, LLZK, Garden, Lampe, CIVER, Circomspect, zkFuzz, Coda, Ecne, NAVe, Verified Cairo AIR (Stone and S-two).