Cantina x ZKsync: The 2026 Guide to Securing ZKPs

Introduction

Zero knowledge proof systems drew sustained security attention in 2025 because multiple critical vulnerabilities showed up in real implementations. When soundness fails, the verifier can accept an invalid proof, and the failure can be hard to see in production.

This guide, a collaboration between Cantina and ZKsync, walks through the most important ZK vulnerabilities disclosed in 2025. By combining Cantina’s security research with ZKsync’s experience securing over $4 billion in assets and 700 million transactions, we aim to provide practical understanding for the industry. We analyze what failed, why it failed, and how teams can build defense-in-depth strategies to prevent similar breaks in audits, on-chain safety, and zkML.

Fiat Shamir transcript failures: Solana confidential transfers

A major 2025 incident was a soundness issue in Solana’s confidential transfer stack, rooted in a Fiat Shamir transcript omission. In Solana’s ZK ElGamal Proof program, a prover controlled value that should have been absorbed into the transcript hash was not included. Researchers described this as a “phantom challenge” because it existed in the protocol state but not in the transcript used to derive challenges.

How the failure happened

In interactive sigma protocols, the verifier’s challenge is meant to be unpredictable to the prover. In the non interactive version, Fiat Shamir replaces the verifier challenge with a hash of the transcript. That only holds if the transcript includes every value that influences verification.

Solana’s implementation left out a prover supplied challenge component in a sigma OR proof. Because it was not hashed, a malicious prover could choose it in a way that makes the final verification equations pass, even though the underlying statement is false.

What assumption broke

The broken assumption was that the verifier derived its randomness from the full transcript. With the omission, the prover gained extra degrees of freedom. The verifier was no longer enforcing what the protocol designers thought it was enforcing.

This is not a subtle consequence. Transcript omissions can turn “the verifier chooses randomness” into “the prover can shape randomness.”

Why it matters

In confidential transfer systems, forged proofs can translate into unauthorized balance changes while still producing proofs that look valid. In the Solana case, the risk included bypassing fee validation, which can lead to manipulating encrypted balances in ways the system is supposed to forbid.

Solana’s response included disabling the affected functionality and patching the ZK program. The operational point is clear. If you ship proof verification in production, you need a way to shut it off when soundness is questioned, because you often cannot detect exploitation directly.

What to do in audits

Practical audit steps:

• Enumerate every challenge derived via Fiat Shamir.
• For each challenge, trace backward and confirm every prover controlled value that should influence that challenge was absorbed into the transcript first.
• Confirm the transcript has domain separation and clear ordering, so later refactors do not silently change what gets hashed.

Under constrained circuits: RISC Zero zkVM missing constraint

A second 2025 case that mattered was a critical under constraint issue in RISC Zero’s zkVM, reported as CVE-2025-52484. The core problem was a missing constraint around source register handling in the rv32im circuit.

How the failure happened

In a zkVM, the prover supplies a witness that represents an execution trace. The circuit must constrain that trace to match the VM’s intended semantics. If any semantic rule is not constrained, the prover can exploit that gap.

In this case, the circuit did not correctly constrain the scenario where an instruction’s two source registers are the same. For certain three register instructions, the circuit did not enforce that the two operands are equal when they should be. That let a prover effectively feed two different values for what should be the same register state, producing an “execution” that cannot exist in a real RISC V machine, while still satisfying the circuit.

What assumption broke

The assumption that “if the proof verifies, the program executed correctly” was no longer true. Under constraint issues break soundness in the most direct way. The prover can prove false execution traces.

In public explanations, this was illustrated with deliberately absurd arithmetic examples, such as proving a wrong division or remainder result. The exact arithmetic is less important than the point: once the prover can lie about execution semantics, the system can be made to accept arbitrary outcomes.

Why it matters

This is a full soundness failure class. If an application uses zkVM proofs as a trust anchor, then accepting a forged execution proof means accepting forged state updates, forged authorization checks, or forged computation outputs.

RISC Zero fixed the issue in later versions and took steps to contain risk for on chain verifiers. The incident is a reminder that zkVM security is not just cryptography, it is also ISA and micro semantic correctness expressed as constraints.

What to do in audits

Audit zkVM circuits like you would audit a CPU specification, but in constraint form.

Practical audit steps:

• Enumerate instruction classes and edge cases, including register aliasing, special register behaviors, division by zero, and bit width boundaries.
• Add property tests that deliberately stress those edge cases.
• Try to construct invalid witnesses that exploit aliasing or missing equality constraints. If any invalid witness verifies, treat it as a soundness incident.

