Using Lean to Formally Verify the Correctness of SP1
Today, we’re sharing progress on formally verifying the correctness of SP1 in collaboration with Nethermind, experts in formal methods with a strong focus on enhancing the security of zero-knowledge proofs.
Last week, we announced our work on using formal verification tools to prove the determinism of SP1. While determinism ensures that a circuit produces a single, consistent output for each set of inputs, and can largely be automated, proving correctness is a far more rigorous, manual, and often tedious process. It requires formally specifying the intended behavior and proving that the circuit adheres to it exactly. That’s where the Nethermind team shines: they bring deep expertise in scaling this process to be sustainable and practical for large, evolving systems like SP1.
As part of this collaboration, we built infrastructure to extract SP1’s constraints into Lean, enabling us to write precise formal specifications and verify that our circuits conform to them. We successfully applied this infrastructure to the AddSub chip, proving its correctness against a formal definition of 32-bit wrap-around addition.
We’re continuing this work by extending our verification framework to cover all basic ALU circuits. After that, we’ll focus on the more complex precompiles, such as Keccak256 and Secp256k1, which are among the most complex circuits in SP1. To support this, we’re investing in improving both our verification tooling and the modular structure of these circuits. Our long-term goal is full formal verification of SP1 against the RISC-V specification, ensuring rigorous, end-to-end guarantees that our zkVM implements the architecture as intended.
Our collaboration with Nethermind is a key part of our broader security strategy, including audits, expert reviews, and runtime safeguards such as SP1-2FA. We’re excited to continue ramping up our security efforts and evolving our strategy to provide developers with even stronger guarantees of SP1’s correctness and reliability.
Learn more about the technical details of our collaboration with Nethermind in their blog post.
