> ## Content Index
> Fetch the complete content index at: https://all-about-ai.ghost.io/llms.txt
> Use this file to discover other available public pages before exploring further.

# Anthropic says Claude wrote formal proofs for code in 123 libraries
- URL: https://all-about-ai.ghost.io/news/anthropic-says-claude-wrote-formal-proofs-for-code-in-123-libraries/
- Published: 2026-10-26T15:11:09.000Z
- Updated: 2026-10-26T15:11:09.000Z
- Description: The collaborators report about 180 million proof lines in results that passed a formal checker, but the guarantees cover selected tests and do not show the programs always finish.
- Author: Frontier Models Desk
- Tags: News, models-research, anthropic, claude, theorem, open-source, formal-verification

In work announced October 22, [Anthropic](https://www.anthropic.com/research/formal-verification?ref=all-about-ai.ghost.io) and Theorem say Claude patched bugs and generated machine-checkable proofs for 239 OSS-Fuzz testing entry points across 123 open-source libraries. A proof can cover every modeled input inside a defined boundary instead of sampling generated inputs and hoping to hit a dangerous case. It does not mean that all 123 libraries are safe: each entry point is one route into a library that developers prepared for testing.

The work took a few weeks, the collaborators report, and produced about 180 million lines in proofs that passed the checker and satisfied the specification. Developers do not have to read every line or trust Claude’s judgment about correctness. Rocq’s separate checker decides whether each mathematical argument proves its exact statement. People still have to decide whether that statement and the modeled environment cover the behavior they care about.

239Testing entry points, collaborators report

123Libraries represented in the reported results

180MAccepted proof lines, collaborators report

60 / 25Entry points / libraries in the public release

One reported finding shows why exhaustive reasoning can help. While attempting a proof, Claude found a decompressor counter underflow that required a specially arranged input of around 20 MB and could cause an out-of-bounds write. Anthropic says conventional fuzz testing, which feeds generated and mutated inputs to programs, typically caps inputs at 1 MB. But Anthropic has not published a bug-by-bug record establishing the reported hundreds of discoveries, their severity or whether maintainers accepted the fixes. The example shows what proof attempts can expose, not that verification will always beat a differently configured fuzzer.

The project begins with tests from [Google’s OSS-Fuzz initiative](https://github.com/google/oss-fuzz?ref=all-about-ai.ghost.io). The team compiled each library and test into RISC-V instructions, then used Theorem’s mathematical model of those instructions and Linux processes to define the claim Claude had to prove. Claude wrote the Rocq proof, and the checker judged it. If Claude patched a bug, the claim was regenerated for the changed program. The guarantee therefore follows that resulting binary and does not automatically apply to code already installed elsewhere.

The [public archive](https://github.com/theorem-labs/oss-verify-proofs?ref=all-about-ai.ghost.io) spells out the contract. For covered inputs within the stated size limits, provided the ordinary build stays within its memory budget, the ordinary and instrumented builds avoid modeled errors and agree on observable behavior such as output bytes, exit status and final file contents. The instrumented build adds checks intended to catch memory errors and other invalid operations.

Every input, within a defined boundary 

The project targets inputs smaller than 64 MB through selected testing entry points. Its guarantees depend on a particular binary and a model of a single-threaded RISC-V Linux environment. They do not certify an entire library, automatically transfer to ordinary x86 or ARM builds, or establish that execution always finishes.

A test can encode more than the absence of memory faults. Anthropic gives the example of a compression test that checks whether decompression restores the original input. If a mismatch triggers an assertion, proving that assertion never fails establishes that property within the proof’s domain. Wrong answers the test never checks remain outside the guarantee, as do memory errors the instrumentation cannot detect.

One limit is easy to miss. Anthropic says the programs “will always exit normally,” but the archive says none of the released proofs establishes the separate *halts* statement required to exclude nontermination. A program that runs forever has not delivered a successful result. This does not show that any covered program actually loops forever. It means the public proofs do not justify a promise that each one always finishes.

A checked proof can also be correct even if the machine model does not perfectly match reality. Theorem’s [documented scope](https://github.com/theorem-labs/rocq-linux-process-semantics/blob/f1006fe8178338a499b5e5c41be83006c4edd058/SCOPE.md?ref=all-about-ai.ghost.io) includes one thread, no signal handlers and a limited filesystem. Outside scrutiny also reaches only part of the headline result: the archive contains proofs for 60 entry points in 25 libraries. Anthropic says it published proofs for tests that required no patching and withheld material that could reveal unpatched bugs. The release makes the method and that subset inspectable, but does not independently establish the full 239-entry-point total.

Routine use remains further away. [Theorem’s service](https://theorem.dev/oss-verify/?ref=all-about-ai.ghost.io) offers free verification to qualifying open-source projects, prioritizes smaller binaries and requires static RISC-V builds that may need porting. Proof generation can take multiple days, and Theorem says AI-generated findings and patches are not guaranteed human review. Anthropic’s [technical appendix](https://www-cdn.anthropic.com/files/4zrzovbb/website/6867eadf760258fa8b42a504600cd3c036d16358.pdf?ref=all-about-ai.ghost.io) gives checking times of 30 minutes to several CPU-hours per proof. Neither collaborator discloses a project-wide cost or expert-labor total. For now, this looks more like selected batch assurance than an everyday per-commit check. The useful next benchmark is whether maintainers can keep proofs current as code changes and extend them to the systems users actually run at a sustainable cost.