Can formal verification guarantee software security in the age of AI?
Protocol design · 2 participants · 2 quotes · 2026-09-16 ~ 2026-09-18
Vitalik Buterin argued against the common view that AI hacking will destroy cybersecurity. If AI can prove Navier-Stokes or Fermat's Last Theorem, he said, it can also prove "this program is secure" as a mathematical theorem, so cybersecurity is fundamentally defense-favored. Sam Williams (samecwilliams) of Arweave and AO agreed with the direction but added a caveat: verified models alone are not enough, and the translation gap between the model and the actual code has to be closed with property-based testing.
Background
Formal verification is a technique that mathematically proves a program satisfies a specification (definition). According to Vitalik's argument, the definition of security can itself be subtle enough to run to thousands of lines, but a definition is a much smaller attack surface than an implementation, and different definitions can be added together (additive) and verified jointly. The translation gap Sam Williams pointed out is the question of whether the verified model matches the code that is actually deployed. seL4 (2009) is the representative case, shipping with a large body of assembly and C code that has no formal proof attached. He argues this gap should be narrowed with property-based testing so that both the model and the actual code are verified.
Why it matters
Whether the AI-era security bet leans toward formal verification will shape how Ethereum prioritizes formal verification investment and managing risk in "deployed code." Vitalik presents holding about 90% of his net worth in crypto as a practical expression of this bet, so it is worth watching whether tools that make definitions human-readable and reduce the translation gap actually raise real security standards.
Key points
- Can software security be proven like a mathematical theorem using formally verified definitions?
- How do we close the translation gap between a verified model and the code actually deployed?
- Is a definition a smaller attack surface than an implementation?
For — If you verify the definition, security favors the defender
vitalik.eth
- If AI can prove Navier-Stokes or Fermat's Last Theorem, then no matter how complex a program is, it can prove "this program is secure" as a mathematical theorem.
- The definition of security can be subtle enough to run to thousands of lines, but for security-critical components a definition is a much smaller attack surface than the implementation, and definitions are additive and can be proven together.
- Making definitions human-readable may be the only high-level language that matters right now.
Neutral — Model verification alone is not enough
🐘🔗 sam.arweave.net
- I agree with the direction, but model verification alone is not sufficient, and the theorem prover itself almost certainly has bugs.
- On top of the spec gap Vitalik described, there remains a translation gap over whether the verified model matches the code actually deployed, and seL4 is an example.
- In practice, formal verification and property-based testing should be used together, narrowing "hope the code matches the model" to "the invariants must match the theorems."