How Zero-Knowledge Broke in Real Life: Under-Constrained Circuits and the Bugs That Minted Money

1. A Proof of Something That Was Not True#

In June 2025, security researchers sent Solana's engineers a quiet, alarming message. The blockchain's on-chain ZK ElGamal Proof program -- the component that checks zero-knowledge proofs behind Token-2022 confidential transfers -- would accept a proof of something that was not true. The post-mortem stated the consequence plainly: a sophisticated attacker could forge a proof enabling "minting unlimited tokens or draining a victim's confidential balance" ^[1].

No elliptic curve had been solved. No hash had been reversed. The discrete logarithm was exactly as hard the morning after as the morning before. What went wrong was smaller and stranger than any of that. In the program's own words, "a component was not included in a hash used to generate a transcript for the Fiat-Shamir Transformation" ^[1]. One algebraic value was left out of a single hash, and that omission was enough to forge a proof the verifier would wave straight through.

"...minting unlimited tokens or draining a victim's confidential balance ... There is no known exploit." -- Solana ZK ElGamal Proof program post-mortem, June 2025

Read the last clause of that quote carefully, because it governs everything that follows. There is no known exploit ^[1]. The bug was reported and disclosed responsibly, confidential transfers were disabled on June 11, and the proof program itself was disabled at the start of mainnet-beta epoch 805 on June 19 ^[1]. The feature was still in testing, and no real funds moved. This was a near-miss, not a heist.

That distinction -- between a proof of a true thing and a proof the verifier merely accepts -- is the property under attack in every incident here. When it fails, we say the system has lost soundness.

Here is the thesis in miniature, and it inverts the headline you would expect. Solana's flaw is not an anomaly -- it is the signature of how zero-knowledge breaks in real life. Picture the system as two layers. Underneath sits a cryptographic hardness floor: the discrete-log-type and pairing-based hardness assumptions -- formally argued in the generic group model -- together with the collision-resistant hashes that proofs rest on.

Stacked on top is a human-built artifact: the construction, the circuit, the verifier, the transcript. In every publicly disclosed failure, the floor held. The artifact above it leaked. And where that artifact guarded a rollup or a bridge, the leak was denominated in money.

This piece is the documented record of that pattern -- the empirical mirror of its structural sibling, A Valid Proof of a False Thing, which derives why these proofs can break, and a companion to Never Decrypted: Proving You Ran the Computation, which shows how the proof systems are built in the first place. Here we do neither the derivation nor the construction. We read the ledger.

No cryptography broke -- so what, exactly, did? To answer that, we have to go back to the first time real money sat behind a shipping zero-knowledge system.

2. The First Silently Forgeable Proof#

On March 1, 2018, Ariel Gabizon -- a cryptographer then at the Electric Coin Company, which builds Zcash -- found something disquieting in the paper Zcash had launched on. The privacy coin's proving system was a variant, known as BCTV14, of an earlier protocol called Pinocchio ^{[2, 3]}. Gabizon discovered "a subtle cryptographic flaw" in it ^[4]. Not in the hardness of the pairings the proofs relied on, but in the construction wrapped around them.

The flaw was specific. Pinocchio's template deliberately left certain elements out of its public parameters; the BCTV14 variant put some of them back. Gabizon's write-up names the mechanism exactly: the construction included "redundant elements in the CRS ... which are vital not to expose," and their exposure let a prover create "a proof of knowledge for any public input given a valid proof for some public input" ^[5]. In plain stakes, that is counterfeiting -- forging shielded Zcash out of nothing. The assigned CVE puts the consequence in a single sentence ^[6].

"...transform the proof of one statement into an ostensibly valid proof of a different statement, thereby breaking the soundness of the proof system." -- CVE-2019-7167

The company found no evidence anyone had used it. The bug was patched silently by the Sapling network upgrade, which activated on October 28, 2018, and disclosed publicly on February 5, 2019 ^[4]. The vulnerability ran on two clocks. It was exploitable for roughly two years -- from the Sprout launch in October 2016 until Sapling closed it on October 28, 2018 -- but secret for only about eleven months, from Gabizon's March 2018 discovery to the February 2019 disclosure ^[4]. A long window of exposure, a short window of concealment. The first near-miss in a long line.

Zcash teaches the shape of the entire record. Separate two things that are easy to blur. Underneath any real proof system sits a hardness floor -- named, well-studied assumptions like the discrete logarithm and elliptic-curve pairings. A pairing here is the verifier's tool, the operation that checks the proof equation, not itself a hardness assumption. A Groth16-style SNARK's soundness is argued in the generic group model, an idealized setting in which the adversary may only combine group elements through the allowed operations ^[7].

On top of that floor, humans build an artifact: the construction, the circuit, the verifier, the transcript. Gabizon's flaw did not touch the floor. It lived in the construction -- the topmost, most human layer -- and his fix confirms the diagnosis: the corrected BCTV14 is provably sound "in the generic group model, when these elements are excluded from the CRS" ^[5]. The math was fine; the wiring around it exposed something it should not have.

flowchart TD
A1["Construction: CRS and proof-system wiring"] --> A2["Circuit: the statement compiled to field constraints"]
A2 --> A3["Verifier: the on-chain proof-checker"]
A3 --> A4["Transcript: the Fiat-Shamir challenge hash"]
A4 --> F1
subgraph FLOOR["Hardness floor (generic group model) -- unbroken in every disclosed case"]
F1["Discrete-log and pairing hardness, plus collision-resistant hashes"]
end

The same shielded-Zcash counterfeiting signature returned almost exactly eight years later, one artifact layer down. In late May 2026, Taylor Hornby, working for Shielded Labs, found an under-constrained element in the newer Orchard circuit -- the shielded pool that succeeded Sapling -- that made it "possible to put arbitrary false inputs into an elliptic curve multiplication and still have the multiplication check pass" ^[9]. A complete exploit generated "unlimited, undetectable counterfeit ZEC" in a local regtest ^[10].

