Matter Labs engaged Veridise for a tooling-focused security assessment of ZKsync Airbender, the STARK-based RISC-V zkVM that proves execution for the ZKsync ecosystem, ahead of its V2 prover upgrade. Using formal verification to target the soundness bugs that ordinary testing cannot catch, and fuzzing for the ones it can, the engagement verified most of the prover’s circuits and found three critical issues, all since fixed.
- Veridise ran a formal-methods engagement on ZKsync Airbender, a STARK-based RISC-V zkVM.
- Picus verified 21 of 26 circuits; 3 critical soundness bugs were found and fixed.
- Formal verification proved determinism, fuzzing checked correctness, manual review caught verifier flaws.
What the engagement covered
From February to April 2026, three Veridise analysts spent 21 person-weeks on Airbender’s proving and verification components: the circuits that enforce RISC-V instruction semantics, the multi-stage STARK prover, and the recursive verifier. Picus formally verified the circuits, proving them deterministic and ruling out underconstrained soundness bugs. Fuzzing checked the prover and executor for correctness, and manual review covered the verifier composition logic.
What the assessment found
Picus verified 21 of the 26 targeted circuits as deterministic, ruling out underconstrained soundness bugs in them. It also caught one of the three criticals: a missing constraint-finalization step in the unrolled jump_branch_slt circuit left arithmetic relations unenforced, which would have let a prover forge branch outcomes and the program counter. Manual review of the verifier caught the other two, composition flaws that let proofs be checked under inconsistent challenges. All three were fixed during the engagement, and the Picus-found bug was re-verified afterward. A low-severity issue and two memory-safety warnings were acknowledged as outside the prover’s trust model.
Why it matters
For a proving system, the question that counts is whether the bugs that let a prover forge an execution have been ruled out. Across most of Airbender’s circuits, they now have been. The tools used here are available through AuditHub, and the regression harnesses built for the fixed issues rerun there as the circuits and verifier change, so the guarantees hold as the code evolves.
The view from Matter Labs
“It is rare to come out of a security engagement with real confidence that an entire class of bugs is absent. Under-constrained soundness bugs worry me most, because you cannot test your way to confidence about them. Formal verification with Picus changed that for us. We keep our other defenses, but we are far more confident these issues are unlikely in the circuits that were verified.”
Antonio Locascio, Security Engineer, Matter Labs
What is ZKsync Airbender? The Takeaway
ZKsync Airbender is a STARK-based RISC-V zkVM that proves execution for the ZKsync ecosystem. Securing it means formally verifying that its circuits are deterministic, which rules out a class of forgeable-proof soundness bugs that testing cannot reach. In a Veridise tooling engagement, Picus proved determinism across most targeted circuits and the team fixed three critical soundness flaws.
Read the full report
ZKsync Airbender Tooling engagement report_2026
Custom tooling
Securing Airbender meant building tooling around it: extraction to get its circuits into Picus, and harnesses to fuzz its prover. If your codebase needs the same kind of work and you want a second pair of eyes on your project, talk to us. You can also Request an Audit.
