Anthropic and Theorem Say Claude Wrote Machine-Checked No-Crash Proofs for 239 Entry Points in 123 Open-Source Libraries, on RISC-V Only

The same AI progress that is speeding up bug-hunting is now being pointed at proving that some bugs are absent. The result is narrower than a security guarantee but much broader than formal verification has usually reached. On Thursday, October 22, Anthropic and its collaborator Theorem said that, over a few weeks, Claude patched the bugs it found and then proved that 239 entry points across 123 libraries in Google's OSS-Fuzz project cannot crash on any input up to 64 MB. Anthropic says the proofs run to about 180 million lines of the Rocq proof language and are machine-checked. They apply to the compiled RISC-V binaries under a stated set of assumptions, not to the libraries as most people run them.

What was proved

OSS-Fuzz runs developer-written fuzz tests, which feed huge numbers of semi-random inputs into a program's test entry points to provoke crashes. Anthropic says it converted those tests into formal specifications over the compiled RISC-V instructions, stating that the test never crashes for any input under 64 MB. Because OSS-Fuzz builds C and C++ code with AddressSanitizer, a crash includes the improper memory accesses that tool detects. Claude wrote the proofs, and the Rocq proof checker verified them against the specifications, using Theorem's formal models of RISC-V instructions and Linux processes. Anthropic says a typical proof runs to about 600,000 lines and covers a binary with a median of 18,000 RISC-V instructions.

The proofs assume that each program runs as a single-threaded static binary, linked against musl libc, with a fixed memory budget on a RISC-V CPU under Linux. What a developer has to trust, Anthropic says, is the RISC-V and Linux models, the exact theorem statements, and the Rocq checker itself, along with the hardware, operating system and compiler the checker relies on.

Bugs found on the way

Anthropic says that trying to prove these specifications turned up hundreds of bugs, which Claude was allowed to patch before re-proving the updated code. It describes a counter underflow in one library's copy of a decompressor that led to an out-of-bounds write, but only on inputs of about 20 MB with one rare layout. It says Claude also found an out-of-bounds read in an image decoder that needed a 64 MB input and over 2 GB of memory, and rediscovered CVE-2026-56132 in libexpat. Anthropic argues that fuzzers, which typically cap inputs at around 1 MB, would be unlikely to find many of these. Letting Claude patch code opens the door to reward hacking, Anthropic acknowledges, so it says it penalized patches, rewarded proofs that showed how few inputs a patch changed, and audited the patches.

In separate experiments, Anthropic says Claude proved that the Linux kernel's zlib implementation correctly implements the RFC 1950 format at the x86 binary level, using x86 semantics that Claude itself generated. It says Claude also built a Rust interpreter for a large subset of Python that matched CPython's behavior on 99.95% of 1.7 million randomly generated programs. Anthropic says it is publishing a subset of the proofs, the RISC-V and operating-system semantics, and specifications for fuzz tests it could not prove. It says it is withholding proofs that could reveal an unpatched bug. Theorem is offering to run the same pipeline for other open-source projects and is publishing a Claude skill for developers, according to Anthropic.

What it does not show

Anthropic's own post says "formally verified" does not mean "bug-free." Most users run these libraries on x86 or ARM, dynamically linked against glibc, which the RISC-V proofs do not model. AddressSanitizer does not catch every memory-safety bug, not every entry point in each library was verified, and a program that calls a library incorrectly can still corrupt memory. Anthropic also says the proofs can take hundreds of millions of tokens to produce, which limits how widely the method can be used for now. It reports that Opus 5.5 proved half of a 36-task test set with about 40% fewer tokens than Opus 5, and that agents sharing proofs used 17% fewer tokens.

The work comes in a month of AI-assisted bug-finding. AI-assisted research helped find the PHP2Shell flaws in PHP, and Fortinet has said its October 22 updates carry fixes found through AI-assisted testing. Anthropic is pitching proofs as the next step after finding bugs: showing that a class of them is absent. Its figures describe what was proved on one architecture, not how secure the libraries are in production.

Limits

• Every figure here comes from Anthropic's post. We did not run or check the published proofs, and we found no independent outlet that had examined them.
• Our Theorem source is partial. We read only the index entry on Theorem's blog, which says the collaboration proved security properties in more than 100 open-source libraries at the assembly-code level, and not Theorem's full post.
• Anthropic describes its effort as, to its knowledge, the first of its kind at this scale. We have not verified that claim and do not repeat it as fact.
• Anthropic does not list all 123 libraries or give an exact bug count in the main post. We did not open the appendix or the published proof repository.

Sources

• Anthropic: LLMs are making formal software verification feasible at a much larger scale (October 22, 2026)
• Theorem: Blog index, October 22, 2026 entry (accessed October 23, 2026)
• Times of AI: PHP2Shell, PHP patches two critical RCE flaws found with AI-assisted research (October 21, 2026)
• Times of AI: Fortinet says its October 22 updates carry critical fixes from AI-assisted testing (October 22, 2026)