Vitalik Buterin, co-founder of Ethereum, has addressed growing concerns that AI-driven bug hunting could overwhelm developers and create nonstop exploitation opportunities on blockchains.
He argues that, rather than making systems more vulnerable, the short-term application of this technology could actually improve security. In particular, AI-assisted formal verification may become one of the strongest defenses against serious failures in crypto systems and broader internet infrastructure.
AI Could Strengthen Security Instead of Breaking It
Formal verification involves producing mathematical proofs about software behavior that a computer can automatically check, instead of relying solely on human code review. Although the concept has existed for decades, it never became mainstream because manually creating these proofs is time-consuming and tedious for developers.
Buterin says AI changes that balance. Instead of developers writing proofs by hand, they can have AI generate both the code and the accompanying proofs, and then verify that the proven statement matches the intended property. In this workflow, the developer’s role shifts to confirming that the formal specification captures the desired behavior.
He envisions AI models becoming powerful enough to automate bug discovery in existing code. For systems where a single flaw can cost users everything, end-to-end formal verification would mean that an advanced AI looking for vulnerabilities would be analyzing code already proven to meet specific correctness properties.
Buterin highlights Ethereum-related projects already experimenting with this approach. Arklib, for example, aims to produce a fully formally verified STARK implementation. Another project, evm-asm, is developing an EVM implemented in low-level RISC-V assembly and verifying it against a human-readable reference implementation to ensure correctness.
Regarding which AI models are effective for writing proofs, Buterin reports that Claude and Deepseek 4 Pro are sufficient for producing Lean proofs. He also points to Leanstral, a smaller open-weights model fine-tuned specifically for the Lean theorem prover, which can run locally and outperform much larger general-purpose models on formal verification benchmarks.
But There Are Limitations
While optimistic about formal verification, Buterin offers a measured assessment of its real-world limitations and failures. He recounts instances where verified systems still contained vulnerabilities: bugs in verified compilers, libraries where only parts of the code were proven and unproven sections introduced flaws, and specifications that were formally proven but did not actually capture the developer’s true requirements.
His overarching point is that formal verification is not a complete substitute for other security practices. Instead, it is a powerful tool within a broader trend toward reducing the number of bugs per line of code. When applied carefully, it raises the bar for attackers by eliminating entire classes of errors, but it must be combined with proper specifications, auditing, and secure development processes.
The timing of Buterin’s essay is notable. On the same day it appeared, the crypto industry was dealing with a wave of exploits. One attacker drained more than $76 million from the Echo Protocol’s cross-chain bridge. Days earlier, THORChain suffered a breach costing over $10 million. A separate incident targeted the Verus-Ethereum Bridge, where the absence of a validation check allowed a hacker to steal roughly $11.58 million. These are precisely the kinds of localized logic errors that rigorous formal proof and verification efforts aim to prevent.
In summary, Buterin suggests that advancing AI and formal methods together could shift the security landscape in favor of defenders. By automating proof generation and verification, developers may be able to produce software with stronger, machine-checked guarantees—reducing certain categories of vulnerabilities and making it harder for automated attackers to succeed. At the same time, he cautions that formal verification must be applied thoughtfully, with correct specifications and complementary security measures to realize its full potential.