- Vitalik Buterin says that formal verification on Ethereum, assisted by AI, would create “extremely efficient code” and be far more secure.
- His proposal comes at a time when Ethereum has lost over $300 million in the first four months to hackers.
Formal verification, enabled by artificial intelligence and written in low-level languages or in Lean, could be the biggest security leap for the crypto industry, Ethereum founder Vitalik Buterin says.
In a blog post on Monday, Vitalik broke down how AI is catalysing a new approach to crypto security. This approach involves writing code in very low-level languages such as EVM bytecode or directly in Lean, a language designed specifically for writing and automatically checking mathematical proofs.
He stated:
“If done right, this has the potential to both output extremely efficient code and be far more secure than the way programming has been done before.”
Vitalik says that crypto faces a bug problem; if an attacker introduces a bug in a smart contract, they can drain millions with no way to recover the funds. For Ethereum, the challenge is bigger due to its use of new zero-knowledge proofs.
The solution lies in formal verification, says Vitalik. This is the practice of writing mathematical proofs about code that a computer can automatically check and verify.
Many people have claimed that with AI-assisted bug finding, secure code (and hence trustless anything) will be impossible.
I have a much more optimistic take, and AI-assisted formal verification is a major part of the reason why:https://t.co/0ceMBZ6uqj
— vitalik.eth (@VitalikButerin) May 18, 2026
Vitalik Targets Ethereum Security Amid $1B Hacks in 2026
Formal verification has existed for over a decade. However, it’s too tedious and technical to use at scale. AI changes this, writing and checking these proofs, says Vitalik.
He stated:
“if we want to have a model of internet security that is not based on everyone trusting a few powerful organizations, we need to be able to instead trust code – including trusting code in the face of powerful AI adversaries. AI-assisted formal verification lets us take large steps in doing just that.”
He notes that Signal, the encrypted messaging app, is already trying this approach. The app is working with a research group to verify its X3DH key exchange protocol in Lean.
Fortifying Ethereum’s security is vital in a year in which hackers have ramped up their attacks on dozens of protocols building on the network. This year, over $1 billion has been stolen in crypto overall, with a sizable chunk of this being in Ethereum. The biggest attack has been on Ethereum-based KelpDAO, where attackers exploited the LayerZero bridge to steal $300 million. As we reported, these attacks have shaken investor confidence in DeFi, with 60% of DeFi platforms recording outflows in the past month, totalling $18 billion.
ETH trades just above $2,100, dipping 10% in the past week, with bullish accumulation from Tom Lee’s Bitmine failing to trigger a comeback.
