Vitalik Buterin says AI-assisted “formal verification” could help secure blockchain networks, smart contracts, and cryptographic systems against software flaws

Ethereum co-founder Vitalik Buterin said that mathematically verified software is becoming essential to protecting Ethereum …

Decrypt 2026-05-19 Jason Nelson

Context & Ripple Effects

Related coverage shows AI reasoning models being treated as increasingly useful for mathematics, while Axiom Math’s funding highlights commercial interest in combining AI with Lean-based code verification. That makes Ethereum a prominent security-critical application for a capability that is moving from research evaluation toward software assurance.

The same coverage also includes mathematicians’ warnings about AI accuracy and reliability. For cryptographic and blockchain uses, that distinction matters: AI may accelerate construction or checking of proofs, but the value of formal verification depends on the rigor of the underlying proof system rather than confidence in model output alone.

First-order effects

Buterin’s endorsement raises the profile of AI-assisted formal verification as a security tool for Ethereum-related smart contracts and cryptographic software, directing attention toward mathematically checked development workflows.
Developers and auditors working on high-value blockchain code face a clearer incentive to use AI for proof assistance and verification tasks, while retaining formal checks as the acceptance criterion.

Second-order effects

Verification-tool providers and AI labs have an incentive to compete on integrations with proof languages and developer workflows, not only on general-purpose code generation.
As stronger verification becomes more practical, projects that can demonstrate rigorous assurance may differentiate themselves from systems relying primarily on conventional audits; audit practices could shift toward reviewing specifications and proof coverage.

Third-order effects

If AI reliably lowers the cost of producing formal proofs, mathematically verifiable software could become a more common baseline for security-critical digital infrastructure, not just blockchain applications.
The limiting issue will remain trust in specifications, proof tooling, and implementation boundaries: broader AI use may increase demand for independent validation and human expertise rather than eliminate it.

The trend: This is part of the shift from AI as a code-generation tool toward AI as an assistant for rigorous, machine-checkable software assurance.

Discussion

@vitalikbuterin @vitalikbuterin on x
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://vitalik.eth.limo/...
@haenko21 @haenko21 on x
the clearest framework I've read on what happens after AI floods the world with sloppy code. vitalik's argument: the only stable architecture is “insecure edges in sandboxes” around a “secure core” that administers everything. if the edge breaks, the core protects you. he names
@vezko_zkp @vezko_zkp on x
normal software is finally running the AI checker vs AI attacker loop. zk circuits have been doing this for years. every proof is formal verification by design. vitalik's optimism here is just rest of software catching up to what crypto already shipped. #zkPass
@wyatt_benno Wyatt Benno on x
Great piece. The thesis is right, formal verification is finally practical thanks to AI! One gap: Lean requires proof experts, relies on interactive proving, and produces non-succinct proofs. SMT-based verification (Dafny, ICME PreFlight, etc) automates the proof step entirely.
@toly @toly on x
Formally verify your code!
@mertunsal2020 Mert Ünsal on x
It would be an interesting world if software becomes so cheap that we rewrite everything in Lean and verify! We are building the models that enable such a future.
@abanand9 @abanand9 on x
At Category Labs, we've been using AI-assisted formal verification to prove correctness of real C++ code in the Monad execution client. In our experience, frontier models often missed bugs in ordinary review, but found them when asked to do Rocq proofs. Blog post coming soon.
@hosseeb Haseeb on x
We're currently in the herd immunity phase of AI-assisted cyber. The wave of hacks and exploits is brutal. But we have to go through it, and it will ultimately make all of our software more robust. In 10 years, we will look at AI-assisted formally verified software the same way […
@sagivmooly Mooly Sagiv on x
This is something the industry hasn't seen yet. Certora is the pioneer in formal verification. FV + AI is our bread and butter and we've got something new coming soon.

Chronicles