Reilabs: formal verification services for cryptography and ZK
=============================================================

Reilabs 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
Tools: Lampe, proven-zk and gnark-lean-extractor, Lean 4 and Mathlib
Evidence: https://github.com/reilabs/lampe | https://github.com/reilabs/proven-zk

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