sp1-lean: Lean verification of SP1 Hypercube's RISC-V chips, built on Clean
===========================================================================

sp1-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
Category: ZK circuit verification
Targets: SP1 Hypercube, RISC-V (RV64) chips, AIR
Approach: Lean 4 on Clean; chip constraints proved sound against the Sail RISC-V model
Access: Open source (MIT / Apache-2.0)
Status: Active
Strengths: 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: 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).
Firms using it: zkSecurity, Nethermind (Formal Verification team)
Sources: https://blog.succinct.xyz/nethermind-lean/ | https://zkevm.ethereum.foundation/blog/sp1-fv

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