Zcash Orchard Bug and Formal Verification

On May 29, 2026, a security researcher running an AI-assisted audit framework pointed a next-generation model at Zcash's Halo2 implementation. Six hours later, they had a working proof of concept demonstrating that the same Orchard note could be spent multiple times, each producing a unique, valid-looking nullifier the protocol accepted.

The bug had been live since May 31, 2022, the day the NU5 upgrade activated Orchard. Four years, one day, ten hours of exposure. The fix was two lines of code.

This is not a story about negligence. Zcash is among the most carefully designed codebases in the industry. A story about the structural limits of the tools we use to secure ZK systems.

Understanding Zcash's Orchard Pool

Zcash operates with two address types: transparent addresses with fully public transactions, and shielded addresses that use zero-knowledge proofs to hide the sender, receiver, and amount. Orchard is the newest shielded pool, using the Halo2 proving system with no trusted setup required.

When you spend a shielded note, you do not reveal which note you are spending. You generate a zero-knowledge proof that you know the spending key for some valid note, and you publish a nullifier: a unique value derived from that note. Once a nullifier appears on-chain, the note cannot be spent again because any reuse produces a duplicate nullifier the network rejects.

The privacy guarantee and double-spend protection are both enforced entirely inside the ZK circuit. Nothing is visible externally. The circuit is the security boundary.

The Orchard Action Statement

Every Zcash shielded transaction executes what is called an Orchard Action. Among the properties an Action must prove is what is called the diversified address integrity condition:

1pk_d^old = [ivk] * g_d^old
2

In plain language: the internal viewing key (ivk) you are using must be the correct one for the address you claim to be spending from. Specifically, if you multiply the base point of the address (g_d) by ivk, you must get the public key (pk_d) of that address.

This constraint is load-bearing. It is what forces the prover to use the real ivk for the note being spent. And ivk feeds directly into the nullifier computation: nf = PRF(ivk, note_commitment). If you can supply a fabricated ivk and pass the address integrity check, you can derive a completely different nullifier for the same note, making the network believe it has never been spent before.

The double-spend attack lives entirely inside this chain.

Where the Bug Lived

The computation [ivk] * g_d is an elliptic curve scalar multiplication: multiply a curve point by a scalar. In Halo2, this is implemented using a double-and-add algorithm in the ecc::chip::mul gadget inside halo2_gadgets.

The algorithm has three stages for performance reasons:

Stage 1 (complete addition): Handles the first few bits with an addition formula that correctly handles all degenerate cases, including adding a point to itself or to the identity.

Stage 2 (incomplete addition): Handles the bulk of the computation using a faster but incomplete addition formula. Incomplete addition is valid here because an honest prover would never hit the degenerate cases in this middle stage.

Stage 3 (complete addition): Handles the final bits and cleanup, again with complete addition.

The base point g_d needs to flow through all three stages. Stage 1 and Stage 3 handle it correctly. Stage 2 is where the bug lived.

In Stage 2, the base point (x_p, y_p) was assigned to the circuit using these two lines:

1region.assign_advice(|| "x_p", self.double_and_add.x_p, row + offset, || x_p)?;
2region.assign_advice(|| "y_p", self.y_p, row + offset, || y_p)?;
3

assign_advice() is a function that writes a value into a circuit cell as a private witness. The critical word is "private witness." It tells the circuit: here is a value the prover is supplying. It does not create any constraint requiring that value to equal anything else in the circuit.

There was a separate constraint, q_mul_2, that enforced consistency of the base across all rows of the Stage 2 loop: the base stayed the same from row to row. But that chain of consistency was never anchored to the actual input base point g_d. It was a chain floating in the air.

A malicious prover could set x_p and y_p to any curve point B' they chose. q_mul_2 would then consistently enforce that B' stayed constant across the loop, satisfying all existing constraints while computing [ivk] * B' rather than [ivk] * g_d.

By choosing B' correctly, the attacker could make the circuit output any value they wanted, including exactly pk_d. The address integrity check would pass. The fabricated ivk would be accepted. A different nullifier for the same note would be published. The note had been double-spent.

The Full Attack Chain

To make this concrete, here is how an attacker executes the exploit.

They generate a fresh random nullifier key nk_fake, producing ivk_fake = Commit(ak, nk_fake). They then compute a fabricated base point B' = [ivk_fake_inverse] * pk_d, chosen specifically so that [ivk_fake] * B' = pk_d. They construct the Orchard Action proof with ivk_fake and B' as private witnesses. The circuit computes [ivk_fake] * B', outputs pk_d, and the address integrity check passes.

The resulting nullifier nf = PRF(nk_fake, note_commitment) is entirely different from the real one. The network has never seen it. It accepts the spend. Repeat with a new nk_fake each time, producing a fresh nullifier each time. The same note can be spent indefinitely.

Because all transaction data is hidden inside the proof, every fraudulent nullifier is mathematically indistinguishable from a legitimate one. There is no forensic method to detect the attack after the fact.

