Buterin: AI-assisted proofs could harden Ethereum

Ethereum co-founder Vitalik Buterin wrote in a blog post Monday that combining formal verification — mathematical proofs that code matches a specification — with recent advances in artificial intelligence can make blockchain software more efficient and more secure.

Formal verification checks whether code implements a formal specification, reducing reliance on manual code review. Buterin wrote that end-to-end proofs show the specific code users run matches the protocol’s security properties.

His post appears amid warnings from researchers and some governments that large AI models are improving at finding and exploiting software flaws. Developers restricted access to a cybersecurity-focused model after internal tests reportedly found hundreds of vulnerabilities in a web browser. Researchers also reported that a preview model helped develop an exploit targeting protections in Apple’s M5 chip, and a U.K. AI security institute flagged offensive cyber capabilities in a newer model.

Software flaws have produced large, irreversible losses in crypto. In April, attackers linked to the North Korea-backed Lazarus Group drained about $292 million in tokens from Kelp DAO after compromising internal RPCs used by LayerZero Labs. Security firms estimate North Korean state-backed actors have taken more than $6 billion in cryptocurrency to date.

Buterin argued formal proofs can increase trust in AI-generated code by showing that optimized, low-level implementations correspond to readable reference implementations and by finding interaction bugs at the edges of subsystems. “If you formally verify end-to-end, then you are proving not just that some description of the protocol is secure in theory, but that the specific piece of code that the user runs is secure in practice,” he wrote.

He added that verification fits cases where the goal is simpler than the implementation, citing quantum-resistant signatures, STARKs, consensus algorithms and ZK-EVMs. “Formal verification is not a panacea,” he warned.

Buterin rejected the idea that advanced cyberattacks will make open-source software or decentralized systems impossible to secure, calling such an outcome bleak for internet decentralization and freedom. He said defenders can preserve an advantage by keeping a small, rigorously verified core of infrastructure and by restricting run-time environments where needed.

The blog post presents AI-assisted formal verification as a defensive approach to reducing software bugs and preserving trust in decentralized systems.