From Patching Bugs to Proving Them Gone
A Y2K moment for software security
Dear SoTA,
ARIA has a £20m call for AI-enabled formal methods in cybersecurity, open until 1st July. I encourage your members to apply. In this letter, I want to share why I’m excited about this call, and why I think AI-enabled formal methods could underpin a Y2K-scale effort to harden the critical software society runs on.
Bug-hunting at machine speed
Earlier this year, Nicholas Carlini, security expert and research scientist at Anthropic, gave an eye-opening talk on what frontier AI models can now do in the realm of cybersecurity. Reportedly, Anthropic’s latest series of models found thousands of vulnerabilities, among them finds like a Linux kernel bug that had gone unnoticed since 2003, or a high-severity bug in OpenBSD that had survived twenty-seven years in one of the most carefully audited codebases ever written. The recipe for finding these vulnerabilities was almost mundane: a short script that asked the model to read each file, find something exploitable, and check that it worked, with a little expert steering along the way.
To most people in the cybersecurity community, this reads like concerning news. Models that find, in minutes, bugs that survive decades of expert auditing are poised to fundamentally alter the economics of cyber offense: groups who would otherwise lack the expertise could start launching sophisticated attacks; running many bug-finding agents in parallel could surface vulnerabilities at a volume that hands attackers a rich menu of exploits and temporarily overwhelms our defensive capacity to patch.
This matters because a lot of software is part of the critical infrastructure that society relies on in its functioning: operating systems, browsers, and cryptographic libraries, but also power grids, water treatment plants, telecoms, medical health records or payment systems. It’s no secret that much of this critical software is not as hardened as we would like it to be. When these systems come down, the costs snowball quickly, plausibly even resulting in lives lost.
So what do we do about it?
One option is to turn the same AI capability toward defence: find the bugs and patch them before anyone else does. We should do this! The more bugs are fixed, the harder it becomes to chain a series of vulnerabilities into a real, high-stakes exploit.
The problem is that ‘find-and-patch’ is, ultimately, still a cat-and-mouse game. Better bug-finding models help attackers and defenders approximately equally. But the defenders must also ship a fix through change windows, legacy systems, and uptime requirements, which takes time. We see this already: a standing backlog of patches that are known but not yet implemented. That gap is attacker time. And even a patch that ships closes only a single hole. How many holes are there yet to be found?
Exiting the cat-and-mouse game
What if, instead of patching bugs one by one, we could rule out entire classes of them in one fell swoop? Or, more ambitiously: what if we could write code that probably has no such bugs in the first place? Attackers would find nothing to get started with. And it is not fantasy: formal methods promise exactly that, and the community has demonstrated it works. The HACMS programme, for example, run by DARPA from 2012 to 2017, built formally verified flight-control software, including for a manned helicopter, that expert red teams could not break.
But, to be frank: formal methods have never quite made the jump from being clearly useful in principle to being demonstrably useful in practice, at scale, and across the wide range of industry-grade software systems that matter. No knock on the community: it has delivered a great number of wonderful projects over the decades. But the bottom line stands: formal methods remain a specialist’s instrument, and haven’t become industry standard.
Not yet, at least!
A key problem with formal methods is that they are costly – both in time, and in specialised expertise. Verifying the seL4 microkernel took about 27 person-years for 9,300 lines of code. At that pace, you don’t harden a power grid, let alone an economy. Checking a proof is cheap and mechanical; finding one is hard.
At least it’s hard for humans. As it turns out, AI agents are getting pretty good at it! In 2024, DeepMind’s AlphaProof reached silver-medal standard at the International Mathematical Olympiad by writing formal proofs in Lean. The same capability is now reaching real software. On this 2025 benchmark of more than twelve thousand specifications, off-the-shelf models produced verified code from the specification alone for 82% of tasks in one proof language, 44% in another, and 27% in a third. Earlier this year, the team at the Lean FRO used general-purpose AI with no special training for theorem proving to port zlib, the compression library embedded in virtually every computer, to Lean and proved that decompressing a compressed file always returns exactly the original data.
Are we ready for prime time?
At ARIA, we think this means it’s time to ask the question again: how far beyond the current frontier can AI-enabled formal methods go? Can they move from securing software in principle to securing industry-grade critical software at scales and speeds that matter? Are they ready to power a Y2K-scale effort to harden our critical systems against AI-enabled cyber offense?
We intend to find out. The Safeguarded AI programme is putting £20m on the table for ambitious, fast-moving teams: take whatever AI and tooling you can get your hands on, and direct it at high-impact targets – components where machine-checked proof would decisively bolster our societal resilience. Projects will run in eight-week sprints, so that ambition recalibrates continuously to the moving frontier of what’s possible. To keep the feedback grounded, an independent red team stress-tests what teams ship, every cycle.
Top of mind for us is protecting critical infrastructure. Promising avenues include verified, retrofittable components that protect network boundaries, or hardened foundational software (operating systems, browsers, compilers, etc.) where hardening one component protects thousands of systems downstream. Then there is the machine-learning infrastructure behind AI training, evals, and inference, fast becoming critical infrastructure in its own right. Another valuable target class might be the very proof checkers that formal methods rely on. Once the world starts directing AI at generating proofs at scale, it matters even more that we can trust them to be sound. But these are examples, not a menu: if you see a higher-impact target we haven’t thought of, we want to hear about it.
What we’re after is not just technically impressive artifacts, but real-world impact. That will require real grit, and a compelling plan for how the verified system will be adopted where it’s needed to actually start protecting lives and livelihoods. We will help you get there. Beyond funding, we will work with you to iterate on targets, keep you ambitious, connect you to our stakeholder network of critical-infrastructure operators to ground your specs and open adoption paths, and more.
To be clear, this undertaking is not without its own, important challenges. For one: while AI is poised to help speed up proof search, a proof is only as strong as the specification it checks against and the assumptions beneath it. And getting those right for a real system, and doing so scalably, remains genuinely hard.
Y2K is remembered as the disaster that never happened because thousands of teams did the unglamorous work ahead of time. AI-enabled cyber offense is our millennium bug, minus the certainty of the date. Come do the work that makes it a non-event. And if you know the team who should build this: send them this letter.
To learn more and apply, check out our website. The deadline is 1 July 2026.
Yours,
Nora Ammann
Nora is Programme Director for Safeguarded AI at ARIA. She has spent nearly a decade working on making transformative AI go well. Her work spans AI assurance – hardware guarantees, formal verification and the coordination needed for safety claims between untrusting parties. She previously founded Principles of Intelligence, bringing together AI researchers, neuroscientists, and physicists to study the foundations of intelligence behaviour.
Write to the Society for Technological Advancement on letters@ilikethefuture.com.