Ethereum co-founder Vitalik Buterin said on May 18 that artificial intelligence could improve crypto security by making formal verification more practical for developers. He tied the idea to Ethereum infrastructure, consensus systems, cryptography, and zero-knowledge technology, arguing that AI-assisted proof systems may let teams verify software behavior mathematically instead of leaning only on audits and testing.
Formal verification aims to prove code behavior
Buterin described formal verification as a method that uses mathematical proofs, automatically checked by computers, to confirm that software behaves correctly under predefined conditions. The appeal is clear: rather than treating tests as the main safety check, developers can try to prove what a program will do. That gap between intended behavior and actual execution is where many failures emerge.
He also noted the long-standing obstacle. Writing such proofs by hand has been slow and difficult, which has limited adoption. In his view, AI could reduce that burden by generating code, proofs, and added testing structures at the same time. Researcher Yoichi Hirai, whom Buterin referenced, described this direction as the “final form of software development.” Even so, Buterin said humans would still need to verify that the specifications themselves are correct.
Ethereum-related projects are already applying the approach
Buterin pointed to several Ethereum-linked efforts already using these methods, including quantum-resistant signatures, STARK proof systems, Byzantine fault-tolerant consensus protocols, and ZK-EVM infrastructure. He also named Arklib as a project pursuing formally verified STARK implementations, while evm-asm is building a mathematically verified Ethereum Virtual Machine with RISC-V assembly.
Those examples show that formal verification is not being discussed only at the research level. It is being pushed into live infrastructure work. In systems such as virtual machines, consensus components, and cryptographic modules, a flaw can have consequences well beyond one application.
Verification has limits if the specification is wrong
Buterin did not present formal verification as a complete answer. Verified software can still fail if the specification contains mistakes, or if vulnerabilities exist outside the part of the code that was verified. In other words, proving that code matches a design does not prove that the design itself is sound. That distinction remains important.
Still, he argued that mathematical verification can reduce uncertainty in critical software. As AI-generated software expands, he said, deeper verification may be needed for consensus mechanisms and cryptographic infrastructure. He also outlined a structure in which software is split into secure and insecure layers: a smaller secure core would handle sensitive infrastructure, while lower-risk systems would run with restricted permissions.
AI-assisted attacks are advancing, and defenders need better tools
Buterin connected the issue to the rise of advanced automated cyberattacks. His argument was that defenders may finally gain stronger tools as attackers also adopt AI. He cited Mozilla’s internal experience hardening systems against automated exploit discovery tools as part of that discussion.
The comments come as decentralized finance platforms continue to face exploits linked to smart contract bugs and infrastructure weaknesses. For Ethereum, the question is whether AI can help move formal verification from a difficult specialist method into broader engineering use across critical systems.