TL;DR:
Vitalik Buterin published an extensive reflection on formal software verification, a discipline that allows for mathematically proving that a program behaves exactly as it was designed.
According to the Ethereum co-founder, this technology —powered by artificial intelligence— could become the definitive answer to one of the most persistent problems in the tech industry: critical bugs in high-security code.
In simple terms, it involves writing mathematical proofs about a program’s behavior, so that a computer can verify them automatically. Rather than trusting that code “looks correct” or that tests cover it sufficiently, formal verification allows one to prove with logical rigor that certain properties always hold. Buterin illustrates the concept with examples in Lean, a programming language specifically oriented toward this type of proof.
Smart contracts are immutable once deployed, and a bug can mean the irreversible loss of funds —even at the hands of actors like North Korea, Buterin notes. Projects such as Arklib, evm-asm and others are already working on formally verified implementations of key Ethereum components: STARKs, the EVM, and Byzantine fault-tolerant consensus algorithms.
As AI expands its role in code generation, having tools to guarantee the highest possible level of security becomes essential.
Buterin draws a parallel: just as ZK-SNARKs restore privacy and scalability to blockchains, formal verification restores precision to AI-generated code. Artificial intelligence can write large volumes of code —even in assembly language for maximum efficiency—, while formal verification ensures that code is correct. The result would be a virtuous cycle: code that is faster, more secure, and auditable by anyone.
The co-founder of Ethereum acknowledges that formal verification is not a magic solution. Bugs can hide in unverified parts, specifications can be poorly framed, and side-channel attacks elude any mathematical model. But he concludes with optimism: in the secure core of critical systems —operating systems, blockchains, hardware—, the old maxim that bugs are inevitable could finally cease to be true.
