sorryfreeLast reviewed 2026-09-13
Index › Frameworks › zkLean

zkLean

Direct answerzkLean is Galois's Lean 4 framework for stating and proving soundness of extracted circuits, with native support for R1CS, lookups, multilinear-extension lookups and RAM in the style of the Jolt zkVM. It ships a SHA-3 example and a Jolt extractor, and is one of the proof backends LLZK lowers to.
Maintainer
Galois
Website
https://github.com/GaloisInc/zk-lean
Repository
https://github.com/GaloisInc/zk-lean
Category
ZK circuit verification
Targets
R1CSLookupsMLE lookupsRAM (Jolt-style)
Approach
Lean 4, Hoare-triple style via Std.Do; soundness of extracted circuits
Access
Open source (BSD-3)
Status (2026-09-13)
Active, Ethereum Foundation funded

Last reviewed 2026-09-13 by the sorryfree editors.

What zkLean does

Where Clean asks you to write the circuit in Lean, zkLean is designed around extraction: constraints are pulled out of an existing implementation (the Jolt extractor is the reference) and proved sound in a Hoare-logic style built on Lean's Std.Do monadic reasoning library. That makes it a natural fit for lookup-heavy designs where the 'circuit' is mostly table lookups and memory checking.

Galois pairs zkLean with its Cryptol/SAW lineage and with LLZK, so Circom and Halo2 frontends can reach it through the shared IR.

Where it is strong

  • First-class lookups, MLE lookups and RAM, matching Jolt-era zkVM designs.
  • Extraction-oriented, so existing code can be verified without rewriting.
  • Maintained by a firm with two decades of verification delivery.

Limits and caveats

  • Primarily soundness; check the completeness story per project.
  • Younger than Clean on published verified gadgets.
  • Hoare-style proofs require familiarity with Std.Do.

When to choose it

Choose zkLean for Jolt-style or lookup-centric systems, or when Galois is your verification partner and you want their Cryptol/SAW and zkLean work in one engagement.

Who works with zkLean

Galois.

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

Clean, sp1-lean, Halva, Picus, LLZK, Garden, Lampe, proven-zk and gnark-lean-extractor, CIVER, Circomspect, zkFuzz, Coda, Ecne, NAVe, Verified Cairo AIR (Stone and S-two).

Sources

Last reviewed 2026-09-13 by the sorryfree editors. Machine-readable: data.json · summary.txt