Last month, Shielded Labs security researcher Taylor Hornby discovered a counterfeiting vulnerability in our flagship shielded pool, Orchard. The flaw was patched in a network upgrade, and it is believed that no exploitation occurred.1
However, because exploitation of the vulnerability is undetectable, our community announced plans to launch a new shielded pool called Ironwood. This pool is based on Orchard, but starts fresh with the vulnerability patched. Thanks to a turnstile mechanism in the protocol, wallets can help demonstrate that counterfeiting never occurred by migrating funds from Orchard to Ironwood, protecting their users in the process. At the same time, payments within the old Orchard pool will be disabled to provide an upper bound on the supply of circulating ZEC.
We cannot afford to ship a major bug in Zcash again, since we may not be fortunate enough to discover the next one ourselves. Merely patching the recently discovered bug is insufficient, and so our community engaged in a multi-pronged effort to obtain assurance of the correctness of the upcoming Ironwood pool. This includes extensive auditing and analysis using frontier AI tools.
Our team, for its part, has primarily undertaken a comprehensive effort to formally verify Ironwood, ruling out undetectable counterfeiting bugs. In this post, we want to describe that effort and the strong guarantees that it will establish regarding the safety of Ironwood.
Counterfeiting Vulnerabilities
Counterfeiting bugs are not unique to private cryptocurrencies like Zcash. Any transparent ledger is capable of hosting these vulnerabilities as well, including Bitcoin, which had a counterfeiting incident early in its history.
Transaction values are public in Bitcoin by construction. This means it is far more likely that an exploit of an obscure bug will be noticed shortly afterward, which is why Bitcoin's bug was quickly patched.2 The blast radius can sometimes be smaller as well, since the lack of privacy means counterfeit funds can be identified during remediation.3
More importantly, exploitation of counterfeiting bugs in public ledgers is detectable in the first place, meaning that we can examine the ledger's history to see if those flaws have been previously exploited. The famous counterfeiting vulnerabilities in Zcash's past lacked this property, which is especially irritating: we seemingly found them all before they were ever exploited, yet we cannot definitively claim this until evidence is gathered through the turnstile.
Undetectable Counterfeiting
Undetectable counterfeiting vulnerabilities are only possible in Zcash because of its strong privacy: users keep their transaction information to themselves, and in exchange, the protocol uses cryptography to check that nobody is breaking the rules. This means that the soundness of the monetary supply within a shielded pool rests on cryptographic assumptions.
Every conceivable counterfeiting vulnerability stems from a mistake in the protocol's specification, a mistake in the software that implements it, or a broken cryptographic assumption beneath both.
Broken assumptions can introduce undetectable counterfeiting vulnerabilities, but they aren't bugs, and no counterfeiting vulnerability in Zcash's history has been caused by one. Over time we have reduced our reliance on risky assumptions: our newer shielded pools avoid trusted setups and pairing-based cryptography entirely, and rely on the same kind of discrete-logarithm (DLOG) assumptions that most other cryptocurrencies do.4
Specification and Implementation Bugs
Once we take cryptographic assumptions for granted, counterfeiting vulnerabilities come in two flavors: bugs in our specification and bugs in our implementation. The specification is the formal description of our cryptographic protocol, which we can reason about mathematically. It describes the protocol's algorithms and states the security properties they are meant to provide. The implementation is supposed to carry out those algorithms.
Our formal verification effort is based around a single observation: undetectable counterfeiting bugs can only exist in the specification.
Implementation bugs, whatever other damage they may cause, can only produce detectable counterfeiting. Blocks commit to the full contents of every transaction, including its proofs, so replaying history through corrected software is a deterministic computation anyone can perform. Any transaction that buggy software wrongly accepted becomes permanent public evidence.
Zcash's history illustrates both flavors.
Zerocash InternalH Collision Bug (2016)
Zcash's shielded protocols center around two cryptographic objects: a note, which encapsulates some monetary value and a key authorized to spend it, and a nullifier, which acts as a kind of revocation token to prevent double-spending. Notes are functionally similar to Bitcoin transaction outputs, which users spend by explicitly identifying them so that the network can mark them consumed.
In order to protect user privacy, every user on the Zcash network instead reveals a nullifier for every note they spend. These are all added to a list, and their reuse is prohibited so that the nullifier acts as a public tombstone for the note. To prevent counterfeiting, the nullifier must be cryptographically bound to the note being spent, so that a given note can only ever produce a single nullifier.
Notes in Zcash are revealed in the form of cryptographic commitments. These commitments should be hiding, meaning that discovering their contents is difficult, and binding, so that opening commitments to multiple interpretations of their contents is also difficult.
The original Zerocash paper (upon which Zcash was built) contained a flaw in this binding property, namely that the commitment was not bound to the full note 
. Because the value 
used for the computation of the nullifier 
was only bound to 
via a truncated hash, an attacker could find a hash collision5 and substitute a second value to spend the same note twice.
This flaw was noticed by Taylor Hornby and fixed before Zcash ever launched. It was a mistake in the protocol's specification, and its exploitation would have been undetectable.
Circuit Bugs
Spending notes without revealing them requires proof that the rules were followed. Every shielded transaction carries a zk-SNARK, a kind of zero-knowledge proof, showing that the spent notes exist within the pool and that their nullifiers were derived correctly, among other requirements. The statement being proven is expressed as a circuit, which describes the computation in the form of mathematical equations, and the network's verifier checks each transaction's proof against those equations.
The recent Orchard vulnerability was caused by a "soundness" bug in the zk-SNARK circuit, a flaw that lets a dishonest prover convince a verifier of a false statement.
Morally speaking, this is not a bug in the implementation. A zk-SNARK circuit models a real computation, and so its specification is complicated enough that in practice we use code to represent and describe it. Full nodes never run the code you see above against a transaction. Rather, it induces the mathematical formulas that the verifier relies on.
We have caught other bugs in Zcash's zk-SNARK circuits as well, though before they ever shipped in production. Prior to the initial launch of Sprout—Zcash's original shielded pool—we found a missing boolean constraint during a reimplementation of the Zerocash protocol. Mistakes like these are always bugs in the specification, since reasoning about the SNARK (and its circuit) is necessary to establish any useful claims about the protocol's security guarantees.
When we formally verify our zk-SNARKs to rule out bugs, we do not actually study the circuit code. Instead, we represent the specified behavior of the verifier algebraically and directly prove the correctness properties we need. This captures both circuit bugs and bugs in the SNARK itself.
[BCTV14] Soundness Flaw (2018)
The original Sprout protocol also had an undetectable counterfeiting bug (discovered by Ariel Gabizon), owing to a mistake in the [BCTV14] paper describing the Pinocchio-style zk-SNARK that Sprout deployed. Early zk-SNARKs like this one required a trusted setup: a ceremony that samples secret randomness and encodes it into the public parameters used to create and check proofs. The ceremony is trusted to destroy the randomness afterward.
In this case, too, the flaw was in the specification of the zk-SNARK verifier rather than in the code. The paper took for granted that soundness survived the inclusion of certain polynomial encodings in the trusted setup parameters, but this was never rigorously proven, and turned out to be false.6 Indeed, a formal analysis of the specified verifier would have revealed the problem: with these values in view, a verifier-accepted proof no longer guarantees that the prover knows a valid witness.7
Query Collision Bug (2025)
Specification bugs can produce detectable counterfeiting bugs, too. Last year, zkSecurity identified a soundness bug in halo2_proofs, the proving system used by Orchard. Certain contrived circuits would cause the verifier to consume a redundant polynomial evaluation from the proof string without ever checking its correctness, allowing a malicious prover to lie about it and break soundness.
This is a bug in the specification, not the implementation: for an affected circuit, the redundant evaluation and the missing check both appear in the algebraic description of the verifier that the circuit induces. Formal analysis catches all bugs of this form, because an attempt to prove knowledge soundness of that verifier would fail.
Interestingly, exploitation would have been detectable, though zkSecurity's report doesn't explore this. Neither Orchard nor any other known production deployment was actually affected, but if one had been, every accepted proof would permanently record both the redundant evaluation and the value it should have agreed with. Honest provers always make the two agree, so any accepted proof where they differ is evidence of an exploitation attempt.
Validation Bug (2016)
Zcash has had bugs in the implementation as well.
The zero-knowledge proofs originally used in Zcash were based on pairing-friendly elliptic curves. These constructions center around two elliptic curve groups named 
and . In the original Sprout protocol, the elliptic curve used (BN254) gave us as a prime-order elliptic curve group, but gave as a prime-order subgroup of a different composite-order elliptic curve group.
Unfortunately, a bug in libsnark meant that elements were not checked to exist within the actual prime-order subgroup. Readers might recognize this kind of bug from the famous CryptoNote counterfeiting bug. And just like that bug, because it's in the implementation, it is detectable: any transaction the buggy verifier accepted remains in the chain history forever, where re-running a correct verifier would expose it. The bug was patched in Zcash shortly after launch and, if it was exploitable8, we know it was never exploited.
Similar implementation flaws could exist in our curve and field arithmetic. The specification defines the cryptographic protocol based on the abstract group operations, and so if the real implementation sometimes misbehaves, that deviation will be detectable for the same reason.
Nullifier and Anchor Cache Invalidation
Not every implementation risk is cryptographic. Full nodes are responsible for preventing duplicate nullifiers, and several kinds of mistakes can quietly allow reuse: cache invalidation bugs during chain reorganizations, or edge cases within blocks and transactions. Similar hazards surround the "anchor," a Merkle tree root that each transaction references to show that the notes it spends exist within the pool; an anchor must only be accepted if it was a valid candidate for that pool at a block boundary.
Zcash has never had a bug of this kind. Still, these would be bugs in the implementation, and they would be detectable if exploited.
Formal Verification
Fortunately for us, it is far easier to mathematically exclude the existence of bugs in a cryptographic specification, and therefore all undetectable counterfeiting bugs, than in software, whose correctness rests on slippery claims about the real-world environment our code executes within.9 This is not just a matter of settling for the easier target. Bugs in the software advertise themselves in the chain history, as we've seen, while mistakes in the underlying mathematics are precisely the ones that can hide forever.
We analyze the mathematical structures and behavior of our formalized protocol, reducing its correctness to the security notions and cryptographic assumptions stated in our specification.10 The only remotely shaky claim, then, is that the real software on the Zcash network actually executes the algorithms that we formalized, and any divergence there is an implementation bug that replaying history will expose. Any potential counterfeiting bug is left with nowhere to stand: it is either a flaw in the formalized protocol, which this analysis eliminates, a divergence in the software beyond it, which is always detectable, or a break in the assumptions underneath.
Modern tools such as Lean can automatically check these proofs once written, providing certainty about their mathematical correctness, and LLMs guided by humans can shorten the process of generating these machine-assisted proofs to just weeks, even for complex cryptosystems like ours. We have pivoted our time and resources toward providing this analysis for Ironwood, working with our own Tal Derei, Gregor Mitscha-Baude from zkSecurity (whom we've contracted to assist in this effort), and Daira-Emma Hopwood from the Zcash Open Development Lab. Thanks to our experience designing and formally analyzing Tachyon's upcoming protocol, we've made substantial progress in the last several weeks.
Conclusion
The above is not meant to be an exhaustive list of every kind of counterfeiting bug, or every possible implication of a serious flaw in our protocol. Rather, it shows that formally verifying our specification is enough to rule out all undetectable counterfeiting vulnerabilities that could exist in our protocol and its implementation.
In principle, formal verification can reach much further than this: the implementation itself, and every bug in between, can be subjected to the same mathematical scrutiny, and we intend to pursue that over time. But undetectable counterfeiting is the class of bug where the stakes are highest and where mathematics alone can settle the question, so that is where our effort is aimed first. Most of the analysis rests on a property called knowledge soundness, and its story, along with how the verifier we formalize compares with the software the network actually runs, will be discussed in our next post.
Profit-maximizing attackers who discover a counterfeiting flaw face a race against discovery, patching, competing attackers (especially in our case, where the code is open source), exchange intervention, and ultimate market collapse. Their incentive is to convert as many counterfeit coins as possible into external value before the opportunity disappears, staying below the threshold that would trigger suspicion. And once the flaw becomes known, the same logic becomes a broader race to exit: confidence falls, liquidity deteriorates, exchanges and users react defensively, and the expectation of others selling (including other counterfeiters) is a strong reason to rapidly sell. Nothing of the kind has been observed.
The bug discovered in Bitcoin was patched within hours, followed by a blockchain reorganization spanning dozens of blocks. This remediation deprived honest miners of thousands of freshly mined bitcoins, and erased billions of counterfeit ones from the ledger.
What would have happened if the Bitcoin bug had been discovered months after exploitation? It's possible that the remediation would have looked quite different; a chain reorganization spanning months of history would have been impractical, so the transaction graph descending from the counterfeit funds would likely have been invalidated instead. But if those funds had circulated, the crisis of confidence might have been unbearable.
We have also consolidated assumptions. For example, we rely on the collision-resistance of Pedersen hashes for our Merkle tree based accumulators, which tightly reduces to an existing assumption (DLOG) that we already assume for soundness. Additionally, we will continue to weaken our assumptions to defend against quantum adversaries or add redundancy to the protocol in the future.
The hash output was truncated to 
bits, so a birthday-style attack could find a collision with roughly 
work, within reach of a well-resourced attacker.
The offending encodings appeared in the trusted setup transcript rather than in the proving key, but this was a technicality; an implementation faithful to the paper would have placed them in the proving key itself. Either way, the elements had to exist somewhere (by assumption), and the security claim needed to hold with them in view. It did not.
Knowledge soundness is formalized through an extractor that can recover the prover's witness (the notes, values, and keys underlying a shielded transaction) from any convincing prover; if no valid witness exists, no prover can succeed. Here, the verifier could be convinced even though there was nothing to extract.
We're not aware of a published analysis giving a concrete soundness break for this exact failure mode in this SNARK or any other pairing-based scheme, and finding one may be nontrivial as it would depend on the specific implementation of the pairing as well. If the second input to the pairing is merely a point on the twist curve and not in , it is outside the domain modeled by the proof system; any value returned by the Miller loop/final exponentiation is an implementation artifact rather than the pairing assumed by the protocol. The security argument only treats the pairing as a bilinear map on the prime-order groups, and assuming otherwise is regarded by auditors as a massive soundness risk for any cryptographic scheme.
Formal verification can also be applied more comprehensively to real implementations, but the bridge between a formal model and executable code introduces gaps of its own. In practice we must assume that some translation between the real and the formalized behavior is sound, and that the machine and operating system environment are reliable. The more complicated this translation, the more difficult it is to justify.
The machine checks that the formalized protocol satisfies these security notions exactly as written; whether the notions capture what we actually care about is left to human judgment. A mis-stated definition of balance, for example, could quietly narrow what the proofs establish. Fortunately, such definitions are short, largely standard, and sit in plain view of reviewers.