Veridise recently completed a preliminary engagement with Succinct to evaluate the use of Picus — our tool for formally verifying the determinism of zero-knowledge (ZK) circuits — on SP1, Succinct’s RISC-V zkVM. The objective was to assess Picus’s ability to verify SP1 circuits and lay the foundation for a broader effort to verify the determinism of all SP1 circuits.
Over the course of the engagement, we successfully proved the determinism of several SP1 circuits using Picus. We also identified key improvements in our prototype verification pipeline that would enable Picus to scale to more complex circuits — improvements we’re excited to implement together in the next phase of our collaboration.
Why checking determinism matters in ZK circuit security
Most critical bugs in ZK circuits stem from underconstrained logic — missing equations that let malicious provers produce verifiable proofs that the developers did not intend. These so-called underconstrained bugs break soundness and are notoriously hard to detect.
Determinism offers a powerful safeguard: if a circuit’s outputs are uniquely determined by its inputs, then no unintended behaviors are possible. Proving determinism is therefore a practical way to rule out an entire class of bugs.
With Picus, we can formally prove determinism — mathematically guaranteeing that the circuit behaves exactly as intended, with no room for ambiguity or adversarial manipulation.
Building the bridge: Translating Succinct SP1 circuits to Picus
A key challenge in applying Picus to SP1 was the mismatch in circuit representations. Picus operates on circuits written in LLZK, Veridise’s intermediate representation, while SP1 circuits are defined in Plonky3. To bridge this gap, we developed a prototype extractor that translates Plonky3 circuits into LLZK. A huge thank you to John Guibas, CTO of Succinct, for his guidance during this development.
Our extractor has two main components:
air-llzk: A visitor that walks the Plonky3 constraint AST and emits LLZK.llzk-bridge: A Rust binding to LLZK’s C++ APIs, enabling Rust programs to generate LLZK circuits. We hope this binding can be reused to support other Rust-based EDSLs like Halo2 in the future.
With this infrastructure in place, we were able to apply Picus to an increasing number of SP1 circuits and formally verify their determinism.
Early results: 11 operations successfully verified
Once the extraction pipeline was in place, we began translating basic SP1 operations into LLZK. After translation, verifying determinism with Picus was as simple as pushing a button — and we successfully extracted and verified the following operations:
Current limitations in the Plonky3-to-LLZK pipeline
While the initial results were promising, scaling Picus to verify more complex SP1 circuits revealed several key limitations in the current translation pipeline from Plonky3 to LLZK:
1. Lack of modular constraint blocks
Plonky3 does not yet support logical grouping of constraints, which makes it difficult for Picus to reason about subcomponents in isolation.
2. No native input/output annotations
We had to specify the input and output columns manually. This is feasible for small circuits, but could become error-prone and unscalable for larger modules. Ideally, as the circuit is developed, the developer would specify the functional relationship between the columns.
3. Missing support for assumptions & postconditions
When verifying a large circuit composed of many sub-circuits, it’s important to be able to decompose the overall proof into smaller proofs for each subcomponent. However, sub-circuit proofs often rely on assumptions made by their callers — such as inputs being range-checked to lie within the byte range. Conversely, callers may depend on guarantees provided by their callees — for example, that exactly one output in a one-hot encoding is set to 1.
Ideally, these assumptions and guarantees could be expressed as annotations within the codebase and automatically extracted into LLZK for use during verification.
Succinct has recognized the importance of these gaps and has already committed engineering resources to extend their Plonky3 Air builder (the Rust API that defines constraints) to address them.
What’s ahead: Formal verification across all Succinct SP1 circuits
We plan to continue this collaboration with Succinct and extend our bridge so that Picus can verify all the circuits within SP1. With the improvements specified above, we’re optimistic that formal determinism checking will become a routine part of SP1’s circuit development.