The gap had been latent from Orchard's activation in May 2022 until an emergency fix on June 1, 2026 -- roughly four years -- and because Zcash's privacy hides transaction values, there is "no definitive way to determine using only cryptography whether such exploitation occurred" on mainnet ^[10]. A near-miss that rhymes with 2018 down to the coin, and -- as Section 3 will show -- a textbook case of a bug you cannot test for, because the flaw is a constraint that was never written. The 2026 Orchard bug sits in a different layer from the 2018 flaw -- 2018 was a redundant-CRS construction bug, 2026 an under-constrained circuit gadget -- but the coin and the consequence are identical: counterfeit shielded ZEC from nothing. The discovery was AI-assisted, through a targeted review of the Orchard circuit ^[9]. It stays a near-miss: proven in regtest, never confirmed on mainnet ^[10].

Two catalogs make the rest of this record legible, and both recur below. The first is the 0xPARC ZK Bug Tracker, the canonical community catalog of zero-knowledge bugs found in the wild, with its own taxonomy of failure modes ^[8]. The second is the academic corpus: a 2024 systematization by Chaliasos and colleagues that analyzed 141 real-world SNARK vulnerabilities and asked what patterns they share ^{[11, 12]}. Between them, they let us treat "how zero-knowledge breaks" as an empirical question with an answerable shape.

flowchart LR
Z["2018-19: Zcash counterfeiting -- construction"] --> D["2021: Dark Forest range check -- circuit"]
D --> AZ["2022: Aztec 0-bug -- verifier"]
AZ --> FH["2022: Frozen Heart -- transcript"]
FH --> B["Oct 2022: BNB Token Hub -- adjacent Merkle verifier, CONFIRMED THEFT"]
B --> S["2025: Solana ZK ElGamal -- transcript, near-miss"]
S --> VG["Feb 2026: Veil Cash / FOOMCASH -- Groth16 verifier key, EXPLOITED then RECOVERED"]
VG --> V["early 2026: six zkVMs -- transcript, near-miss"]
V --> OR["June 4 2026: Zcash Orchard -- circuit, near-miss"]
OR --> AC["June 14 2026: Aztec Connect -- circuit + settlement, CONFIRMED THEFT"]
AC --> HK["July 3 2026: Hinkal -- verifier integration, REPORTED"]

Zcash's flaw was exotic -- a redundant element buried in a trusted setup. It would have been comforting if that were the whole story. Instead, as zero-knowledge spread from one coin to thousands of applications, the same kind of bug appeared everywhere -- and in a form so ordinary it hid in plain sight.

3. The Constraint That Was Never Written#

Dark Forest is a fully on-chain, real-time strategy game -- a galaxy of planets settled on Ethereum, where players keep their coordinates secret and prove in zero knowledge that each move is legal. A move requires showing that a target coordinate lies inside the map's bounds without revealing where it is. Dark Forest's circuit did this with a RangeProof built on a standard library comparator ^[13]. The comparator looked right. It was not, and the bug was flagged by Daira Hopwood ^[8].

The subtlety is that a proof does not certify that a statement is true. It certifies that some witness satisfies the constraints that were actually written. If the constraints permit a witness the designer never intended, the proof will happily certify it.

The smallest illustration fits in one line. Suppose a circuit constrains $y \cdot y = x$ and treats $x$ as the output. Over a prime field, that equation has two solutions for most $x$: both $y$ and its negation satisfy it. The output does not determine $y$. That non-uniqueness -- one input, more than one satisfying witness -- is the algebraic signature of every under-constrained circuit.

// A tiny field: the integers modulo a small prime.
const p = 23;
const mod = (a) => ((a % p) + p) % p;

// A constraint that only says: y * y === x  (mod p).
// It pins down x from y, but never pins down which root y is.
const x = 9;

// Search the whole field for values of y that satisfy the constraint.
const witnesses = [];
for (let y = 0; y < p; y++) {
if (mod(y * y) === x) witnesses.push(y);
}

console.log('Constraint: y*y === ' + x + ' (mod ' + p + ')');
console.log('Witnesses that satisfy it: ' + witnesses.join(', '));
console.log(witnesses.length + ' distinct witnesses, so the output does NOT determine y.');
// Both 3 and 20 (which is -3 mod 23) pass. The circuit is under-constrained.

Dark Forest's bug was this same shape, dressed in a range check.

Dark Forest v0.3 built its RangeProof on CircomLib's LessThan(n) comparator ^[13]. That gadget is only correct when its inputs are already known to fit in n bits -- it assumes the bound but does not enforce it.

The circuit never constrained its inputs to n bits, so an attacker could feed an oversized field element whose low bits looked in-range and satisfy a RangeProof for an out-of-range coordinate. The fix was to add Num2Bits bit-length checks on both inputs, forcing them into range before the comparison ^[14]. In Circom the assignment operators are not interchangeable. <== both assigns a value and adds a constraint tying it to the equation, while <-- and = only assign, producing a witness value with no constraint attached. A signal written with <-- and never separately constrained is invisible to the proof -- the classic way an intended constraint goes missing.

// CircomLib's LessThan(n) is only correct when BOTH inputs are < 2^n.
// It decides a < b from the low n bits. If a caller forgets to constrain
// the inputs to n bits (no Num2Bits), the gadget can be fooled.

const n = 8;          // designed for values in 0..255
const bound = 100;    // we want to prove: secret < 100

function lessThan_nbits(a, b) {
const mask = (1 << n) - 1;            // only the low n bits are meaningful
return (a & mask) < (b & mask) ? 1 : 0;
}

const honest = 42;            // a legitimate in-range coordinate
const oversized = 256 + 42;   // 298: same low 8 bits as 42, but out of range

console.log('LessThan says 42 < 100  : ' + lessThan_nbits(honest, bound));    // 1, correct
console.log('LessThan says 298 < 100 : ' + lessThan_nbits(oversized, bound)); // 1, FALSE but accepted
console.log('298 is out of range, yet the range proof passes.');
console.log('The forgotten Num2Bits(8) on the input is the missing constraint.');