Arithmetic mistakes in zkEVMs: Polygon zkEVM remainder check bug

Polygon zkEVM had a 2025 disclosure that illustrates a different but common class of ZK failures. Arithmetic gadgets that are almost correct, but miss a key invariant.

The specific issue involved division logic in the zkProver ROM, in a subroutine commonly referenced as divARITH. The implementation enforced the equality E = A * B + C but checked the wrong inequality for the remainder. It checked C < E instead of the intended C < A.

How the failure happened

Division in circuits is not just the linear equality. The remainder must be bounded by the divisor, otherwise multiple quotient and remainder pairs satisfy the equality.

With the wrong inequality, a prover can craft an alternative quotient and remainder:

• Set B' = B - 1
• Set C' = C + A

The equality still holds because A * (B - 1) + (C + A) equals A * B + C, which equals E. The flawed inequality C' < E can still hold even when C' is greater than A, so the circuit accepts the forged pair.

A concrete example used in public analysis:

• E = 101, A = 10
  
  
• Correct result is quotient 10, remainder 1
  
  
• Forged result is quotient 9, remainder 11
  
  The equality holds, the remainder bound is wrong, and the circuit accepts a mathematically invalid division.
  
  

What assumption broke

The broken assumption is that the circuit enforces the full division specification, not just a convenient identity. In ZK, missing a range check is missing the statement itself.

Why it matters

In a zkEVM, arithmetic gadgets underpin EVM semantics. If a prover can falsify division or modulo constraints, they can potentially manipulate downstream logic, including fee logic, rewards, accounting, or opcode semantics. In a rollup context, this can translate into invalid state roots being accepted on Layer 1.

Polygon fixed the issue by enforcing the correct bound, C < A. The lesson is not about division specifically. It is about every “obvious” invariant that developers assume without constraining.

What to do in audits

For every arithmetic gadget, write down the complete specification in math and enforce it.

Practical audit steps:

• For division, enforce both E = A * B + C and 0 ≤ C < A, plus edge case handling for A = 0 if relevant.
• For comparisons and range checks, ensure constraints actually bind bit length and do not rely on implicit assumptions.
• Add adversarial tests that attempt to satisfy the equality while violating the bound, exactly like the crafted B' and C' pair above.

Lookup table soundness: Plonky2 padding bug, CVE-2025-24802

Plonky2 had a 2025 soundness issue involving lookup tables, tracked as CVE-2025-24802. The issue was tied to how lookup tables were padded when their length was not divisible by a gate dependent factor (commonly cited as 26 in public writeups).

How the failure happened

Lookup tables are used to constrain that a pair (x, y) belongs to a defined mapping. To fit polynomial commitments, tables may be padded.

In Plonky2’s case, padding behavior could introduce an unconditional (0, 0) entry. That means the lookup constraint would accept the claim “f(0) = 0” even if the table’s intended mapping did not include that pair.

What assumption broke

The assumption that padding is semantically neutral. Padding is only safe if it does not add new valid mappings. Introducing a new mapping is a soundness change.

Why it matters

Any circuit using a lookup to constrain behavior can be undermined if the prover can route part of the computation through the padded entry. In many real circuits, a forced (0, 0) entry might not be exploitable because f(0) is already 0 or because other constraints prevent that path. In others, it can become an exploit lever.

The fix in the patched version changed padding to repeat an existing entry rather than introducing a new mapping. That avoids adding new admissible pairs.

What to do in audits

Treat lookup gadgets as part of the proof system’s soundness surface.

Practical audit steps:

• Review how tables are sized and padded.
• Confirm padding does not introduce new valid pairs.
• Test boundary lengths and adversarial inputs, including zero, to ensure there is no “free pass” path.

Other notable ZK vulnerabilities and research (relevant patterns)

The incidents above are the headline cases because they involve direct soundness breaks in widely discussed stacks. They also mirror recurring bug classes that show up across ZK ecosystems.

Unconstrained signals: Circom MiMC and Tornado Cash class bugs

A classic Circom failure mode is “assigned but not constrained.” In Circom, = assigns a value, it does not create a constraint. The constraint operator is <==. A known class of bugs involved using = where <== was intended, causing outputs to be computed in code but not constrained to match the computation.

In the MiMC hash context, an unconstrained output can let a prover set the hash output arbitrarily while still satisfying the circuit, because the circuit never binds the output to the inputs. In a mixer style protocol, that can turn into the ability to fake Merkle roots or satisfy withdrawal checks improperly.

The fix is simple, but the implication is not. One unconstrained wire can invalidate the security property the circuit is meant to enforce.

