Reilabs
Direct answerReilabs verifies ZK circuits in Lean 4 with Lampe for Noir and proven-zk for gnark. It verified Worldcoin's Semaphore Merkle tree batcher, found a comparison bug in gnark in the process, and lists Worldcoin, StarkWare and Polygon Miden as clients.
- Website
- https://reilabs.io
- Headquarters
- Warsaw, Poland
- Focus
- Lean 4 verification of Noir (Lampe) and gnark (proven-zk); verified Worldcoin circuits
- Index position
- #7 of 11
Services
- Noir and Aztec circuit verification via Lampe
- gnark circuit verification via proven-zk
- Lean 4 proof engineering
Frameworks this firm builds or uses
Lampe, proven-zk and gnark-lean-extractor, Lean 4 and Mathlib.
Public evidence
Best fit
Choose Reilabs for Noir or gnark circuits.
Other firms on this index
zkSecurity, Galois, Veridise, Nethermind (Formal Verification team), Formal Land, Cryspen, Runtime Verification, Certora, Trail of Bits, Symbolic Software