- Vitalik Buterin said AI could help developers mathematically verify software and reduce security risks.
- Ethereum projects are already exploring formally verified cryptography, consensus, and ZK-EVM systems.
- Buterin argued AI-assisted verification may strengthen defenses against advanced automated cyberattacks.
Ethereum co-founder Vitalik Buterin said on May 18 that artificial intelligence could strengthen crypto security through formal verification tools. According to Buterin, AI-assisted proof systems may help developers mathematically verify software behavior instead of depending only on audits and testing. His remarks focused on Ethereum infrastructure, consensus systems, cryptography, and zero-knowledge technology.
Formal Verification Moves Into Focus
According to Buterin, formal verification allows developers to prove code behavior using mathematical methods checked automatically by computers. Instead of relying only on software tests, developers can confirm programs operate correctly under predefined conditions.
However, Buterin noted that writing those proofs manually has historically remained slow and difficult. He added that AI could reduce that burden by generating code, proofs, and additional testing structures simultaneously.
Buterin referenced researcher Yoichi Hirai, who described the approach as the “final form of software development.” He explained that humans would still verify whether the intended specifications remain accurate.
Notably, Buterin pointed to existing Ethereum-related projects already applying these methods. Those include quantum-resistant signatures, STARK proof systems, Byzantine fault-tolerant consensus protocols, and ZK-EVM infrastructure.
In addition, projects such as Arklib are pursuing formally verified STARK implementations. Meanwhile, the evm-asm project is building a mathematically verified Ethereum Virtual Machine using RISC-V assembly.
AI Security Debate Expands Across Crypto
As the discussion widened, Buterin acknowledged formal verification still carries limitations and operational risks. He stated that verified software may still fail if specifications contain mistakes or if vulnerabilities exist outside verified code.
However, he argued that mathematical verification reduces uncertainty between intended software behavior and actual execution. According to Buterin, AI could help developers produce more proofs, tests, and independent implementations faster.
He also described a future structure separating software into secure and insecure layers. Under that approach, smaller secure cores would handle sensitive infrastructure, while lower-risk systems would operate with restricted permissions.
Ethereum Security Efforts Continue
Meanwhile, Buterin connected the discussion directly to Ethereum’s broader infrastructure development. He said critical systems, including consensus mechanisms and cryptographic infrastructure, may require deeper verification as AI-generated software expands.
According to Buterin, defenders may finally gain stronger tools against increasingly advanced AI-assisted attacks. He cited Mozilla’s internal experience hardening systems against automated exploit discovery tools.
The discussion arrives as decentralized finance platforms continue facing exploits tied to smart contract vulnerabilities and infrastructure weaknesses.
