On October 22, 2026, Anthropic’s Frontier Red Team, working with the startup Theorem, reported that Claude had written machine-checked proofs for 239 fuzz-test entry points across 123 open-source libraries. Each proof shows that its entry point never crashes on any input up to 64 MB. Anthropic says the work took “a few weeks” and produced about 180 million lines of proof in Rocq, a proof assistant whose kernel checks every step. Along the way, Claude found bugs that, in Anthropic’s words, “had eluded detection for years, despite trillions of test runs.”
Anthropic’s yardstick is seL4, an operating system kernel whose correctness was formally proved. Its authors put the kernel’s development at 2.2 person-years and the proof at about 20.
The report came a day after Wiz disclosed PHP2Shell, flaws in the PHP engine found with frontier AI models; the NSA told organizations running PHP to update or take their systems offline. Wiz says the flawed code had been in the PHP engine for more than a decade.
Why proofs stayed rare
Formal verification means writing down in mathematics what a program must always do, then proving that the code does it on every possible input. A fuzz test checks the inputs it happens to generate, and a proof covers all of them. The cost kept the method in niches: Anthropic writes that verification has been practical “only in truly mission-critical applications, such as Airbus’s avionics code.”
A fuzz test turned into a theorem
The team avoided writing specifications by hand and started from Google’s OSS-Fuzz project, which runs fuzz tests for open-source software: small entry points that feed the code generated inputs and crash when something goes wrong, for instance when AddressSanitizer catches a bad memory access.
Each library and its fuzz test were compiled into a RISC-V binary, and the test became a statement: for every input under 64 MB, the program exits normally, with no memory-safety error and no failed assertion. Theorem’s formal models of RISC-V and of a Linux process define what running the binary means. Claude writes the proof, and the Rocq kernel checks it.
What remains to be trusted, per Anthropic, are the RISC-V and Linux models, the exact theorem statements and the Rocq checker. Rocq is a proof assistant like Lean, in which a formalization of the newly proved KLS conjecture appeared on GitHub this month.
180 million lines, checked by machine
A typical proof runs to about 600,000 lines, for binaries with a median length of 18,000 RISC-V instructions. The appendix says Claude wrote around one billion lines of Rocq in all, and about 180 million ended up in proofs that passed the checker. Most of each proof covers code every program carries, such as C startup and the sanitizer’s runtime: of the 630,000-line proof for cJSON’s 391-line parser entry point, only about a tenth concerns cJSON. Checking one proof takes from 30 minutes to several hours of CPU time.
The public subset is in the oss-verify-proofs repository, opened on October 22 under the MIT license: 60 entry points in 25 libraries, including OpenSSL, mbedtls, bzip2 and libpcap, checked with Rocq 9.2.0. Anthropic says it is not releasing proofs that may reveal an unpatched bug.
Bugs the fuzzers missed
Some targets became provable only after Claude patched the bugs it hit; the specification was then regenerated from the patched code and the proof went on. Anthropic says the effort “discovered hundreds of bugs.” To keep the model from rewriting a program into one that trivially never crashes, the team penalized every patch and audited all of them.
Fuzzers typically mutate small inputs, capped around 1 MB. Claude found a counter underflow in a decompressor that caused an out-of-bounds write only on inputs of about 20 MB with one rare layout, and an out-of-bounds read in an image decoder that needed a 64 MB input and over 2 GB of memory. It also rediscovered CVE-2026-56132 in libexpat.
In separate experiments, the team found a logic bug latent for more than a decade in one critical application, and while trying to verify a widely used PDF reader it found “as many security bugs in one week as are typically reported in a year.” The post names neither program.
Cheaper with newer models
Anthropic lists cost as a key limitation: a proof “can take hundreds of millions of tokens to produce.” On 36 small tasks built from OSS-Fuzz code, its chart shows Opus 5.5 proving half of them with about 40% fewer tokens than Opus 5.
Theorem tracks the trend on its own eval of 36 small C programs: across seven Anthropic and OpenAI models released between May and September 2026, verification speed went from 0.12 KB of machine code per hour for Opus 4.8 to between 0.56 and 0.91 for the three September models, with GPT-6 Astra the fastest. In Theorem’s fit, speed doubles every 1.9 months, against eight months in Epoch AI’s estimate for language models in general.
If models can be made to improve at verification much faster than their general capabilities, Theorem estimates that 95% of the machine code in nixpkgs, the Nix package collection, could be verified by the end of 2027 for about $134 million. Theorem sells verification and offers it free to qualifying open-source projects through OSS Verify, and four of the six authors of that post appear on the team list of Anthropic’s report.
The same week, on the attack side
On October 21, Wiz Research disclosed PHP2Shell, memory-safety flaws in the PHP engine present “for more than a decade” in nearly every version back to PHP 5.4, with severity up to CVSS 9.2. Wiz found the first one on August 19 using Wiz Atlas, Gemini 4 Argon and GPT-5.6 Sol. The company estimates that PHP powers 70% of websites.
The same day, Amazon said the flaws were “now being broadly exploited in the wild,” the Financial Times reported. Google asked sites that went down for the patch to serve an HTTP 503, and OpenAI said that “to our knowledge, frontier AI found these vulnerabilities before attackers did.” The Anthropic work is a separate project, and PHP is named neither in the report nor among the 25 libraries with public proofs.
What the proofs do not cover
The first point in Anthropic’s limitations section reads “‘Formally verified’ does not mean ‘bug-free.'” A proof holds for the model of the machine, and these models describe single-threaded, static RISC-V binaries linked against musl, while most people run these libraries on x86 or ARM with glibc. AddressSanitizer does not catch every memory-safety bug, and not every entry point of each library was verified. The repository’s README adds that Theorem’s Linux model “is best effort and not complete” and that no proof in the release rules out a run that never ends.
A section of the appendix looks at the proofs from the point of view of a human formal verification expert. The agent proofs are “verbose,” and human proof engineers “would have immediately introduced abstractions” to factor out the repetition. Experience from MachCSL, another agent-based verification project, suggests the style may not scale to more complex programs: there, “the agents hit a complexity wall.”
Beyond the 60 public proofs, the count rests on Anthropic’s report, which gives no total cost or compute figure and does not say which Claude model ran it.
What it means
Until now, a machine-checked guarantee meant a specialist team and years of work per system, so it went to kernels and avionics. Anthropic and Theorem describe a pipeline that turns existing open-source tests into theorems and has a model prove them across a catalog of libraries. Anthropic’s token counts and Theorem’s speed tests, both run on small programs, show the cost falling.
The guarantee is narrower than seL4’s, and both figures, 20 person-years and a few weeks, come from Anthropic’s post. Claude’s proofs cover crashes and the memory errors a sanitizer can see, at specific entry points, on a modeled RISC-V Linux machine. The seL4 proof covers the functional correctness of the whole kernel.
The volume of code to check is growing as well: Anthropic reported more than 30,000 merged code changes a day in September. These proofs rule out the memory-safety errors AddressSanitizer can detect, at the entry points they cover. Wiz classes all the PHP2Shell flaws as memory-safety issues.
Anyone can rerun the 60 public proofs today, against public RISC-V and Linux models. The open questions are the cost per proof, whether the verbose style holds on larger programs, and whether Theorem’s 1.9-month doubling continues past seven models and four months of releases. The next markers are independent rechecks of the public proofs, models of x86 and glibc that match the machines people run, and how many OSS-Fuzz projects enroll in OSS Verify.
Sources
- LLMs are making formal software verification feasible at a much larger scale, Anthropic, October 22, 2026
- Appendix: LLMs are making formal software verification feasible at a much larger scale, Anthropic, October 22, 2026
- theorem-labs/oss-verify-proofs, Theorem on GitHub, October 22, 2026
- Bootstrapping the Verified Software Stack, Theorem, September 29, 2026, updated October 19
- Comprehensive Formal Verification of an OS Microkernel, G. Klein et al., ACM Transactions on Computer Systems, February 2014
- PHP2Shell: AI uncovers critical RCE vulnerabilities affecting 70% of the Internet, Wiz Research, October 21, 2026
- Hackers got a four-day head start on epic PHP2Shell vulnerability, Financial Times, via Ars Technica, October 22, 2026
Header image: chart by MACCUS, data from Klein et al., ACM Transactions on Computer Systems (2014) and Anthropic (October 22, 2026)
