proven-zk and gnark-lean-extractor: Lean 4 verification of gnark circuits
=========================================================================

proven-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
Category: ZK circuit verification
Targets: gnark, R1CS
Approach: Extract gnark circuits to Lean 4; prove properties with the proven-zk library
Access: Open source
Status: Maintained
Strengths: Production track record (Worldcoin). | Found a real bug in the underlying framework. | Reusable lemma library for common gadgets.
Limits: gnark only. | Extractor coverage of gnark APIs is partial. | Less active than Lampe.
Firms using it: Reilabs
Sources: https://github.com/reilabs/proven-zk

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