Ethereum's co-founder published a long essay on Sunday arguing that machine-checkable mathematical proofs, generated and verified by AI, could become the foundational security layer for blockchains, cryptography and critical internet infrastructure — even as the same AI capabilities accelerate vulnerability discovery on the offence side.
Vitalik Buterin published a long essay on Sunday arguing that AI-assisted formal verification — using machine-checkable mathematical proofs to confirm that software behaves exactly as written — could become the foundational security layer for blockchains, cryptography and critical internet infrastructure once large language models become competent enough to generate both the code and the proofs needed to verify it. The piece is titled "A shallow dive into formal verification" and runs against the prevailing intuition that AI-generated code will mostly make systems easier to attack.
Buterin's argument is structural rather than rhetorical. Formal verification has existed for decades; academic projects like CompCert, seL4 and miTLS have produced verified compilers, kernels and TLS implementations with mathematical guarantees that conventional auditing cannot match. It has remained niche because writing the proofs is brutally laborious. A proof of a moderately complex Ethereum precompile can take a senior engineer months. AI changes the economics. If a model can draft both a candidate implementation and a Lean proof of its correctness in minutes, the constraint that has kept formal verification out of mainstream development collapses.
The applications Buterin identifies are specific. He points to Ethereum's consensus mechanism, zero-knowledge proof systems, post-quantum cryptography, and the EVM itself as candidates for verification. The interesting case among those is post-quantum cryptography, where the new lattice-based and hash-based schemes Ethereum will need by the end of the decade are too young to have the years of cryptanalytic scrutiny that protect existing schemes. A formal proof of correctness — not unhackability, but mathematical equivalence to the algorithm as specified — is the closest substitute available.
He is also explicit about what formal verification cannot do. A proof that one layer of a system is correct says nothing about the layers above or below it. Specifications themselves can be wrong; a perfectly verified implementation of the wrong algorithm is still wrong. Hardware-level attacks — Rowhammer, Spectre, side channels — sit outside almost every formal model in current use. And the proof assistants themselves have small trusted bases that could theoretically contain bugs, though those bases have been re-implemented and cross-checked for decades. None of this is a reason to dismiss the approach. It is a reason to be careful about overclaiming what verified code guarantees.
The timing of the piece is not accidental. The first four months of 2026 produced more than $750 million in DeFi exploits, dominated by infrastructure failures rather than smart-contract bugs in the narrow sense — Kelp DAO's $292 million bridge incident in April, the THORChain Asgard-vault breach last week, the Verus-Ethereum bridge drain three days after that. None of these is a contract that auditors missed. They are validation gaps, key-management failures, and cross-chain economic-binding errors — the kind of defects formal verification, properly applied, is built to catch. Buterin's essay frames AI-assisted verification as the long-run response to exactly that class of attack.
There is a competitive subtext too. Solana, which has had its own security incidents, is moving in the opposite direction on roadmap — faster finality, higher throughput, looser developer constraints. The Alpenglow upgrade, currently in test, targets 150-millisecond block finality and replaces both Proof of History and TowerBFT. Ethereum's response under the upcoming Glamsterdam upgrade is more cautious; the network is targeting a 200-million gas limit floor and is investing heavily in primitives — block-level access lists, proposer-builder separation, native ZK — that lend themselves to formal verification because they are small, well-defined and stable. Buterin's vision of a verified-by-default Ethereum is not in tension with that roadmap. It is the long-term case for it.
The essay is not a roadmap document. It is a research note from one of the few people whose research notes still move the field. The headline question — whether the security advantages of AI-assisted verification outpace the additional attack surface AI-assisted exploitation creates — is unresolved. Buterin's answer is that the defenders will get there first, partly because formal proofs can be checked by anyone in seconds while exploits have to be discovered, weaponised and deployed. That asymmetry is real. Whether it is enough is the question every protocol team currently planning a 2027 launch is going to have to answer.
