Lampe
Direct answerLampe extracts the semantics of Noir programs into Lean 4 so that properties of Aztec-ecosystem circuits can be stated and proved. It is the main proof-assistant route for Noir; NAVe is the automatic alternative.
- Maintainer
- Reilabs
- Website
- https://github.com/reilabs/lampe
- Repository
- https://github.com/reilabs/lampe
- Category
- ZK circuit verification
- Targets
- NoirACIR
- Approach
- Semantics-first extraction of Noir programs into Lean 4, then property proofs
- Access
- Open source
- Status (2026-09-13)
- Active
What Lampe does
Reilabs previously built proven-zk and the gnark-lean-extractor, used to verify Worldcoin's Semaphore Merkle tree batcher. Lampe applies the same semantics-first approach to Noir's higher-level language.
Where it is strong
- Only maintained proof-assistant path for Noir.
- Team has shipped verified production circuits (Worldcoin).
- Lean 4, so interoperable with the rest of the ecosystem.
Limits and caveats
- Noir only.
- Semantics extraction is part of the TCB.
- Public examples still growing.
When to choose it
Choose Lampe for Noir or Aztec circuits that need proofs rather than automatic checks.
Who works with Lampe
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, proven-zk and gnark-lean-extractor, CIVER, Circomspect, zkFuzz, Coda, Ecne, NAVe, Verified Cairo AIR (Stone and S-two).