The Orchard Bug and the Unfolding Cybersecurity Reckoning

The flood of AI bug-finds heading for crypto and trad-fi alike — and the well-known math cure we’ve been too lazy to apply

A journalist wrote me earlier today asking for a quick comment on the Zcash situation — by which he meant the Orchard pool bug that just lopped something on the order of forty percent off the price of ZEC over the span of a day or so — and whether other cryptocurrencies are exposed to the same sort of risk.

Indeed, I do suspect what we’re looking at here is a small early tremor of something considerably larger that’s coming for essentially all the software in the world — not just the crypto corner of it, and not even mostly the crypto corner of it, though crypto is one place it happens to be showing up first and most visibly.

The specific bug that bit Zcash is not going to bite anyone else, because it was a specific bug — a subtle under-constrained element buried in the Orchard circuit, down in the elliptic-curve arithmetic, where a constraint that was supposed to enforce a particular check on transaction inputs quietly failed to actually enforce it. The upshot, at least in principle, was that someone could have minted counterfeit ZEC inside the shielded pool without leaving any trace on the transparent ledger — a supply-inflation problem rather than the more familiar double-spend, and a particularly nasty one precisely because Orchard is private by design, which means there is no cryptographic way to go back and prove the thing was never exploited during the years it sat there. Strip away the zero-knowledge exotica and what you have is a plain old logic error: a place where the code did not in fact do the thing its designers were confident it was doing.

One striking thing here is the way this flaw lived undetected for roughly four years — it had been there since Orchard went live back in May of 2022 — and in that time it survived multiple rounds of review by some of the very best zero-knowledge cryptographers on the planet, people who do this for a living and are extremely good at it. And it was finally caught not by yet another careful human audit, but by a security researcher (Taylor Hornby, working under Shielded Labs) pointing a current-generation AI model at the Orchard circuit and, more or less in a single concentrated effort, watching it surface the gap. The model in question, as it happens, was Anthropic’s Opus 4.8. So the AI implications for crypto aren’t some speculative thing I have to gesture at hypothetically — the AI implication is sitting right there in the etiology of this very incident: an AI found, in a matter of days, what four years of world-class human scrutiny did not.

So, to answer the journo’s core question: Are other cryptocurrencies vulnerable to this? To this exact bug, no — it was an implementation error particular to the Zcash codebase. But are other cryptocurrencies, and other smart-contract platforms, and DeFi protocols, and bridges, and wallets, very likely to harbor analogous vulnerabilities of their own — subtle logic gaps that have likewise been sitting quietly through multiple audits? Almost certainly yes: I’d expect a meaningful fraction of them to be found over the coming weeks and months, and I’d expect AI tools to be doing most of the finding. The economics of bug-finding are simply too favorable now. A capability that previously required a scarce, expensive specialist and weeks of attention can increasingly be deployed at scale and at speed, and the same kind of targeted circuit review that turned up the Orchard flaw can be turned, more or less mechanically, on the next protocol, and the one after that.

And this is in no way a crypto-specific problem, even though crypto is one of the places the spotlight is right now. The software infrastructures of banks, payment networks, clearing systems, insurers, exchanges, government agencies — the whole sprawling, decades-deep accretion of centralized financial and institutional code — is every bit as likely to be riddled with serious, long-dormant bugs that the same class of AI tools will start to surface in the near future. If anything the crypto codebases, being newer, smaller, open-source, and written by people who are at least nominally paranoid about exactly this category of failure, are probably in better shape than the average sixty-million-line legacy core-banking system that nobody alive fully understands anymore. The reckoning that’s arriving for crypto is arriving for everyone else too.

The cure for this ailment is well understood, and we mostly haven’t bothered

Here’s the part that I find genuinely heartening, though, and it’s the part that tends to get lost when these stories get told as pure doom. The solution to this whole category of problem is not unknown, not exotic, and not waiting on some future research breakthrough. It is simple and well established and goes by the name of formal verification: you prove, using mathematics, that the software actually does what it was designed to do — not test it, not audit it, not eyeball it very hard, but prove it, with the same kind of deductive certainty you’d want behind a textbook math theorem.

A formally verified implementation of the Orchard circuit would not have shipped with that under-constrained element, because the proof obligation would simply have failed to discharge; the gap would have announced itself at build time rather than four years and several billion dollars of market cap later.