flowchart TD
IN["Attacker supplies an oversized field element as the coordinate"] --> RP["RangeProof calls LessThan(n) on the input"]
RP --> ASSUME{"Is the input constrained to n bits?"}
ASSUME -->|"No Num2Bits check (the bug)"| WRONG["LessThan reads only the low n bits, returns in-range"]
ASSUME -->|"Num2Bits added (the fix)"| RIGHT["Oversized input rejected before comparison"]
WRONG --> ACCEPT["Verifier accepts a proof for an out-of-range value"]

Now sit with why this is so hard to catch.

You cannot unit-test the presence of a constraint you forgot to write. A test feeds the circuit an input, computes a witness, and checks that a valid proof results -- and it always does, because the illegitimate witnesses live in exactly the space the missing equation was supposed to forbid. Every positive test passes. The bug is an absence, and absences do not appear in a test that only exercises what is already there.

This was no one-off. The same absence recurs across production libraries -- unbounded remainders, unchecked range gadgets, and more -- catalogued in the next section ^[8].

Different libraries, same shape: a value assigned but never pinned down. All of these were near-misses -- audit-caught or disclosed before any exploitation. But the pattern was now visible, and it was not going away.

The comforting response is "audit harder." Yet a missing constraint is an absence, and absences do not live in one place. To defend against them, you first have to see the whole artifact they can hide in.

4. Three Ways to Accept a Lie#

If a circuit can forget a constraint, what else can? Walk up the artifact and each layer has its own way of certifying something false. There are three: the circuit, the verifier, and the transcript. Each has a signature failure, and each disclosed failure is the reason the next defense exists.

flowchart TD
L1["Circuit layer: Dark Forest, Aztec nullifier, MACI -- a missing constraint or range check"] --> L2["Verifier layer: Aztec 0-bug, BNB Merkle -- the proof-checker itself accepts a forgery"]
L2 --> L3["Transcript layer: Frozen Heart, Solana, zkVMs -- the Fiat-Shamir hash binds too little"]

The circuit forgets a constraint#

This is the dominant class -- the $y \cdot y = x$ intuition, generalized across production code. Once you know to look for an absence, you start to find it everywhere:

• BigInt arithmetic. A BigMod template left its output remainder unbounded, so the "remainder" could exceed the modulus ^[8].
• Circom-Pairing. The library never checked the outputs of its BigLessThan range checks -- Veridise's "million-dollar bug caught early," found during an audit before the code reached mainnet ^[15].
• MACI 1.0. An under-constrained vote-validity check would have let a coordinator quietly censor targeted votes ^[8].
• MiMC. A hash value was "assigned but not constrained" -- = where <== was required ^[8].
• ZK Email. An under-constrained circuit enabled email-address spoofing ^[8].
• PSE, Scroll, and Polygon zkEVMs. The same family surfaced as missing-constraint and unbounded-remainder findings inside production rollup circuits ^[8].

The most vivid of the set is Aztec's nullifier bug. In Aztec 2.0, "the field element representing this position was not actually constrained to be 32 bits," a gap that would "allow the attacker to spend the same input multiple times" ^[16]. A double-spend, produced by a single missing bit-length constraint. The 0xPARC catalog does not date its individual entries, so several years in this under-constrained cluster are approximate -- Dark Forest around 2021, the rest grouped roughly 2021 to 2023 ^[8]. The dates are soft; the pattern is not.

Every one of these is an absence. Every one was a near-miss -- caught in an audit or disclosed before exploitation. Not every "missing range check" is a soundness bug, and the distinction sharpens the point. Semaphore and its Zk-Kit dependency once shipped without a check that a proof input was smaller than the SNARK scalar-field order ^{[17, 18]}. But that check was in the smart contract, and its absence produced "a group that will always fail verification" -- valid proofs rejected, a group rendered unusable ^[8]. That is a completeness or liveness failure -- a denial of service -- not a soundness forgery, and it was fixed by adding the missing bound ^[19]. It belongs one layer up from the circuit-soundness absences in this section, and naming it that way is what keeps "every failure here is a soundness failure" honest.

The verifier itself is wrong#

Aztec's PlonK verifier, written in C++, accepted forged proofs when two proof elements were set to zero. The code recognized 0 as "not on the curve" yet did not reject it, then re-interpreted that same 0 as the point at infinity, which satisfied the final pairing equation. A point-at-infinity and zero-encoding inconsistency, living in the checker rather than in any circuit ^{[20, 8]}.

February 2026 then put that warning on-chain twice, in the first two known exploits against live zero-knowledge verifiers. Neither touched the circuit, the pairing, or the curve. Both hit a trusted setup that was never finished.

Veil Cash, a Base privacy pool, deployed a Groth16 verifier at 0x1e65c075989189e607ddafa30fa1a0001c376cfd whose verification key had delta2 == gamma2: both were the BN128 G2 generator point ^{[21, 22]}. In Groth16, $\gamma$ and $\delta$ play different roles and must be independent. DARKNAVY states the consequence directly: with delta == gamma, the proof element C can cancel the public-input term, letting an attacker make the pairing equation pass "for ANY public inputs without any witness" ^[21].

Using fabricated nullifier hashes across 29 withdrawals of 0.1 ETH, an actor drained 2.9 ETH of the roughly 4.5 ETH sitting in the legacy pools ^{[21, 22]}. The Groth16 mathematics held; the deployed verification key was wrong.

flowchart TD
A["Developer runs the snarkjs setup but skips Phase 2, the delta contribution"] --> B["Verification key ships with delta and gamma both the G2 generator placeholder"]
B --> C{"Does the pairing check still depend on the public inputs?"}
C -->|"delta equals gamma (the bug)"| D["Pairing equation collapses into a tautology"]
D --> E["Attacker forges a proof for any public inputs, with no witness"]
E --> F["Mixer pays out: 29 forged withdrawals drain the pool"]
C -->|"Phase 2 run, delta randomized (the fix)"| G["Forged proof rejected"]

Where does an identical, on-chain-verifiable mistake come from twice in one week? zkSecurity traced the shared root cause to the tooling. Both projects used Circom with snarkjs, and in both "something went extremely wrong in the setup phase ... They simply didn't have any contributions to the second phase of the setup ceremony" ^[23]. snarkjs initializes a new key with gamma2 and delta2 set to the same placeholder -- the G2 generator -- and expects the developer to run snarkjs zkey contribute, the Phase-2 step that randomizes delta while leaving gamma alone.

