It looks like the software world is entering a long cybersecurity winter, and my bet is that a lasting answer could come from mathematics. That is why a new article from Anthropic drew my attention this week: it shows formal proofs of software security now becoming feasible at a much larger scale.
Crisis after crisis, with no let-up: something reminiscent of the 'Great Invasions' of the 4th and 5th centuries, as I recently wrote. Major flaws keep surfacing in widely used software, flaws that were there all along, but whose discovery and exploitation demanded a sophistication that, until now, was out of reach. Anthropic's own deputy CISO, Jason Clinton, expects things to get "a lot worse before they get better", and advises holding on for about 18 months. In the age of AI, our digital empires, handwritten over decades, may simply be too vast, too interconnected and too vulnerable to defend through patches and empirical testing alone.
What could replace them? Perhaps a new kind of software that carries a mathematical proof of its security properties: built around invariants, what must remain true whatever the input, rather than around endless collections of tests.
Anthropic's Frontier Red Team worked with Theorem—a company whose motto is "Verify all software"—which helped model the machines and operating system behind the proofs. Claude wrote machine-checkable proofs for 239 entry points across 123 open-source libraries, directly on the compiled binaries, and found hundreds of bugs along the way, some that fuzzers were unlikely to hit. The guarantees are narrow and conditional, as they should be: no memory-safety errors or failed assertions, under explicit assumptions. The PHP and Node.js flaws of this month belong to exactly that class. Theorem now offers to do the same for other open-source projects.
Much as cryptography gave digital trust a mathematical footing, conditional on explicit assumptions, formal verification could do the same for software. Instead of hunting vulnerabilities one by one, we could prove, within stated assumptions, that whole classes of failures cannot occur.
Perhaps mathematics will come to the rescue of software after all?