Overflow and bit length assumptions: Halo2 modulo overflow class (Scroll example)

Another recurring class is missing overflow constraints when implementing arithmetic intended to be bounded, such as 256 bit EVM arithmetic, inside a field where arithmetic is modulo a prime.

A reported class of issues in zkEVM style circuits involved modular arithmetic gadgets where the prover could exploit the lack of a “no overflow beyond 2^256” constraint. By selecting large multiples, the prover can satisfy the field equation while violating the intended 256 bit interpretation, effectively creating false “mod” results.

These bugs look like math edge cases, but they are statement edge cases. If the circuit is meant to model 256 bit arithmetic, it must constrain values to 256 bit ranges at every step that matters.

Nondeterminism and nullifier representation

Privacy systems often rely on nullifiers to prevent double spends. If the circuit allows multiple representations of the same logical nullifier, or does not constrain bit length tightly, it can create nondeterminism where the same note can be nullified twice under different encodings. Even when no exploit is publicly confirmed, these patterns show up repeatedly in audits because they are easy to miss in circuit design.

Fiat Shamir variants: Frozen Heart and related transcript mistakes

Beyond outright omissions like the Solana case, there is a broader family of Fiat Shamir mistakes that show up across libraries and constructions. The Frozen Heart class describes situations where not all public inputs or commitments are hashed into the transcript, enabling the prover to vary an unbound value while still producing a valid proof. Variants include “last challenge” style mistakes where a final challenge is not binding on all earlier messages due to transcript ordering or incomplete absorption.

The audit stance is consistent across stacks. If a value is public, or affects verification, it must be transcript bound. If you cannot explain why it is safe not to bind it, treat it as a bug until proven otherwise.

Newer ecosystems: Noir, Cairo, and emerging stacks

By early 2026, newer ZK languages and systems, such as Noir and Cairo based systems, did not have public soundness incidents on the same scale as the four main cases above. That does not mean they are immune. The same failure modes apply. Missing constraints in a compiler lowering step, in an AIR definition, or in a gadget library can still yield soundness breaks. For these stacks, rigorous testing and independent review matter because the tooling and patterns are still maturing.

Securing Critical Infrastructure: ZKsync Case Study

The industry failures outlined above highlight the necessity of deep inspection at the primitive level. ZKsync stands out as a clear example of how to build and secure a high-performance proving stack while mitigating complexities.

ZKsync has deployed a cryptography-first network securing over $4 billion in assets and processing over 700 million transactions. Their infrastructure, including the ZK Stack and the Airbender Prover, is designed to support programmable capital markets and tokenized assets with Ethereum finality.

ZKsync applies a defense-in-depth security model:

• Open-source codebase, independently audited
  
  
• $1.1M bug bounty program
  
  
• Role-based access controls and permission frameworks
  
  
• Production-proven ZK proof systems with millions of validated transactions

To avoid the soundness pitfalls common in other protocols, ZKsync engaged Cantina for a targeted security audit of their core cryptographic components. This engagement focused on the snark-wrapper, era-boojum, and rescue-poseidon primitives.

Why this matters for soundness:

• Constraint Correctness: The engagement validated the SNARK compression layer. This prevents the "missing constraint" bugs seen in other zkVMs by ensuring the compression step does not lose semantic rules.
• Primitive Integrity: By auditing rescue-poseidon and era-boojum, the review ensured the underlying arithmetic and hash gadgets functioned exactly as specified, protecting against the bit-length and overflow issues that plague modular arithmetic.
• Proof Verification: The audit verified the integrity of the cryptographic primitives that underpin the ZK stack. By securing snark-wrapper and specific boojum components, the engagement established a verified baseline for the proving infrastructure, ensuring the core mathematical operations are sound.

Real world implications for protocols

On chain token protocols

Solana’s incident is a clean warning for any chain integrating ZK features such as confidential transfers or shielded assets. A soundness bug in proof verification can become unbounded minting or theft without any key compromise. Recovery is hard, and detection can lag. Teams need operational controls that allow disabling or upgrading ZK verification paths quickly.

ZK rollups and Layer 2 systems

The Polygon and related zkEVM bugs show that a rollup’s security reduces to circuit correctness. If the proving system can be tricked, Layer 1 will accept invalid state roots. That can lead to stolen funds, inconsistent balances, or irreversible bad state.

Rollup teams should invest in:

• circuit level fuzzing and differential testing against reference EVMs,
• formal methods for high risk arithmetic and state transition gadgets,
• operational safeguards while the stack is still evolving, including emergency stop paths and clear incident playbooks.