Skip that one step and the key ships with delta = gamma = G2 generator, collapsing the pairing check into a tautology ^[23]. The bug is a missing ceremony step with a valid-looking default, which is exactly why it survives testing: honest proofs verify perfectly. zkSecurity shows the tell in one line -- run the snarkjs quick-start without the contribution step and jq '.vk_gamma_2' and jq '.vk_delta_2' print the identical BN254 generator ^[23]. A reviewer who compares those two points catches the collapse before the verifier ever holds value.

Six days after Veil Cash, the identical bug was pointed at FOOMCASH, a larger "ZKProof-powered" lottery whose Groth16 verifier had shipped on both Ethereum and Base with gamma and delta set to the same point ^{[24, 25]}.

QuillAudits puts the exposure at about $1.3M in FOOM on Ethereum plus about $316K on Base -- roughly $1.6M by that accounting -- drained by algebraically forged proofs "without possessing any legitimate deposits or private witness"; other trackers report the gross across both chains as high as about $2.26M ^{[24, 26]}. CertiK diagnosed the delta2 == gamma2 collapse within hours, and BlockSec flagged the event as a "copycat" imitation of Veil Cash -- a published post-mortem turned into an attack blueprint inside a week ^[26].

Here the disposition tag matters as much as the mechanism, and it is the reason this cluster gets its own tier. Neither drain was a permanent theft. Veil Cash's funds were recovered in full: Decurity rescued the remaining pools, and the original actor returned the 2.9 ETH unprompted ^[26]. FOOMCASH was substantially white-hat-rescued -- about $1.84M, roughly 80 percent of the $2.26M gross -- and whether it was ever malicious is disputed across the primaries: zkSecurity states flatly that "some websites reported the issue as an attack, which was not the case," while QuillAudits frames the same event as a drain ^{[23, 24, 26]}.

What no source disputes is that a broken verifier moved real money on-chain. Tag both exploited-then-recovered -- a distinct middle tier, neither a clean near-miss nor a permanent theft. And note what the cluster does to the thesis: it sharpens it. No curve broke and no Groth16 theorem failed; the deployed verification key violated the $\gamma \ne \delta$ separation the theorem assumes, so this is a verifier mismatch, not a pure in-circuit under-constraint.

"The first two known exploits against live ZK circuits happened in the past week ... some websites reported the issue as an attack, which was not the case." -- zkSecurity, "The Groth16 Trusted Setup Exploit," 2026

On October 6, 2022, a verifier-layer failure produced the largest confirmed on-chain theft in this record -- and the largest ever traced to a proof-verification bug, one layer over from any zk-SNARK. The BNB Chain Token Hub bridge relied on a precompiled contract that verified IAVL Merkle inclusion proofs, a Cosmos-SDK proof format. As samczsun's analysis showed, the verification code validated the Merkle path against only one branch and skipped lpath.Right, letting an attacker splice in an empty "phantom node" so that a crafted proof reproduced the expected root and certified a cross-chain deposit that had never happened ^{[27, 28]}.

The forgery minted roughly 2,000,000 BNB, nominally around $566 to $586 million; validators halted the chain before most of it escaped, limiting the funds bridged off BNB Chain to an estimated $100 million and up ^[29]. The figure of about 2,000,000 BNB minted is consistent across write-ups; the nominal dollar value (~$566 to $586 million) and the amount successfully moved off-chain before the halt (reported between roughly $100 and $127 million) vary by source ^[29].

flowchart TD
A["Attacker crafts a deposit that never happened"] --> B["Builds an IAVL Merkle proof for it"]
B --> C["Splices in an empty phantom leaf node"]
C --> D{"Does the verifier check both branches of the path?"}
D -->|"Skips lpath.Right (the bug)"| E["Crafted proof reproduces the expected root"]
E --> F["Bridge certifies the deposit, mints about 2,000,000 BNB"]
D -->|"Checks both branches (the fix)"| G["Forged proof rejected"]

That was, and remains, the largest confirmed theft in this record. On June 14, 2026, a newer confirmed theft reached a zero-knowledge circuit. An attacker drained about $2.19 million from a deprecated, immutable Aztec Connect contract, RollupProcessorV3, in one atomic transaction ^{[30, 31]}. SlowMist's forensic post-mortem names the mechanism a ZK-rollup settlement-boundary bypass ^[30].

The shape is worth tracing. The rollup's proof committed to 32 public-input slots, but the Layer-1 settlement contract processed only the first, indexed by an attacker-controlled numRealTxs value read straight from calldata with no on-chain constraint ^{[30, 32]}. Between the two counts sat a gap of unused slots, and SlowMist says the circuit constraint that gap slots' publicValue should be zero was "either bypassed or not imposed" ^[30].

So the attacker packed the gap with forged deposits, minted unbacked balance across fourteen processRollup calls -- seven mints, then seven withdrawals -- and cashed it out as real ETH, DAI, and wstETH ^{[30, 32]}. SlowMist's summary is the thesis in a sentence: "when the ZK circuit constraint is missing, the L1 contract layer also fails to detect the issue" ^[30].

flowchart TD
A["Attacker sets numRealTxs from calldata, no on-chain constraint"] --> B["ZK proof commits all 32 public-input slots"]
A --> C["L1 settlement loop traverses only the first slot"]
B --> D{"Circuit forces gap-slot publicValue to zero?"}
D -->|"Either bypassed or not imposed"| E["Gap slots 2..32 carry forged deposits"]
E --> F["Mint unbacked L2 balance across 14 processRollup calls"]
F --> G["Withdraw real ETH, DAI, wstETH from L1"]
D -->|"Constraint present (the fix)"| H["Gap slots forced empty, forgery rejected"]

The verifier can be wrong on its own. But there is a third layer, subtler than either the circuit or the checker -- the one that turned Solana's proof into a forgery, and the one with the longest history of quietly re-shipping.

The transcript hashes too little#

That last clause is the whole ballgame.

