sp1-lean

Direct answersp1-lean is Succinct's Lean 4 project, developed with Nethermind, that expresses the constraints of SP1 Hypercube's RISC-V chips in Clean and proves them sound against the Sail RISC-V reference model. As of the Ethereum Foundation's May 2026 review, 51 of 62 opcodes were fully proven; completeness is deferred for five chips.

Maintainer: Succinct, with Nethermind
Website: https://github.com/succinctlabs/sp1-lean
Repository: https://github.com/succinctlabs/sp1-lean
Category: ZK circuit verification
Targets: SP1 HypercubeRISC-V (RV64) chipsAIR
Approach: Lean 4 on Clean; chip constraints proved sound against the Sail RISC-V model
Access: Open source (MIT / Apache-2.0)
Status (2026-09-13): Active
First public release: 2025-10-09 (announcement)

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

What sp1-lean does

The project is the most visible zkVM verification effort in public. Each RISC-V chip's AIR constraints are restated as a Clean circuit whose specification is the Sail semantics of the instruction, and soundness is proved 'axiom-clean' (no additional axioms beyond Lean's core).

It is also the public case study in specification gaps. In May 2026 the Ethereum Foundation disclosed a JALR bug in SP1 Hypercube whose theorem assumed a 4-byte-aligned jump target, so the proof was valid but excluded legitimate programs. The disclosure and the accompanying audit of sp1-lean are required reading before trusting any zkVM proof claim.

Where it is strong

Real, deployed zkVM constraints proved against an independent ISA model rather than a hand-written spec.
Built on Clean, so proofs compose with other Clean gadgets and benefit from the Channel work for multi-table soundness.
Openly reviewed by a third party (the EF Formal Verification team), with gaps published.

Limits and caveats

Specific to SP1 Hypercube; not a general framework.
Completeness deferred for several chips and some opcodes still unproven at last public review.
Correspondence between the Lean restatement and the Rust constraints is a manual step (a Plonky3 codegen backend for Clean would close it).

When to choose it

Read sp1-lean when you deploy on SP1 or want a template for verifying your own zkVM's chips in Clean.

Who works with sp1-lean

zkSecurity, Nethermind (Formal Verification team).

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, zkLean, 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