“We were attacking our own protocol very early on and eagerly with frontier AI models in order to find these really difficult to discover bugs that had eluded auditors and cryptographers and hackers for years. And there turned out to only be one of them, and it was very, very subtle, that only an AI could really find, apparently.”
Bankless · Crypto & Web3 · November 2026
Context
Asked about formal verification and AI threats to cryptography, Bowe describes how an earlier counterfeiting bug in a Zcash shielded pool was found by pointing frontier models at the protocol. The team then formally verified the pool.
Transcript
…people on the other side are just like denying the threat entirely of AI or quantum computers and stuff like that. And they look silly. So I think Justin probably ran into maybe the extent to which he can be a doomer without looking kind of ridiculous. That's just my personal view, personal view.
What about the subject of formal verification just to give Zcash longer term, stronger, harder assurances about the hardness of the whole entire system?
We have been working on, so with Tachyon, we were already writing, doing formal verification of Tachyon because Tachyon's actually kind of, it's using more esoteric cryptography. So like a year ago, we had already set up contracts with these like formal verification people to help us build this stuff and integrate it into our into our cryptography stack. And so we were already kind of ahead of the game on that. Then this orchard counterfeiting bug was discovered earlier this year. And so we needed to basically rule out that it was impossible for any more counterfeiting bugs to exist. And you can do this with formal verification. Like we can mathematically prove that there are no undetectable counterfeiting bugs in the protocol anymore inside of the shielded pool. And so we had this like massive month and a half long or two month long sprint to prove that to formally verify it. And we pulled it off and shipped this upgrade. And I think it's like been hugely inspirational. I've heard from every project in the crypto world has messaged me and said, how are we? Going to do this for our protocol? What'd you guys do?…
What's kind of cool is for verification is like getting more and more capable every month. Like literally today, one of my friends made a post after this whole PHP instant about how do you do formal verification off of the raw assembly to protect like a PHP like thing again, where TLDR, this PHP…
So with all this formal verification stuff, there's just a ton of auditing to do with regards to all the code. Like Dave just talked about all this fuzzing, which is a term I once knew, but not really familiar. Why do we believe in this, in formal verification? What does this really do for Zcash in…
So you can formally verify things. What does it mean to formally verify something? It means that you have some kind of proof that some code or some math is correct according to some property or specification. And that's really vague because the specification can be wrong. Like the property you're…
More from Bankless