sequenceDiagram
participant P as Malicious prover
participant H as Fiat-Shamir hash
Note over P,H: Weak FS hashes the commitment but omits a public value
P->>H: Send commitment only
H->>P: Challenge derived from too little
P->>P: Vary the omitted public value, recompute
Note over P: Grind until the challenge suits a false statement
P->>H: Submit forged proof
Note over P,H: Strong FS binds statement plus all public inputs, blocking the grind

In April 2022, Trail of Bits published a coordinated disclosure of exactly this mistake across three different proof systems -- Girault's proof of knowledge, Bulletproofs, and PlonK ^[34].

"We've dubbed this class of vulnerabilities Frozen Heart. The word frozen is an acronym for FoRging Of ZEro kNowledge proofs." -- Trail of Bits, April 2022

The Bulletproofs instance was especially telling: it "stem[med] from a mistake in the original academic paper," whose authors had recommended an insecure Fiat-Shamir implementation that omitted a Pedersen commitment from the hash ^{[35, 36]}. That is the instance the class's CVE was filed against: CVE-2022-29566 names the Bulletproofs 2017/1066 paper, which "mishandles Fiat-Shamir generation because the hash computation fails to include all of the public values" ^{[37, 38]}. The PlonK instances shared the same shape, leaving public inputs out of the transcript ^[39]. The pitfall was not new. Bernhard, Pereira, and Warinschi had drawn the weak-versus-strong distinction a decade earlier and shown that the weak form broke the Helios electronic-voting system ^[40]. The same one-line omission then recurs across four eras: Helios in 2012, Frozen Heart in 2022, Solana in 2025, and six zkVMs in 2026.

This was a proactive disclosure: affected parties were notified and had remediated before publication. A near-miss, class-wide.

How common is the class? A peer-reviewed systematization by Dao, Miller, Wright, and Grubbs surveyed open-source code and found 36 weak Fiat-Shamir implementations affecting 12 different proof systems ^[41]. Not an anecdote -- a recurring omission with a name.

And here the article's opening snaps shut. The Solana ZK ElGamal bug from June 2025 was this exact root cause: a component left out of the Fiat-Shamir transcript hash, following an earlier instance in the same program reported that May ^{[1, 42]}. But the story did not stop at Solana. In early 2026 -- March, by the disclosure timeline that runs from the first report in September 2025 -- OtterSec published "Unfaithful claims: breaking 6 zkVMs," reporting the same omission one layer up, inside the verifiers of six production zero-knowledge virtual machines: Jolt, Nexus, Cairo-M, Ceno, Expander, and Binius64 ^[43].

"...public-claim data was not always bound into Fiat-Shamir transcripts before challenge generation ... We are breaking soundness in all six systems." -- OtterSec, "Unfaithful claims: breaking 6 zkVMs," 2026

The public claim the proof was about -- the statement itself -- was not always hashed into the transcript before the challenge was drawn, exactly the ordering invariant the transform depends on. To make the break concrete, the researchers proved mathematically impossible statements -- a counterexample to Fermat's Last Theorem among them -- against reference implementations, noting that in a blockchain context such a forgery "could translate to receiving $1M out of thin air" ^[43]. Every case was responsibly disclosed and fixed between September 2025 and March 2026, in reference and production code, with no realized on-chain theft -- a transcript-layer near-miss, six times over.

Trace the thread and you get four eras of one omission -- Helios in 2012 ^[40], Frozen Heart in 2022 ^[34], Solana in 2025 ^[1], and the zkVMs in 2026 ^[43]. The same missing line of code, re-shipped for fourteen years, each time in a more powerful system than the last.

Three layers, three ways to accept a false proof -- and a pattern nagging underneath all of them. Every break we have seen has the same shape. What is it?

5. One Lens for Every Break#

Line the incidents up -- Zcash, Dark Forest, Aztec, Frozen Heart, Solana, the 2026 zkVMs, and the BNB bridge next door -- and a single sentence explains all of them.

Name the artifact layer -- construction, circuit, verifier, or transcript -- and you have named the break. Across the entire disclosed record, the cryptographic hardness floor never appears. No incident attacked the discrete logarithm, a pairing, or a hash. Every one attacked the human-built layer above them.

That is the whole thesis, stated as a sorting rule. It is falsifiable -- one confirmed break of the discrete-log or pairing assumption in a shipping system would refute it -- and so far nothing in the record refutes it.

You do not have to take the sorting rule on faith. Here is the ledger -- a non-exhaustive but growing record -- laid out so you can audit the claim yourself. Read the "layer" column and the "tag" column together: the clean pure-circuit cases are near-misses, the Groth16 verifier-key drains were exploited and then recovered, and every confirmed theft lives in a verifier, a settlement boundary, or integration code. BNB remains the largest confirmed theft.

The money framing needs the same care. The artifact is what leaked, and where it guarded a rollup, a pool, or a bridge, the leak was measured in funds minted or drained. "The bugs that minted money" is discharged by reading the ledger by category, not by count: the permanent thefts are BNB Token Hub -- still the largest -- and Aztec Connect ^{[29, 30]}; the Veil Cash and FOOMCASH verifier-key drains were exploited-then-recovered, not permanent theft ^{[21, 24, 26]}; and Hinkal is reported, its "proofless deposit" root cause resting on a security firm's reading with a full post-mortem still to follow, its loss put at roughly $800,000 to $830,000, so this article uses about $820,000 ^{[44, 45]}.

Every one reinforces the scoped claim rather than disturbing it: each is a verifier, settlement, trusted-setup, or integration mismatch. What the record still shows no confirmed theft of is the pure case -- an in-circuit under-constraint independent of any settlement, verifier, setup, or integration mismatch. That is not luck to rely on; it is a fact about the record, and the record is still short.

A lens that names every break is worth little if you cannot act on it. So the field built tools -- one for each layer. How well do they work?

6. How the Industry Hunts the Bug Now#

Each defense in use today is a scar -- a direct response to a documented failure. Read them from most sound to most human, and keep one tension in view the whole way down. The tools that can prove a circuit is properly constrained cannot yet run on production-size circuits, and the tools that run on production-size circuits cannot prove anything. No deployed tool is both. Call it the sound-versus-scalable frontier.

