Lampe: Reilabs' Noir-to-Lean semantics extraction
=================================================

Lampe 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
Category: ZK circuit verification
Targets: Noir, ACIR
Approach: Semantics-first extraction of Noir programs into Lean 4, then property proofs
Access: Open source
Status: Active
Strengths: 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: Noir only. | Semantics extraction is part of the TCB. | Public examples still growing.
Firms using it: Reilabs
Sources: https://github.com/reilabs/lampe | https://reilabs.io

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