Vitalik Buterin rejects AI cybersecurity doom claim

Vitalik Buterin has rejected the claim that increasingly capable AI hackers will make cybersecurity effectively unwinnable, arguing on Sept. 17 that advanced verification tools could eventually give defenders a structural advantage.

Buterin wrote in his Sept. 17 post on X that he disagrees with the increasingly common view that “AI hacking means cybersecurity is doomed.” He said people who continue holding cryptocurrency are implicitly betting that secure digital systems can survive stronger automated attacks, adding that roughly 90% of his own net worth remains in crypto.

His argument centers on formal verification, a technique that uses mathematical specifications and proofs to determine whether software behaves according to predefined properties. Buterin used advanced mathematical theorem proving as an analogy, saying sufficiently capable AI could help prove that “this program is secure” even when the software itself is complex.

Buterin says formal verification can favor defenders

Buterin’s argument does not treat AI security as a race where defensive researchers simply find bugs before attackers. His post instead describes a model where developers define the properties a system must satisfy, then use automated proof tools to establish that the implementation obeys them.

Ethereum’s own formal verification documentation describes the technique in narrower terms. It says formal verification can mathematically prove that a smart contract complies with a formal specification, offering stronger guarantees than ordinary testing for the properties included in that specification.

The same Ethereum documentation identifies an important limitation behind Buterin’s comments. A proof establishes that software satisfies the specification being checked; it does not automatically prove that developers defined every security property correctly. Poorly chosen or incomplete specifications can leave behavior outside the proof.

Buterin made the same distinction in his post. He argued that defining “security” too narrowly can omit attack paths involving areas such as protocols, servers, databases, networking layers, caches or other supporting components. His proposed direction is therefore to verify more of the complete system instead of labeling a small group of modules as security-critical.

Buterin had already described AI-assisted formal verification as a possible “final form” of software development. His earlier comments applied the approach to areas including Ethereum consensus, zero-knowledge systems and quantum-resistant cryptography.

Ethereum is already testing AI-assisted security

Ethereum researchers are already using AI in security work, although current systems remain far from automatic proof of whole-system security.

The Ethereum Foundation Protocol Security team reported in July that coordinated AI agents had found real defects in systems used by Ethereum. One confirmed finding involved a remotely reachable crash in Rust libp2p’s Gossipsub networking implementation.

The flaw became CVE-2026-34219. The U.S. National Vulnerability Database record says versions before 0.49.4 could be crashed remotely through a crafted PRUNE message that triggered an arithmetic overflow during Gossipsub backoff handling. Version 0.49.4 fixed the issue.

The Foundation’s security team said vulnerability discovery was not the hardest part of the AI workflow. Researchers found that AI agents frequently generated convincing reports involving unreachable execution paths, debug-only failures or formal proofs that technically passed while proving a weaker property than intended.

Independent reproduction remained a requirement before the team accepted a finding. The Foundation said automated checks and human review were needed because an agent could produce a valid-looking proof that failed to constrain the software behavior researchers actually wanted to test.

The Foundation’s experience was described as a triage problem: AI could generate large numbers of candidate vulnerabilities, but researchers still had to determine whether each issue was reachable and meaningful in production.

Formal verification is entering Ethereum’s protocol roadmap

The Ethereum Foundation has separately made formal verification part of its current protocol research program. In its Sept. 7 protocol priorities update, the Foundation said formal verification would serve as cross-cutting tooling across its remaining multi-year research areas. The document covers work on privacy, state, zkEVM development, post-quantum security and other protocol components through 2029.

The same roadmap says development of an L1 zkEVM is expected to advance formal-verification tools, workflows and verified cryptographic components. Ethereum researchers are working toward a system where validators eventually verify succinct execution proofs instead of independently re-executing every block.

A separate Ethereum Foundation project launched in August is already combining AI agents with machine-checked proofs. The better.codes project lets researchers direct AI systems at a cryptographic soundness problem formalized in Lean, while the Lean kernel checks whether submitted proofs satisfy a fixed theorem statement.

The Foundation’s Q2 funding report lists further work combining large language models with formal methods. Projects include ETHeorem for checking Ethereum client implementations against specifications, SPECA and LeanAgent for automated protocol compliance work, and formal verification involving RISC-V zkVM infrastructure.

Ethereum’s updated technical roadmap gives formal verification a role alongside privacy, zero-knowledge proofs and post-quantum protection. Buterin’s Sept. 17 comments therefore continue an existing research direction instead of announcing a new upgrade or scheduled fork. His post did not name a new EIP, deployment date or mandatory rule requiring every Ethereum program to undergo formal verification.

Current AI evidence shows stronger offensive capability too

Recent cybersecurity research supports the concern that AI is making attackers more capable, even as defensive use expands. Anthropic said in itsSeptember threat intelligence report that it had observed malicious actors using AI to automate vulnerability research, exploit development and multi-target campaigns. The company said some operators maintained automated workflows that could conduct vulnerability research continuously.

Earlier research from Anthropic found similar evidence at scale. Its coordinated disclosure dashboard said that, by Aug. 26, the company had disclosed 2,300 AI-discovered vulnerabilities across 392 open-source projects, with 421 patched upstream at that point.

Anthropic has described the same technology as useful for defense. Its Project Glasswing initiative reported using frontier models with security companies and software vendors to locate high- and critical-severity flaws before malicious actors could exploit them.

The offensive side remains measurable. Anthropic’s June study examined 832 accounts associated with malicious cyber activity from March 2025 through March 2026 and found threat actors using AI across multiple stages of cyber operations. Buterin had already rejected a separate argument that AI-driven security risks could severely damage confidence in Bitcoin. He said network-layer problems could often be addressed through software and mining-infrastructure upgrades, while describing actual breaks of Bitcoin’s hashes or proof-of-work mechanism as highly unlikely.

Anthropic’s September report said its investigators had identified operators using AI-built exploit pipelines against security appliances and government targets, with some campaigns producing previously unknown vulnerabilities that attackers validated in their own test environments.