How Succinct Achieved Continuous ZK Security with Picus

Succinct and AuditHub partnered in May 2025 on a small proof of concept demonstrating that Picus could automatically check the determinism of SP1 circuits. The success of that initial collaboration prompted Succinct to work with us to integrate Picus into their development workflow and verify the determinism of SP1-Hypercube, their next-generation Risc-V zkVM, before any external audits. The results exceeded our expectations.

Here are the 3 key success stories:

1. Early detection: Picus caught three critical underconstrained issues early in development.
2. Full-chip verification: After addressing these issues, we verified the determinism of all RISC-V chips—namely the alu , control_flow , and memory  chips—as well as the SHA-256, and Poseidon2 precompiles.
3. Independent adoption: Succinct independently used Picus through our AuditHub platform to identify another critical underconstrainedness issue while developing a new chip—further validating that formal methods can be highly effective throughout the development lifecycle.

In the rest of this post, we’ll describe what Picus does, our methodology for verifying the Hypercube chips, and what’s next for this collaboration.

Underconstrained Circuits and Picus

In ZK circuits, underconstrained vulnerabilities occur when the circuit lacks necessary constraints—allowing invalid or inconsistent witnesses to still produce valid proofs. In short, the circuit doesn’t fully capture the intended computation, leaving “wiggle room” for incorrect proofs that verify. These issues don’t trigger test failures or crashes; instead, they silently compromise soundness and are notoriously hard to detect.

Enter Picus

Picus is our state-of-the-art verifier for automatically finding underconstrained vulnerabilities. It does so by checking a closely related property: determinism. Given a circuit C(I,O), relating inputs I and outputs O, Picus uses a combination of static analysis and SMT solvers to prove that C defines a partial function from I to O—or produces a counterexample demonstrating nondeterminism. Note that if the computation expressed by the circuit is determinisitic, then nondeterminism implies underconstrainedness. Since most circuits intend to express deterministic computation, this allows Picus to catch a broad class of underconstrainedness bugs.

Verification Pipeline

To verify the determinism of the SP1-Hypercube chips, we built a verification pipeline with three stages:

1. Extract SP1 constraints
2. Specify inputs and outputs
3. Run Picus through AuditHub

Our goals were to (1) enable extraction of all SP1 chips into a form Picus could analyze, (2) preserve debug information to map counterexamples back to source code, and (3) make it easy to specify which columns corresponded to inputs and outputs.

To accomplish this, we extended the SP1 constraint compiler with a dedicated Picus backend.

This backend takes as input SP1’s internal constraint IR—structured expressions of the form:

The backend emits constraints in the Picus intermediate format for automated analysis. Early in the engagement, we generated constraints directly in Picus’s internal language. Later, we introduced an intermediate LLZK backend, allowing us to apply a series of optimizations and rewrites that made the extracted constraints more efficient and easier to verify.

A major challenge was that neither SP1’s IR nor their Plonky3 constraints explicitly identify inputs and outputs, making it difficult to define the I/O interface of each chip for Picus without manually annotating every column which would have been cumbersome. This led to our second design goal: finding a scalable and automated way to infer and preserve this information across all chips.

Specifying Inputs/Outputs

Early in the collaboration, we worked closely with the Succinct team to determine the most systematic and least error-prone way to identify circuit inputs and outputs. After several design discussions, we realized that the cleanest solution was already embedded in SP1’s design itself — its interaction system.

In SP1, circuits communicate through interactions that model reads and writes to memory, registers, and various oracles. Each interaction specifies a kind, a direction (send or receive), and a set of values. These interactions naturally define the circuit’s I/O boundary, making them an ideal basis for input/output inference.

Some representative interaction kinds include:

Together, we designed a mapping from interaction semantics to Picus I/O roles:

• Writes to memory or registers are treated as outputs.
• Reads from memory or registers are treated as inputs.

This collaboration gave us a principled, automatable way to extract I/O information without manually labeling every column.

We also incorporated well-formedness checks to ensure that all memory operations respected SP1’s encoding conventions. For example, each 64-bit word is represented as four 16-bit field elements, and Picus validates these range constraints to guarantee each limb is valid. When reading from memory, these assumptions are verified implicitly.

In total, we formalized 20 lightweight interaction specifications, each primarily mapping (kind, direction)  pairs to input/output roles and describing which range constraints should apply to which values. Despite their simplicity, these specs captured all the relevant SP1 I/O semantics and made it much easier to add new chips to our verification pipeline.

Using Picus with AuditHub

With all SP1-Hypercube chips extracted and their I/O specifications defined, we ran Picus through our AuditHub platform to automatically verify their determinism. The results were excellent: Picus successfully verified all RISC-V chips—including the alu , control_flow , and memory  components—along with the SHA-256 and Poseidon2 precompiles, and uncovered three critical underconstrained issues in the DivRem  circuit, which implements the RISC-V division and remainder opcodes.

The DivRem chip is particularly challenging—not just to verify, but also to implement. In addition to supporting both signed and unsigned 64-bit (and 32-bit) division, it must handle a number of subtle edge cases, such as division by zero and division involving INT_MIN . These conditions lead to complex branching and arithmetic relationships, resulting in a large and intricate constraint system. Given this complexity, it’s not surprising that Picus surfaced a few underconstrained regions early in development.

Using the counterexamples produced by Picus, the Succinct team was able to quickly isolate and resolve these issues. Afterward, Picus verified the determinism of the final DivRem  circuit.