Ethereum co-founder Vitalik Buterin says the rise of AI-driven hacking does not make cybersecurity an unwinnable contest, pointing instead to formal verification as a way to prove software secure. Rather than depending on the discovery of vulnerabilities, he argues, developers can demonstrate mathematically that programs meet defined security requirements.

In a May 18 blog post, which he shared on X, Buterin contended that AI could make such verification practical at scale, an approach he said matters most for critical systems, including cryptography, message protocols, and blockchain software.

Security Must Be Defined Before It Can Be Proved

Buterin said proving a program secure first requires defining what security actually means. He cited the encrypted messaging app Signal as an example, noting that encryption alone does not cover every security concern. A complete definition may need to account for message forgery, delivery failures, replayed messages, hacked devices, and leaked keys.

Hardware adds further complications. Physical signals can leak information, while details such as message size, sender identity, and timing can be revealing in their own right. Together, these considerations can push security definitions beyond 1,000 lines of code. Even so, Buterin argued that definitions remain a smaller target for verification than the underlying implementation.

Formal Verification Targets the Whole Program

Formal verification is not a new idea: it has long been applied in safety-critical fields such as aviation and medical software, where the cost of failure is high, but the effort involved has kept it rare in general-purpose development. Historically, developers have verified only sections they themselves identified as security-critical, largely because verification demanded substantial effort. Buterin argued that AI could change that equation, making full-program verification more practical and extending coverage to databases, networking, caching layers, and other components.

He framed the goal as distinct from the traditional model in which defenders race to discover vulnerabilities before attackers do. Under his approach, software becomes more resilient by proving that it satisfies security requirements. Definitions can also be combined when different groups establish separate requirements, he said, and where two definitions cannot coexist, developers can isolate the underlying design conflict. He acknowledged, however, that some user interfaces remain harder to handle.

Complex Verification Needs for Ethereum Software

Buterin identified message-passing protocols, sandboxes, SNARKs — compact cryptographic proofs that a computation was performed correctly — and fully homomorphic encryption, which allows computation directly on encrypted data, as areas where the distinction between definitions and implementations can matter. He tied the approach directly to Ethereum's development direction, saying blockchains need stronger software security, particularly in systems pursuing scalability and privacy.

The setting underscores the stakes: blockchain software is open-source and the networks it supports hold assets directly, so the same code sits in plain view of attackers and defenders alike — conditions under which guarantees that do not depend on who finds a flaw first carry particular weight.

His argument centers on mathematical verification rather than vulnerability discovery alone. Verification, he said, must extend beyond selected code sections: the definition demands careful work, while the implementation remains subject to formal checking. AI, in his view, could shoulder the scale of that process, covering databases, networking, caching, and other components. The question to watch is whether AI-assisted tooling can carry full-program verification into routine practice at production scale, including the user interfaces he flagged as the hardest cases.