Privacy systems and mixers

For mixers and shielded pools, soundness breaks can enable theft, double spend, or privacy set degradation. Circuits in this space are often small enough to be good targets for formal verification and exhaustive testing. Bounties here should pay for proof level issues, not just smart contract issues, because the proof layer is the enforcement layer.

zkML

zkML is still early, but it inherits ZK risks and adds ML specific ones:

• model binding, prove against a committed model, not a model name,
• preprocessing binding, the proof must cover tokenization and normalization,
• numeric edge cases, quantization and truncation can create mismatches between “proved” math and deployed inference,
• parameter hygiene, avoid weakening security parameters to meet latency targets.

A zkML proof that is not tightly bound to the model and full computation is a proof of something else, often something the verifier did not intend.

Strengthening ZK security: recommendations and strategies

Exhaustive circuit auditing

For ZK systems, audits need to cover the full boundary:

• circuit constraints,
• transcript construction,
• witness generation,
• verifier integration,
• serialization formats,
• upgrade and emergency controls.

Checklist items that repeatedly matter:

• no unconstrained outputs,
• complete range checks and bit length constraints,
• equality constraints where indices can alias (registers, memory slots, nullifiers),
• full transcript absorption for every prover controlled value that influences challenges,
• safe lookup table sizing and padding behavior,
• safe aggregation and recursion interfaces, including cross field conversions.

Testing and fuzzing

Unit tests are not enough. You need adversarial tests that assume a malicious prover:

• property tests on edge cases,
• witness mutation tests that try to keep verification passing while breaking the intended statement,
• differential tests against reference implementations.

If a circuit accepts an invalid witness, treat it as a soundness incident, not as a “test failure.”

Formal verification

Formal methods are increasingly relevant for circuits that anchor large amounts of value. The payoff is real. Formal specs for arithmetic gadgets, range constraints, and core state transition invariants can eliminate entire bug classes, including “almost correct” division, modulo, and overflow logic.

Runtime monitoring and failsafes

MDR for ZK systems is rarely about spotting an invalid proof. It is about spotting impossible outcomes:

• sudden invariant drift (supply, pool totals, accounting identities),
• abnormal proof verification patterns (fail rates, size distributions, submission bursts),
• unexpected state transition shapes (rare opcodes, unexpected roots, unusual withdrawal patterns).

These are safety nets. They do not replace soundness, but they can limit blast radius when something breaks.

Bug bounties and community engagement

2025 reinforced that independent researchers find real ZK bugs. Programs should explicitly scope:

• prover and verifier code,
• transcript logic,
• circuits and gadgets,
• aggregation and recursion systems.

Reward proof level soundness bugs at the same severity as contract bugs that mint funds. For many protocols, they are the same class of risk.

Cantina’s proactive monitoring

For teams operating ZK systems, proactive checks help:

• canary tests in staging that attempt known invalid proofs,
• continuous regression tests for transcript and serialization logic,
• monitoring for invariant drift in production,
• incident playbooks that include disabling ZK dependent features and rotating verification keys when applicable.

This is operational security applied to proof verification.

Expanding the ZKP Landscape: What Systems Are We Securing

Zero-knowledge proofs now support a broad range of applications across blockchain infrastructure and protocol design. At Cantina, our security programs cover systems such as:

• zkRollups that compress Layer 2 execution into verifiable Layer 1 proofs.
• zkBridges that authorize cross-chain asset transfers through succinct validation.
• zkVMs that encapsulate smart contract execution within provable computation circuits.
• ZK identity protocols that manage selective disclosure, nullifier logic, and private attestations.
• ZK machine learning systems where inference outputs are encoded and verified within circuits.
• Privacy-preserving voting protocols that rely on nullifiers, encrypted inputs, and eligibility proofs.
• Light clients that verify block headers and state updates from external chains using ZKPs.
• Web2 social media platforms implementing age verification through ZKPs.
• Gaming applications using ZKPs for fair matchmaking and anti-cheat systems.
• Traditional enterprise systems leveraging ZKPs for secure data sharing.

Each of these systems introduces unique constraints and input domains. They are built on shared proof principles but implemented in distinct ways.

Closing

These disclosures gave the industry concrete failure modes:

• transcript omissions break Fiat Shamir,
• missing constraints break zkVM and circuit soundness,
• incomplete arithmetic specs break zkEVM correctness,
• unsafe padding breaks lookup soundness.

If you are building with zero knowledge and your protocol demands security that holds under pressure, we are ready to review it. We are available 24/7 to scope a high signal audit or design the best security program that fits your protocol’s needs. Contact us today.