Share
Ethereum co-founder Vitalik Buterin published a deep dive into formal verification on May 18, describing a programming paradigm he says has been gaining traction rapidly across Ethereum’s frontier research and development circles: writing code directly in very low-level languages or in the Lean theorem prover, then verifying correctness with machine-checkable mathematical proofs.
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
The timing is not incidental. April 2026 closed as the most hack-heavy month in crypto history by incident count, with $606 million drained across 29 separate exploits. Buterin’s answer to that record is not better audits — it is proofs.
“If done right, this has potential to both output extremely efficient code, and be far more secure than the way programming has been done before,” he wrote. Yoichi Hirai, a formal verification researcher cited in the post, calls the approach “the final form of software development.”
The core distinction Buterin draws is between testing and proof. Testing checks that the code behaves correctly on a finite set of inputs. Formal verification proves, mathematically, that code satisfies a specification for all possible inputs. A smart contract that has been formally verified cannot contain the category of bug that testing might miss because the test suite did not cover a specific edge case. The proof covers every case by construction.
The practical tool Buterin describes is Lean, a programming language for writing and verifying mathematical proofs automatically. A developer writes a Lean specification describing what the code should do and writes a proof that the implementation satisfies that specification, and Lean’s kernel mechanically checks the proof. If the proof passes, the code is correct with respect to the specification. The only remaining failure mode is a wrong specification.
That failure mode matters. Buterin spends significant space in the post distinguishing what formal verification can and cannot guarantee. It proves that the code matches its spec. If the spec itself is wrong, or if the code interacts with components outside the verified model, the guarantee does not hold. This is not a weakness unique to formal verification. It is the honest statement of what mathematical proof can deliver.
Buterin flagged AI-assisted formal verification separately in an earlier post: “One application of AI that I am excited about is AI-assisted formal verification of code and bug finding. Right now, ethereum’s biggest technical risk probably is bugs in code, and anything that could significantly change the game on that would be amazing.”
One application of AI that I am excited about is AI-assisted formal verification of code and bug finding.
Right now ethereum's biggest technical risk probably is bugs in code, and anything that could significantly change the game on that would be amazing.
— vitalik.eth (@VitalikButerin) February 19, 2024
The blog post deepens that framing by walking through concrete examples of Lean proofs, explaining how AI tools assist in proof construction, and describing why the combination of AI speed and formal verification correctness is qualitatively different from either alone.
The formal verification post connects directly to the Lean Ethereum project, which Buterin described as “delivering on all fronts to ensure Ethereum’s long-term scaling, decentralization and resilience.”
The lean Ethereum team has been doing a truly amazing job kicking into gear this year, and delivering on all fronts to ensure Ethereum's long-term scaling, decentralization and resilience.
I expect all of these ideas will be ready to kick into gear at roughly the same time as… https://t.co/4uimhAZI5N
— vitalik.eth (@VitalikButerin) September 6, 2025
Lean Ethereum applies formal verification to the core protocol specifications across the consensus and execution layers — and eventually to the Ethereum Virtual Machine (EVM).
Buterin’s January 2026 roadmap includes zkEVM-based block validation, a leaner consensus layer, a state tree overhaul, and a potential RISC-V execution layer, each involving code where a single implementation error carries network-wide consequences.
Formal verification is particularly relevant to post-quantum cryptography, a point Buterin does not address directly in the post but that follows from its framework. Anza and Firedancer independently converged on the Falcon signature scheme as Solana’s quantum-resistant candidate, documented on GitHub. The Coinbase Advisory Board paper from April 21 estimated that 6.9 million Bitcoin (BTC) are held in wallets with exposed keys, and Project Eleven’s Q-Day Prize was awarded for breaking a 15-bit ECC key on cloud hardware in April.
Switching to a quantum-resistant signature scheme addresses the cryptographic layer. It does not guarantee that the implementation of that scheme is free of bugs. A formally verified Falcon implementation, where the proof checks that every execution path of the code matches the Falcon specification, provides the second layer of security.
The cryptographic primitive resists quantum attacks; the verified implementation eliminates the possibility that an adversary exploits an implementation flaw rather than the algorithm itself.
Circle Agent Stack and MoonAgents Card landed this month, joining Coinbase x402, which already processes $1.6 million monthly, as the infrastructure for AI agents transacting autonomously onchain.
Each deployment involves smart contracts and payment rails that agents interact with at execution time without human review. Formally verified contract code is qualitatively better suited to autonomous agent interaction than audited code: The guarantee is mathematical rather than dependent on the quality and scope of a human review.
A16z’s Fund 5 thesis, published May 5, named AI agents transacting autonomously onchain as one of its three forward investment theses. The trust model that makes autonomous-agent transactions acceptable at an institutional scale is not an audit report. Buterin’s post is the technical roadmap for what that trust model looks like in practice: code whose correctness is a theorem, not an opinion.
Lean Ethereum is targeting deployment alongside Glamsterdam, for which developers locked in the 200-million gas limit at the Soldøgn interoperability event, with no mainnet activation date confirmed as of May 19, 2026.
Share
preferred on