Sound uniqueness verification#

The flagship family targets the dominant bug class head-on.

The lineage runs from a first sketch to increasingly capable engines. Ecne was the first widely known open checker that R1CS outputs are uniquely determined by inputs ^{[46, 47]}. Ecne carries a caveat that sharpens what "sound" means: it is a partial prover. A false result "does not mean that the constraints aren't sound, it just means that Ecne is unable to prove" they are ^[46]. Picus, CIVER, and ConsCS go further, returning an actual witness pair.

Picus / QED2 made it quantitative, pairing an SMT solver with uniqueness inference to either prove a signal is determined or return a two-witness exploit; it resolved about 70 percent of a 163-circuit Circom benchmark and found 8 previously unknown vulnerabilities ^{[48, 49, 50]}. CIVER checks uniqueness compositionally, verifying a gadget once and reusing it, from inside the Circom compiler ^[51]. ConsCS is the current accuracy leader on Circom, lifting the solved rate above 80 percent ^[52]. And halo2-analyzer (also called korrekt) carries the whole approach beyond R1CS to Plonkish and Halo2 circuits ^{[53, 54]}.

The governing bound is negative and structural. What these tools actually decide is non-uniqueness: they search for a second, distinct witness that satisfies the same constraints on the same input, and that witness pair is the certificate. Finding one is an NP search, because R1CS satisfiability is itself NP-complete -- so a sound checker cannot also be complete and efficient on every circuit, barring $P = NP$ ^[48].

Deciding uniqueness itself is harder still -- it asks both that a witness exists and that no second one does, which places it above NP, in the class of differences of NP sets; the canonical Unique-SAT problem there is complete under randomized reductions ^{[55, 56, 57]}. Either way the conclusion is the same and unavoidable: every tool in this family is sound but incomplete. It may answer "unknown" or time out. That is not an implementation gap; it is the shape of the problem.

flowchart LR
subgraph SOUND["Sound: a clean result proves absence"]
S1["Ecne, Picus, CIVER, ConsCS, halo2-analyzer -- run on gadgets"]
end
subgraph SCALE["Scalable: runs on hundreds of production circuits"]
S2["ZKAP, Circomspect -- lint, but no proof of absence"]
end
S1 -. "no tool sits in both boxes" .-> S2

Scalable static analysis#

When you cannot prove, you can still scan. ZKAP implements nine detectors over a circuit dependence graph and ran across 258 circuits from popular Circom projects, surfacing previously unknown vulnerabilities ^{[58, 59]}. Trail of Bits' Circomspect is a linter that flags the tell-tale patterns -- a signal assigned with <-- but never constrained with <==, or an output left unconstrained ^[60]. Both scale to hundreds of circuits, and both are unsound: a clean scan means "no known-bad pattern found," not "no bug."

Prevention and the human net#

Two more defenses sit at the ends of the spectrum. At the preventive end, strong-Fiat-Shamir transcript libraries bind the domain separator, the statement, and every public input by construction, removing the avoidable Frozen Heart class before it can be written. The 2026 zkVM breaks named the state-of-practice version precisely: merge the proof and transcript so every value the prover sends is absorbed before any challenge is drawn -- "Halo2 follows this pattern, and Binius is transcript-centric as well," though even transcript-centric Binius still missed binding the statement ^[43].

Alongside it sits a newer, humbler discipline: trusted-setup ceremony hygiene as a shipped step -- confirming the deployed verification key actually finished Phase 2, with $\delta$ independent of $\gamma$, before it holds value. That is prevention by checklist, not a formal tool, but it is exactly the gap Veil Cash and FOOMCASH walked through, and a one-line check would have closed it ^[23].

At the human end sit specialist audits and bug bounties -- the last net, and the one that actually caught the headline cases. The Solana report arrived through disclosure; so did the BNB analysis and the 2026 Groth16 drains ^{[1, 26]}. Firms like Veridise operationalize the sound branch commercially, folding uniqueness checkers into human audits of Circom, Halo2, and other circuits ^[61].

So we have sound tools that do not scale and scalable tools that are not sound. Which philosophy should a team betting real money actually trust?

7. Four Philosophies, No Winner#

This is where the zero-knowledge security community actually argues. Not over which tool is best -- over which kind of tool deserves your trust when funds are on the line. Four camps coexist, and the honest answer is that none of them wins outright.

The first axis is soundness versus scale, which we have already met. Sound formal tools like Picus prove output uniqueness or hand you a two-witness exploit, but only on gadgets; scalable analyzers like Circomspect and ZKAP run across whole projects but can only flag patterns they already know.

The second axis is prevention versus detection: strong-Fiat-Shamir libraries and constraint-safer languages try to make a class of bug unwritable, while linters and verifiers hunt bugs in artifacts that already exist.

The third axis is human versus automated versus economic: an expert audit reasons about intent, a tool reasons about rules, and a bug bounty pays outsiders to find what both missed.

Read the table as a set of holes, not a ranking. The sound tools miss everything past their timeout and every layer that is not the circuit. The linters miss the novel absence they have no rule for. Prevention closes only the class it was designed for. Audits miss what the auditor does not think to check. And a bounty, by definition, reports a bug that already shipped.

The Veil Cash-to-FOOMCASH sequence makes the sharpest case against trusting any single net. The first drain was disclosed with a full technical write-up; six days later the same broken pattern was aimed at a larger target, so a published post-mortem had become an attack -- and rescue -- blueprint inside a week ^{[23, 26]}.

When a bug class's signature is a missing step with a valid-looking default, it is trivially easy to reintroduce and just as easy for a copycat to find once the first case is public. Detection after the fact cannot keep pace with that; only prevention -- a Phase-2 check on every deployed key -- gets ahead of it.

Because the bug is an absence, and absences spread across three layers, no single method can promise to catch them. So the working consensus is not a winner but a discipline: defense-in-depth, one net per bug type. Lint every commit, prove the gadgets, prevent the avoidable class by construction, audit before mainnet, and keep a bounty live after. Each net has holes; the bet is that the holes do not line up.

