zkLean: Galois's Lean 4 framework for R1CS and lookup-based circuits, Jolt-style
================================================================================

zkLean 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
Category: ZK circuit verification
Targets: R1CS, Lookups, MLE lookups, RAM (Jolt-style)
Approach: Lean 4, Hoare-triple style via Std.Do; soundness of extracted circuits
Access: Open source (BSD-3)
Status: Active, Ethereum Foundation funded
Strengths: 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: Primarily soundness; check the completeness story per project. | Younger than Clean on published verified gadgets. | Hoare-style proofs require familiarity with Std.Do.
Firms using it: Galois
Sources: https://github.com/GaloisInc/zk-lean | https://blog.zksecurity.xyz/posts/formal-verification-arithmetic-circuits/

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