Matter Labs: ZKsync Airbender Tooling engagement report
Project Information
CATEGORY
Zero-Knowledge Virtual Machines (zkVM)
NETWORK
Ethereum, RISC Zero zkVM
WEBSITE
https://www.zksync.io/airbender
DESCRIPTION
From February 16, 2026 to April 15, 2026, Matter Labs engaged Veridise to conduct a security assessment of ZKsync Airbender. The security assessment covered the proving and verification components of ZKsync Airbender, a STARK based RISC V zkVM that proves RISC V execution traces through AIR circuits, a multi stage proving pipeline, and recursive verification. Veridise conducted the assessment over 21 person weeks, with 3 security analysts reviewing the project over 7 weeks. The review strategy involved a tooling focused analysis combining Picus formal verification of circuit determinism, structure aware fuzzing of executor and prover components, and targeted manual review of selected circuit and verifier logic.
Tooling Engagement Report
SCOPE
The scope of this security assessment is limited to a specific set of source files from the repository, as agreed upon with the Matter Labs developers:
Formal verification scope (Picus determinism analysis):
- cs/src/machine/ops/unrolled/decoder/decoder_circuit.rs
- cs/src/machine/ops/unrolled/add_sub_lui_auipc_mop.rs
- cs/src/machine/ops/unrolled/jump_branch_slt.rs
- cs/src/machine/ops/unrolled/load_store_subword_only.rs
- cs/src/machine/ops/unrolled/load_store_word_only.rs
- cs/src/machine/ops/unrolled/load_store.rs
- cs/src/machine/ops/unrolled/mul_div.rs
- cs/src/machine/ops/unrolled/shift_binary_csr.rs
- cs/src/machine/ops/unrolled/reduced_machine_ops.rs
- cs/src/machine/ops/add_sub.rs
- cs/src/machine/ops/binops.rs
- cs/src/machine/ops/shift.rs
- cs/src/machine/ops/mul_div.rs
- cs/src/machine/ops/load.rs
- cs/src/machine/ops/conditional.rs
- cs/src/machine/ops/store.rs
- cs/src/machine/ops/lui_auipc.rs
- cs/src/machine/ops/jump.rs
- cs/src/machine/ops/mop.rs
- cs/src/machine/machine_configurations/full_isa_no_exceptions/optimized_state_transition.rs
- cs/src/delegation/bigint_with_control/mod.rs
- cs/src/delegation/blake2_round_with_extended_control/mod.rs
- cs/src/delegation/blake2_single_round/mod.rs
- cs/src/delegation/keccak_special5/mod.rs
Prover fuzzing scope:
- prover/src/prover_stages/unrolled_prover/mod.rs
- prover/src/prover_stages/unrolled_prover/stage2.rs
- prover/src/prover_stages/unrolled_prover/stage_2_shared.rs
- prover/src/prover_stages/unrolled_prover/stage_2_ram_shared.rs
- prover/src/prover_stages/unrolled_prover/stage3.rs
- prover/src/prover_stages/unrolled_prover/quotient_parts/
Executor fuzzing covered the bytecode/VM pipeline. Targeted manual review was applied to code Picus could not verify and to core verifier composition logic.