Buterin Rejects AI Cybersecurity Doom Claim, Cites Formal Verification

Ethereum co-founder Vitalik Buterin has rejected the growing narrative that increasingly capable AI hackers will make cybersecurity impossible to defend, arguing instead that advanced AI could give defenders a structural advantage. In a post on X on September 16, 2026, Buterin stated that cybersecurity is "naturally defense-favoring once people get their shit together," and that he disagrees with the view that AI hacking means cybersecurity is doomed. Buterin's argument centers on formal verification, a technique that uses mathematical proofs to determine whether software behaves according to predefined security properties. He suggested that sufficiently advanced AI could make this process practical even for complex systems, comparing it to AI solving famously difficult mathematical problems like Fermat's Last Theorem. "If AI can prove Navier-Stokes and FLT, then AI can prove the statement 'this program is secure' as a mathematical theorem," Buterin wrote. "Even if the program is very complicated." However, Buterin emphasized that the hardest part of this approach is defining what "secure" actually means.