How Matter Labs used AuditHub’s Picus to prove determinism across most of ZKsync Airbender’s circuits, in an engagement that found and fixed three critical soundness bugs ahead of the V2 prover upgrade.
ZKsync Airbender is the prover behind Matter Labs’ ZKsync stack, a STARK-based RISC-V zkVM that runs a program and then proves it ran correctly. Those proofs are what let the chains on the stack settle to Ethereum. Airbender’s circuits are highly optimized, and in that setting small omissions, such as failing to finalize a constraint accumulator, can leave parts of the intended computation unconstrained. If the prover can be made to prove an execution that never happened, every chain behind it is exposed.
The engagement
Before shipping the V2 prover, Matter Labs brought us in. The engagement centered on Picus, our automated formal verifier for ZK circuits. Rather than a broad bug hunt, the goal was to determine whether the prover’s most dangerous class of bug was present in the circuits that mattered most, and to fix any that were.
The challenge: bugs you cannot test for
The class in question is the underconstrained circuit. The constraints are supposed to tie each input to a single valid output. When they don’t, the circuit accepts more than one. An attacker only has to find a second witness, one that satisfies the constraints but does not match the real computation, and the verifier accepts the proof. In a zkVM, that is enough to prove a state transition that never happened.
Testing cannot establish that these bugs are absent. A test suite feeds the circuit honest inputs, so a passing suite shows correct behavior on the cases that were tried; it says nothing about the witnesses an attacker constructs deliberately. Airbender’s design compounds this. It carries almost no machine state from row to row and ties execution together through shared arguments that span the whole proof, so a single missing constraint can break soundness without anything in the affected circuit looking wrong on its own.
Why Picus?
Matter Labs had a view on this going in. For a codebase this optimized, they put more faith in tooling than in manual review alone.
“I’ve seen weak results from manual audits of these kinds of codebases, my own included. This complexity is better handled by tools. We knew Picus well, down to the original paper, and had built something similar for an earlier proving system, so we were confident it was the right approach.”
Antonio Locascio, Security Engineer at Matter Labs
The solution: Picus and expert review
Picus proves that a circuit is deterministic: for any input, only one output can satisfy the constraints. Proving that rules out a large class of underconstrainedness bugs in the circuit, and the result covers every input rather than a sample. So we ran Picus across the circuits in scope. The verifier that combines all those proofs is not a circuit, so our analysts reviewed it manually, and we fuzzed the executor and prover against a reference emulator to check their correctness.
Getting Airbender into Picus took setup. Its circuits were translated into LLZK, an intermediate representation, then lowered into the language Picus checks, with debug information preserved so any counterexample maps back to the source.
Evaluation highlights
Picus verified 21 of the 26 circuits in scope as deterministic. The five it could not resolve were the largest whole-circuit and delegation components, where the constraints interact too densely for the current extraction to split apart cleanly. All five are identified in the report.
Picus also caught one of the three critical bugs. In the unrolled jump_branch_slt circuit, a missing constraint-finalization step left the arithmetic for branch comparisons and the next program counter unenforced, which would have let a prover forge them. The fix was a single line, re-verified in Picus.
The other two criticals were in the full-statement verifier, the code that composes many circuit proofs. With Picus covering the circuits, manual review concentrated there. As it iterated over circuit families, the verifier reused two scratch buffers:
|
1 2 3 4 5 6 |
let (current, previous) = if circuit_sequence & 1 == 0 { (&mut proof_output_0, &proof_output_1) } else { (&mut proof_output_1, &proof_output_0) }; |
At the end, the verifier derived the expected challenges and compared them against proof_output_0 alone. Because that buffer was reused, only the last family was actually bound to the Fiat-Shamir transcript; the others merely had to be internally consistent. A prover could therefore compose proofs that described inconsistent executions and have them accepted as a single run. A related flaw left machine-state continuity across proofs unchecked. Manual review surfaced both, and the team fixed them during the engagement. Fuzzing added two lower-severity memory-safety findings, reachable only outside Airbender’s trusted-bytecode assumption. The complete scope, methodology, and findings are documented in the full audit report.
Impact
For the 21 circuits Picus verified, Matter Labs has a proof that a large class of soundness bugs is not present.
- Determinism proven: Picus verified 21 of the 26 targeted circuits as deterministic, ruling out a large class of soundness bugs in those circuits.
- Fixes without redesign: all three criticals turned out to be one-line errors, so nothing in the architecture had to change.
- Re-runnable verification: the proofs and the harnesses built for the fixed bugs can rerun through AuditHub when the circuits or verifier change, so a regression shows up instead of slipping through.
“It’s rare to come out of an engagement with real confidence that a class of bugs is absent. Formal verification gave us that. We keep our other defenses, but we’re far more confident these soundness issues are very unlikely in the circuits that were verified.”
Antonio Locascio, Security Engineer at Matter Labs
ZK security that scales with the prover
Manual review still matters on a ZK project, and here it caught two of the three criticals. But the most common critical bug, the underconstrained circuit, is the one formal verification handles best, because the proof covers every input rather than the cases a reviewer thinks to check. The checks are also repeatable: when Matter Labs changes a circuit, the same determinism proof can run again and show whether the change broke soundness.