Formal Verification of SP1 with Picus
Today, we’re excited to share a progress update on our formal verification efforts for SP1, developed in collaboration with Veridise, a leading firm in zero-knowledge security auditing. Formal verification plays a critical role in establishing mathematical guarantees about SP1’s behavior.
This work complements our multi-layered approach to SP1 security, including last month’s launch of SP1-2FA, which gives developers an easy-to-enable runtime safeguard against malicious prover behavior. Alongside thorough audits and external reviews, our collaboration with Veridise on determinism checking with Picus helps ensure that SP1 circuits behave exactly as intended, paving the way toward a formally verified zkVM with security rooted in both practice and theory.
Many circuit bugs, such as missing range checks or underconstrained variables, can be difficult to spot through manual review but are often revealed through non-determinism. If a circuit can produce multiple valid outputs for the same input, that’s a strong signal that something is underconstrained. By formally checking determinism, we can catch these issues early and rule out an entire class of subtle bugs that could otherwise compromise soundness. For SP1, this adds an important layer of assurance that every circuit behaves in a predictable, secure, and verifiable way.
This is an ongoing collaboration, and we’re excited to continue working with Veridise in the coming weeks to scale Picus across the entire SP1 stack, with the goal of formally verifying the determinism of every circuit in SP1. Beyond determinism, we also have exciting work in the pipeline focused on proving the formal correctness of our circuits, bringing us even closer to end-to-end mathematical guarantees. Stay tuned for more updates soon.
Learn more about how Veridise used their tool Picus to formally verify the determinism of key SP1 circuits, including u32 addition, XOR, and range checks, by translating SP1’s Plonky3-based constraints into LLZK, Veridise’s intermediate representation. Read the full technical breakdown in their blog post.