Why Expert Audits Missed It

The reason is structural, not a failure of attention. When a human auditor reads the mul gadget, they check the logical correctness of the algorithm. The double-and-add structure is sound. Complete addition handles the edge cases. The q_mul_2 constraint correctly ensures the base point stays stable across loop iterations. Each component checks out.

What is invisible to sequential code review is the global constraint graph. Verifying that a specific value is properly anchored requires tracing every copy relationship through the entire circuit's constraint topology simultaneously. For a gadget with hundreds of rows and multiple constraint types, this exceeds reliable human recall.

More than 80% of findings in published ZK circuit audit reports trace to this circuit layer: under-constrained witnesses and missing copy constraints. It is the most common class of ZK vulnerability and the one human review is least equipped to catch.

Fuzzing provides no help either. A ZK soundness bug only manifests when a specifically crafted malicious witness is supplied. An honest prover never triggers it. A fuzzer generating random valid transactions would run indefinitely without finding the issue.

An AI model running a targeted audit eventually found it, but only when directed specifically at the scalar multiplication gadget. In broader runs, the same model missed the bug three out of four times.

What Formal Verification Actually Does

Formal verification is the practice of mathematically proving that code satisfies a specification, not sampling it, not testing edge cases, proving it for all possible inputs.

Applied to the Orchard mul gadget, the process works as follows.

You write a formal specification: for all valid inputs (scalar, base), the output must equal the scalar multiple of the base over the Pallas elliptic curve. Tools built for Halo2 extract the actual constraint system from the circuit generation code into a proof assistant like Lean 4, converting constraint logic into formal propositions.

The theorem prover then attempts to prove the specification. To close the proof that output = [scalar] * base, it needs to trace a chain of equalities from the input base point through every constraint in the circuit to the output value. When it reaches the assign_advice() calls in the Stage 2 loop, it finds unconstrained cells. There is no equality in the constraint system linking these cells to the input base. The chain is broken. The proof cannot close.

This is not a false positive. The failure to close the proof is the exact mechanical signature of the missing constraint. The tool does not "think the code looks suspicious." It attempted to derive a theorem and could not, because the theorem is false. The system is unsound.

The fix becomes obvious from the failure mode: the assign_advice() calls need to become copy_advice() calls, which generate explicit equality constraints requiring the assigned value to equal a specific other cell in the circuit, in this case the actual input base point. With those constraints in place, the proof closes, because now there is a complete chain of equalities from the input to every use of the base throughout the computation.

The Limit Formal Verification Cannot Cross

There is an important caveat that the post-Zcash conversation often glosses over.

Formal verification proves that code matches a specification. It does not prove that the specification is correct.

If you write a specification that does not include the requirement that the base point must equal the circuit input, a formal verifier will happily certify your broken circuit as correctly implementing your incomplete spec. The proof closes, and the bug ships.

This is not a theoretical concern. Writing complete, correct specifications for cryptographic protocols is itself a hard problem requiring deep domain expertise. The specification for the Orchard Action statement involves properties spread across the circuit, the protocol description, and the underlying cryptographic assumptions. Capturing all of them correctly in machine-checkable form requires the same quality of expert attention that circuit design requires.

Formal verification raises the security floor dramatically. It eliminates entire classes of implementation bugs. But it shifts the burden of correctness from the implementation to the specification, and the specification is not free.

The path forward is both: invest in formal verification tooling and spec writing expertise together. Zcash's commitment to formal verification in the NU6.2 upgrade is the right decision precisely because their team has the cryptographic depth to write the specs correctly.

The Broader Signal for ZK Infrastructure

ZK circuits are unlike conventional software in one critical way: bugs in the constraint system produce no visible failures under normal operation. A missing constraint is invisible until an adversarial prover exploits it. For privacy protocols, exploitation is also invisible after the fact. Invisible during development, invisible during exploitation: this combination makes ZK circuit bugs uniquely dangerous.

Manual audits catch logic errors in conventional code well. They are structurally insufficient for constraint completeness in ZK circuits. Fuzzing finds runtime failures; ZK soundness bugs have no runtime signature. AI-assisted auditing is improving but remains probabilistic.

Formal verification is the only technique that addresses the structural problem directly. It requires you to prove, not assume, that every constraint is correctly anchored. As ZK protocols move from research into financial infrastructure, the security standard needs to match. An audit is necessary. A proof is necessary too.

Conclusion

A two-line change separated a four-year inflation vulnerability from a sound circuit. assign_advice() to copy_advice(). One adds a value. The other adds a value and a proof that the value is correct. That distinction is the entire story. It is obvious in hindsight, invisible on first read, and exactly what formal verification was built to catch. The Zcash team responded fast, deployed a soft fork within 48 hours of acknowledgment, and has committed to making this class of bug structurally impossible in the next upgrade. The lesson for everyone else building on ZK is simple: do not wait for your own four-year window.