Defense-in-depth buys coverage, not certainty. Push on why no single tool closes the gap, and you hit something deeper than engineering effort -- a wall.

8. Why You Cannot Test It Away#

Suppose every team ran every tool on this list. The bug class still would not disappear -- and the reasons are theorems, not to-do items.

The first ceiling is the one we met in Section 3, now stated in full generality. A missing constraint is an absence, not a behavior you can enumerate. Testing samples witnesses and checks that valid ones produce valid proofs; but the illegitimate witnesses live in exactly the region the missing equation was supposed to forbid, so no finite suite of positive tests ever reaches them. You cannot sample your way to a constraint that is not there.

The second ceiling is the sound-versus-scalable frontier, and it is structural rather than temporary. Detecting under-constraint means searching for a second, distinct satisfying witness -- an NP-hard search, since R1CS satisfiability is NP-complete -- so a sound checker cannot also run efficiently on every input, and deciding uniqueness outright is harder still ^{[48, 55]}.

Production circuits are enormous; sound tools resolve gadgets and time out on the rest, which is why roughly a third of even a modest 163-circuit benchmark went unresolved ^[48]. Verify gadgets, not whole zkEVMs -- not because the tools are immature, but because the problem is hard in the complexity-theoretic sense.

The third ceiling sits beneath even a perfectly constrained circuit. The Fiat-Shamir transform has no general, unconditional standard-model soundness guarantee for the succinct arguments that SNARKs compress: Goldwasser and Tauman Kalai showed in 2003 that the methodology can be uninstantiable there, with no guarantee that any concrete hash makes it sound ^[62].

The scope of that claim is worth stating exactly, because it is easy to overstate. For a broad class of public-coin interactive proofs -- the trapdoor Sigma-protocols -- Fiat-Shamir is provably sound in the standard model, through correlation-intractable hash families built from the plain Learning-With-Errors assumption ^{[63, 64]}. But those results instantiate a concrete hash inside a common reference string and cover statistically sound proofs; they do not reach the succinct arguments, compiled under the random-oracle heuristic, that shipping SNARKs use -- which sharpens the point rather than softening it.

And the risk is not academic: in 2025, Khovratovich, Rothblum, and Soukhanov exhibited a practical Fiat-Shamir break on a widely studied GKR-based argument, holding "for every choice of FS hash function" ^[65]. Strong Fiat-Shamir removes the avoidable class -- forgetting to hash a public value -- but not the heuristic risk underneath it.

A fourth, quieter limit runs in the same spirit. In the plain model, with no common reference string or random oracle, non-interactive zero-knowledge exists only for languages a verifier could already decide on its own (Goldreich and Oren, 1994), so a hard-language SNARK can relocate its trusted setup but never remove it ^[66]. The 2026 delta == gamma drains are that theorem's practical mirror: a setup cannot be wished away, only executed correctly -- and a skipped Phase-2 step is not an abstraction but a live money bug ^[23].

The ceiling is a set of theorems, not a backlog. You cannot test an absence away, because a test only exercises what is present. No tool is both sound and scalable, because detecting under-constraint inherits NP-hardness. Strong Fiat-Shamir removes the avoidable mistake without removing the heuristic beneath it. And the trusted setup can be moved but not eliminated. Better tools will help. They will not make the bug class vanish.

That last caveat is the article's other standing hedge. "The crypto never broke" is a statement about the record to date, not a permanence guarantee. The floor has held in every disclosed case. It has not been proven unbreakable, and one class of it -- the algebraic, pairing-based SNARKs -- has a known expiry condition if large-scale quantum computing arrives.

If the bug class cannot be eliminated, the work is never "done." It is managed. So where is that management still failing?

9. The Seams Still Open#

The frontier is a list of gaps everyone in the field can name.

The first is scaling sound verification. The unresolved tail of the uniqueness checkers -- the roughly one-third of circuits that time out -- is not random. It is exactly the large, non-linear region where production zkEVMs live ^[48]. Closing that tail would move sound verification from gadgets to the systems that actually hold billions, and no one yet knows how.

The second is portability across representations, and it stopped being hypothetical in 2026. Most sound tooling grew up on Circom and R1CS, but the industry has moved to Plonkish arithmetization, AIR, and full zkVMs. When OtterSec broke six of those zkVMs through unbound Fiat-Shamir transcripts, none of the deployed uniqueness or anti-pattern tools would have caught it: they hunt a missing algebraic constraint over circuit signals, while this was a transcript-ordering defect one layer up, in the verifier's absorb-then-challenge sequence ^[43].

The construction-side answer is emerging -- a 2026 framework shows how to compose a special-sound polynomial protocol with a suitably binding commitment so that applying Fiat-Shamir yields a tightly knowledge-sound SNARK ^[68]. But the detection-side analogue -- a sound automated checker for transcript binding in arbitrary zkVM verifier code, the Picus of the Fiat-Shamir layer -- does not yet exist, and testing cannot stand in for it: honest unit tests run the honest prover, and only manual analysis catches the omission ^[43].

The third is standardizing transcripts and disclosure. The Frozen Heart class exists partly because there was no agreed, hard-to-misuse convention for what a Fiat-Shamir transcript must bind. Strong-FS libraries and transcript-proof fusion help, but a genuinely standard transcript format -- and a shared norm for how ZK bugs are disclosed and dated -- is still forming.

Running parallel to these is a setup-side gap the 2026 drains exposed. Catching a mis-finalized trusted setup -- a verification key whose delta still equals gamma -- is trivial if you know to look, yet there is no standard, enforced pre-deployment gate that a shipped key actually completed its ceremony ^[23]. That is a tooling-and-process gap, not a theoretical one, which is what makes it both fixable and, so far, unfixed.

The fourth is the hardest to see, because it is about the evidence itself.

Measuring true prevalence -- not just disclosed prevalence -- would require watching for bugs that were never reported, which is close to a contradiction. It may be the one open problem here that tooling alone cannot solve.

