Ethereum’s Vitalik Buterin Explains How AI Could Make Smart Contracts Truly Secure

Ethereum co-founder Vitalik Buterin has published a detailed argument that AI-assisted formal verification could fundamentally change how secure software is built, pushing back against growing pessimism in the cybersecurity community about whether trustless systems can survive increasingly powerful AI-driven attacks.

“Many people have claimed that with AI-assisted bug finding, secure code will be impossible,” Buterin wrote. “I have a much more optimistic take, and AI-assisted formal verification is a major part of the reason why.”

What Formal Verification Actually Is

Formal verification is the practice of writing mathematical proofs about code that can be checked automatically by a computer. Rather than testing software and hoping bugs do not appear, developers write proofs that mathematically guarantee a piece of code behaves exactly as intended under all conditions.

The technology has existed for decades but remained niche because writing these proofs by hand is extremely difficult and time-consuming. Buterin’s argument is that AI changes this equation dramatically. AI can write both the code and the proofs, while humans simply verify that the statements being proved match what they actually want the software to do.

He described this combination as what researcher Yoichi Hirai calls “the final form of software development.”

Why It Matters for Ethereum

Buterin pointed to several areas where formal verification is already being applied within Ethereum’s development ecosystem. These include quantum-resistant signatures, STARK proof systems, consensus algorithms, and ZK-EVMs, all areas where the security properties are simple to define even though the underlying code is extraordinarily complex.

Projects like Arklib are working toward a fully formally verified STARK implementation. The evm-asm project is building an entire EVM written directly in RISC-V assembly, verified mathematically against a human-readable reference implementation. Byzantine fault-tolerant consensus protocols are also being formally specified and verified in Lean.

The main insight is that for these systems the gap between what the code does and what it is supposed to do can be closed with mathematical certainty rather than probabilistic testing.

The Limits He Acknowledges

Buterin was careful not to overstate the case. Formal verification has real failure modes. Proofs can be written about only part of a system while critical bugs hide in unverified sections. Developers can forget to specify properties that matter. The formal specification itself can be wrong. Hardware vulnerabilities like side-channel attacks can bypass even mathematically correct software.

“Provable correctness does not prove that software is correct in the way most human beings understand correctness,” he wrote. What formal verification actually does is allow developers to express their intentions in multiple different redundant ways and automatically check that all those expressions are compatible with each other.

The Broader Vision

Buterin described an optimistic future where software splits into two layers. An insecure edge layer handles lower-stakes functions, runs in sandboxes, and operates with minimal permissions. A secure core handles everything critical, including Ethereum itself, operating system kernels, and sensitive IoT infrastructure.

The secure core is kept deliberately small and subjected to aggressive formal verification. AI brings the computational power to make verification practical at scale. The result is not software with zero bugs but software where the most critical components can be trusted with mathematical confidence rather than hope.

“Defenders finally have a chance to win, decisively,” he concluded, citing Mozilla’s own experience hardening its codebase against AI-assisted attack tools.