← all musings

The Theoretical Bug Just Expired

"Nobody can exploit it" used to be a triage rule. Now it's a countdown. In the new regime there are only two kinds of code: proven, and waiting.

“Nobody can figure out how to exploit it” used to be a good reason to leave a bug alone. That reason is gone.

In 2024, a security audit of PHP, funded by the Sovereign Tech Agency, flagged an issue now tracked as CVE-2026-109618. According to Drew Silcock’s roundup of this week’s incidents, the PHP Foundation mostly set it aside. It had bigger concerns, couldn’t agree on a fix, and nobody could work out how to turn the theoretical issue into a working exploit. This week two teams found it anyway, along with a sibling bug, CVE-2026-109619. One was Calif, working under OpenAI’s “Patch the Planet” program. The other was Wiz. Both bugs allow remote code execution, and both teams used frontier models to find them and build the exploits. In the same week, Anthropic published work in which Claude, in a collaboration with Theorem, proved security properties at the RISC-V assembly level in 123 open-source libraries. Along the way it found bugs that had gone undetected for years, despite trillions of test runs.

Those are two halves of one story. The price of exploiting a bug collapsed, and so did the price of proving one isn’t there.

Start with the strongest case for what the PHP Foundation did, because it wasn’t negligence. In open source, maintainer hours are the scarcest thing there is. Exploitability is the filter every security team uses, because it’s the cheapest stand-in for real risk. If skilled people can’t turn a finding into a weapon, the typical attacker can’t either, so you fix what’s weaponizable and park the rest. That logic held for decades because building an exploit was expensive. The cost of turning a theory into a working attack was the moat.

That moat is gone. Silcock’s sharpest line is that LLMs are very good at taking a theoretical vulnerability, even a vague description of one, and building it into a full exploit. Once that’s cheap, “theoretical” stops being a category and becomes a waiting list. Every finding parked because nobody could weaponize it is now a work order for whoever points a model at it first. The PHP audit didn’t fail to find the bug. It found it two years early and filed it in a drawer that is no longer locked.

Everyone reads weeks like this as proof that offense is winning. I think that’s half right, and the other half matters more. Formal verification was always the right answer to “is this code safe?” Anthropic is blunt that it historically took years of expert effort, which made it impractical for most real projects. Now its price is falling too. When exploits and proofs both get cheap, the comfortable middle disappears. That middle was code that’s “probably fine, we tested it a lot.” Trillions of test runs missed the bugs Claude found while writing proofs. Testing checks a sample of cases. A proof covers every case the spec describes. That gap used to be an academic point. Now it’s an operating decision.

Here’s the serious objection. A proof covers only what you specified. Prove the wrong property and you get false comfort with a math degree. And 123 libraries isn’t the internet. Both points are true. But notice where they push the problem: away from writing patches and toward writing specifications, the work of deciding what “secure” means for a given library. That’s a far better use of a scarce maintainer’s week than ranking a backlog by guessing which bugs are too hard to weaponize. One caution: models don’t fix governance. Part of why the PHP bug sat for two years is that people couldn’t agree on a fix. No proof assistant settles that argument for you.

The bigger issue is who holds the tools. One of the exploit teams worked under OpenAI’s “Patch the Planet” program. The other, Wiz, sits inside Google Cloud, as Silcock notes. Anthropic is publishing a subset of its proofs, and Theorem a Claude skill for writing them. Open-source security now depends heavily on how three labs decide to spend their compute on defense. Public funders like the Sovereign Tech Agency paid for an audit that produced a finding nobody acted on. The lesson for them is to pay for proofs and fixes, not findings. A finding with no fix attached used to be a to-do item. Now it’s a liability with a timestamp.

The stakes are simple. For any project still sorting its security backlog by “can anyone exploit this,” the backlog has become a target list. In the new regime there are only two kinds of code: proven, and waiting.