The reason we don’t do this everywhere already is not that we can’t — it’s that it takes extra work. Not at all surprisingly, the software industry, left to its own incentives, has consistently chosen to ship faster rather than ship provably-correct. Rust, which is the language the Zcash circuit code (the halo2 gadgets crate, as it happens) was written in, is perfectly amenable to formal verification — there’s a whole healthy ecosystem of tooling for exactly this — but it’s simply not commonly used, because verifying carries a real cost in effort and time that, until very recently, was hard to justify against the next deadline. What needs to happen — and what I think is going to be forced to happen, partly by exactly the sort of incident we just watched — is a broad shift in the norms of software practice, toward a world in which formal verification is the default expectation rather than a luxury reserved for avionics, nuclear control systems and academic researchers.

When Cardano formally verified its Ourobors consensus mechanisms years ago, it was a big deal to have such an academic technique used in the actual commercial blockchain world. This sort of practice and more now needs to become the norm.

Some languages make this harder than others. Solidity, the workhorse language for an enormous share of the world’s smart contracts, presents real challenges for tractable formal verification — enough so that a number of blockchain networks would need a moderate amount of re-implementation before they could be verified in any practical way. That’s not a counsel of despair, it’s just a cost that has to be reckoned with honestly: some of the existing crypto stack can be hardened more or less in place, and some of it is going to have to be partly rebuilt on foundations that are friendlier to proof.

What we’re doing with ASI:chain — and why “correct by construction” beats “verified after the fact”

All is very much on my mind beyond the latest news headlines, because it’s precisely the discipline we’re building into the ASI:chain layer-1 work my team is now doing at SingularityNET, in collaboration with Greg Meredith’s team at F1R3FLY.io. We’re using formalization-friendly methods throughout — but we’re also going a step further than the usual write-it-then-verify-it loop, which is itself a meaningful improvement over the prevailing write-it-then-hope approach. For key parts of the system, rather than programming the software in the conventional sense and then attempting to prove the resulting artifact correct, we’re deriving the software directly from its mathematical specification, so that it comes out correct by construction — the implementation and its proof of correctness are, in effect, two views of the same underlying mathematical object, and there’s no gap between “what we meant” and “what we built” for a bug like the Orchard one to hide in.

To make this concrete: I spent a fair chunk of last month working out a way to derive consensus mechanisms for ASI:chain in exactly this correct-by-construction fashion — in particular a variant of the Cordial Miners protocol that is reputation-based, centralized/replicated-ledger-free, and suited to deployment on mesh networks and on weak, heterogeneous processing infrastructure rather than assuming a fleet of beefy, homogeneous, always-on validators. Getting the consensus layer itself out of a mathematical spec, rather than hand-coding it and praying, is the sort of thing that sounded like over-engineering or academic self-indulgence right up until Anthropic started making noise about Mythos.

Of course, none of this is free, it’s all hard but very interesting work – and the hard work needed won’t be confined to fancy financial cryptography. Look at the Rust language itself: a great many of its core libraries are written using “unsafe” constructs, the very escape hatches that step outside the guarantees the language is otherwise so proud of, and those constructs are exactly the parts that are hardest to formally verify. They can, of course, be rewritten in safe, verifiable form — but doing so naively tends to make them slower, which is precisely why nobody’s rushed to do it. The interesting wrinkle is that this apparent tradeoff isn’t actually fundamental: with sufficiently advanced techniques — supercompilation being the oneof my old favorites. Using a Rust supercompiler, you could take the safe, verifiable rewrite and aggressively transform it into something that ends up faster than the original unsafe version, not slower. This way you could have the proof and the performance both. It just takes work, and the right tools, and someone willing to put in the effort.

Problem = Solution

TL;DR – yes, this kind of problem that just hit Zcash is likely to be pervasive — not just across cryptocurrencies but across the centralized institutions that are forever lecturing crypto about its riskiness, and across the unglamorous infrastructure underneath all of it. We are about to find out, in fairly short order and at least partly the hard way, just how much latent fragility has been quietly accumulating in the world’s software all these years. But — and this is the part I keep wanting to emphasize — we already know how to fix it. The mathematical methods are reasonably mature, the tooling exists, the theory is settled; this is advanced engineering and deployment, not blue-sky research. The whole of the challenge lies in actually applying these methods, rapidly and at enormous scale, across the staggering quantity of software that runs the world.

The lovely symmetry of the moment we’re in is that: The same AI capabilities that are about to expose all of these long-buried vulnerabilities — the very tools that found the Orchard bug — are also exactly the tools that can help us do the verification and the correct-by-construction derivation and the safe-and-supercompiled rewriting at a pace and scale that would have been simply unthinkable for human engineers working alone in the pre-coding-agents era. The threat and the remedy are, to a remarkable degree, the same technology pointed in two different directions. Which one wins out is going to depend on how quickly and how seriously we choose to take the current cybersecurity situation

Such interesting times… and bound to get more and more so… at an exponential pace!