Vitalik Buterin said advances in artificial intelligence could reshape how crypto systems are attacked and defended, pushing infrastructure toward mathematically verified software.
Buterin Essay Outlines AI Threat
The Ethereum co-founder argued that increasingly powerful AI models will make it far easier to discover and exploit vulnerabilities in complex software.
Buterin called bugs in crypto infrastructure even more alarming once AI tools begin automating vulnerability discovery, a concern echoed across the security research community.
He singled out Ethereum (ETH) infrastructure, consensus mechanisms and post-quantum cryptography as priority targets for stronger defenses.
Rather than relying on traditional audits, Buterin said developers should adopt formal verification, an approach that mathematically proves code behaves as intended under set conditions.
Also Read: Crypto Funds Bleed $1.07B As Iran Tensions End Six-Week Inflow Run
Formal Verification As Defense
"AI gives you the ability to write large volumes of code at the cost of accuracy, and formal verification gives you back accuracy," Buterin wrote.
He pushed back against researchers who argue AI-generated software has become impossible to fully trust, presenting instead a more optimistic case.
Buterin believes AI-assisted coding paired with verification tools could eventually produce software stronger than what humans build alone.
He also flagged active projects such as Arklib and evm-asm, which focus on securing cryptographic infrastructure and Ethereum Virtual Machine software.
The essay warned, however, that formal verification is not a cure-all. Even mathematically proven systems can fail when developers verify the wrong assumptions or when exploits sit outside the verified code path.
Buterin Security Track Record
Buterin sketched a future in which sensitive digital infrastructure concentrates into smaller "secure core" systems, isolated and heavily verified while less critical applications run with limited permissions.
The Ethereum co-founder has returned to the AI security theme repeatedly this year. In February, he suggested splitting AI productivity gains between speed and security, and in May he endorsed formal verification tools like Lean for high-assurance development. His latest post extends those arguments to a broader claim, framing mathematical proof as the most credible answer to AI-driven attack tools across blockchain and traditional internet systems.
Read Next: Iran Settles Hormuz Shipping Cover In Bitcoin, Eyes $10B Haul