Underneath all four is a maturity gap. Circuits ship on product timelines; verification tools mature on research timelines. As long as the first clock runs faster than the second -- and it now ships whole zkVMs while the tooling is still learning to read them -- the record will keep adding near-misses, and the industry will keep hoping they stay near-misses.

None of that helps the engineer shipping a circuit this quarter. So here is what you can do today.

10. A Reviewer's Checklist#

Everything above collapses into a handful of questions you can ask of any zero-knowledge system before it holds value. Ask them layer by layer.

Circuit. Is every signal constrained, not merely assigned -- is there any <-- or = without a matching <==? Is there a range or bit-length check on every input that needs one, before any gadget that assumes it? That single question would have caught Dark Forest, whose fix was exactly a pair of Num2Bits checks added ahead of a comparator ^[14]. Is every uniqueness-critical value -- a nullifier above all -- constrained to a fixed length so it cannot take two forms ^[16]?

Verifier. Is the on-chain verifier itself the audited artifact, and is it correct at the edges -- point-at-infinity, zero encodings, on-curve membership? Aztec's circuit was not the problem; its C++ verifier accepting a zero was ^[20].

Trusted setup. If the verifier is a Groth16-style SNARK, did its trusted setup actually finish -- is the verification key's delta independent of gamma, rather than the placeholder generator the two share before Phase 2? A one-line comparison of those two points would have caught Veil Cash and FOOMCASH before either held value ^[23].

Transcript. Does the Fiat-Shamir transcript bind the domain separator, the statement, and every public input, before any challenge is drawn? This is the one-line question behind Frozen Heart, behind Solana's 2025 near-miss, and behind the 2026 zkVM breaks ^{[1, 43]}.

Settlement and integration. Does the on-chain settlement loop cover every public-input slot the circuit committed to, and is a proof actually verified on every path that moves value? Aztec Connect's L1 loop read only the slots up to an attacker-controlled count while the proof committed all 32, and Hinkal was reported to have accepted a deposit with no proof at all ^{[30, 44]}.

// A toy stand-in for a transcript hash: just concatenate the bound parts.
function challenge(parts) {
return parts.join('|');
}

const commitment = 'C';
const statementA = 'honest public statement';
const statementB = 'false statement the prover prefers';

// WEAK Fiat-Shamir: bind only the commitment. The statement is NOT bound.
const weakA = challenge([commitment]);
const weakB = challenge([commitment]);
console.log('weak:   same challenge for two statements? ' + (weakA === weakB));
// true -> the prover can swap the statement without moving the challenge.

// STRONG Fiat-Shamir: bind the statement and every public input too.
const strongA = challenge([commitment, statementA]);
const strongB = challenge([commitment, statementB]);
console.log('strong: same challenge for two statements? ' + (strongA === strongB));
// false -> swapping the statement changes the challenge, blocking the forge.

// A Groth16 key that skipped Phase 2 ships with delta == gamma, both still
// the G2 generator placeholder. Detecting it needs no pairing algebra -- just
// a point-equality check: are the two verification-key points identical?

const G2_GENERATOR = [[10857046, 11559732], [8495653, 4082367]];

// A key that finished Phase 2: delta was randomized, so it differs from gamma.
const goodKey = {
vk_gamma_2: [[10857046, 11559732], [8495653, 4082367]],
vk_delta_2: [[19824234, 55049283], [77712121, 30310670]],
};

// A key that skipped Phase 2: delta is still the generator, equal to gamma.
const brokenKey = {
vk_gamma_2: G2_GENERATOR,
vk_delta_2: G2_GENERATOR,
};

function phase2Skipped(key) {
return JSON.stringify(key.vk_gamma_2) === JSON.stringify(key.vk_delta_2);
}

console.log('good key   -- Phase 2 skipped? ' + phase2Skipped(goodKey));   // false
console.log('broken key -- Phase 2 skipped? ' + phase2Skipped(brokenKey)); // true
console.log('Equal gamma and delta means the verifier accepts forged proofs.');

Then map the tools onto the layers. The point is not to run everything, but to run the right net at the right layer.

One last item belongs on any honest checklist: knowing when zero-knowledge is the wrong tool. A proof system adds a large, subtle artifact -- three layers, each independently fallible -- on top of whatever it protects. If a cheaper mechanism gives the same guarantee, the safest circuit is the one you never had to write.

A checklist is only as good as the misconceptions it clears. Here are the ones this topic breeds.

11. Questions the Record Answers#

The topic breeds a handful of durable misconceptions. Here are the ones worth clearing.

Step back and the ledger reads the same from every angle. In each publicly disclosed failure of a production zero-knowledge system, the cryptographic floor held: no curve solved, no hash reversed, no pairing broken. The human-built artifact above it leaked -- a circuit missing a constraint, a verifier mishandling a zero, a transcript that hashed too little, or integration code that forgot to check the proof at all.

And where that artifact guarded a rollup, a pool, or a bridge, the leak was denominated in money: minted or drained in the near-misses, moved and then returned in the 2026 Groth16 drains, and stolen outright in the confirmed cases, with the largest still in the adjacent BNB Merkle verifier. ※ No confirmed theft in this record is a pure zk-SNARK circuit break: BNB was a Merkle-proof verifier bug; Veil Cash and FOOMCASH were Groth16 verifier-key bugs; Hinkal was reported as a proofless-deposit integration bug; and Aztec Connect paired a circuit-side gap-slot problem with a settlement-layer flaw. That is the distinction this whole article has kept, so that "the bugs that minted money" never quietly becomes "zero-knowledge cryptography was broken."

The crypto held; the code didn't -- in every disclosed case, and so far.

That refrain carries its own hedge. "So far" is doing real work: the record is short, the corpus counts only the bugs that were found, and the floor is unbroken rather than unbreakable -- a STARK's post-quantum security is still a conjecture, and Shor's algorithm remains the one clocked risk ^[67].

The honest claim is not that zero-knowledge cannot break at the math. It is that, to date, it never has -- and every time it broke in real life, the fault was a line of code a human forgot to write. To see why those mechanisms can fail, read the structural sibling, A Valid Proof of a False Thing; to see how the proof systems are built in the first place, read Never Decrypted: Proving You Ran the Computation.