AI-powered bug-finding and exploitation challenge is transitional, Ethereum's Buterin says
As more stories of AI-enabled exploits targeting crypto protocols emerge, the co-founder of the Ethereum blockchain, Vitalik Buterin, says he's optimistic that AI can also finally enable the implementation of an old protection method at scale.
This is all related to so-called formal verification. Originally, it refers to writing proofs of mathematical theorems so they can be checked automatically. In a broader sense, it's about verifying that a system behaves the way we want it to. The regular exploitation of code vulnerabilities in crypto and other industries shows that these systems remain vulnerable.
But now, Buterin says that AI can help overcome the difficulties of implementing formal verification.
“The entire reason why formal methods have not taken off is that most people can't wrap their heads around writing the damn things,” Buterin wrote in his latest blog post, adding that now, “you can just let the AI run for hours all on its own” and get your code verified.
According to him, Claude and DeepSeek 4 Pro are already sufficient for writing proofs.
Therefore, Buterin says he’s more optimistic about the future of cybersecurity, and while the recent trend of AI bug-finding and exploitation is a serious challenge, it is a transitional one.
The conversation on this topic is live. Join in the discussion.
“Once the dust settles and we get into the new equilibrium, we will get to something far more defense-favoring than what we had before,” the Ethereum co-founder wrote in a lengthy and technically detailed blog post.
However, he emphasized that formal verification is not bulletproof, as the computer and the human would need to be 100% on the same page about what "provable correctness" and "provable security" mean when it comes to specific code, and this might be difficult.
“It's very easy to forget to prove the claims that are actually important.<..>And it's very easy to decide that only one part of the system really needs to be formally proven, but then still get hit by a critical bug in the other parts (or even hardware),” Buterin explained, suggesting that this problem might be solved only when human brains can be simulated.
According to him, while formal verification won’t solve all code verification problems, it might provide a model of internet security that doesn’t require user trust in a few powerful organizations.
“AI gives you the ability to write large volumes of code at the cost of accuracy, and formal verification gives you back ... accuracy (in fact, even more than you had before),” Buterin concluded.
Unlock more exclusive Cybernews content on YouTube.
