Anthropic says Claude proved no-crash guarantees for 239 entry points across 123 open-source libraries

What happened: Anthropic said on October 22, 2026, that Claude produced formal proofs of security properties at the RISC-V assembly level in over 100 open-source libraries, in a collaboration with Theorem. Who's affected: maintainers and users of open-source C and C++ libraries, and developers weighing formal verification for their own code.

Anthropic calls it a first at this scale.

To its knowledge, Anthropic says, this is the first large-scale effort to use AI to formally verify production software at the assembly level. The company says Claude also found bugs that had eluded detection for years, despite trillions of test runs.

The numbers behind the claim.

Over a few weeks, Claude patched the bugs it found and proved no crashes for 239 entry points across 123 libraries from Google's OSS-Fuzz project, according to Anthropic. The proofs total about 180 million lines of Rocq. A typical proof runs about 600,000 lines, covering binaries with a median of 18,000 RISC-V instructions.

How fuzz tests became proofs.

Anthropic converted existing fuzz tests into a spec stating the test never crashes for any input under 64 MB. Claude writes the proof against Theorem's RISC-V and Linux process semantics, and the Rocq proof checker verifies it. Developers need to trust only those models, the theorem statements and the checker, Anthropic says.

Bugs fuzzers would likely miss.

Anthropic says the work surfaced hundreds of bugs. Examples include a decompressor out-of-bounds write triggered only by roughly 20 MB inputs, and a rediscovery of CVE-2026-56132 in libexpat. Fuzzers typically cap inputs at 1 MB, the company notes.

In plain terms.

Testing tries many inputs and hopes to hit the bad ones. A formal proof instead shows mathematically that no input in a defined range can crash the program. Anthropic says AI now makes writing those proofs fast enough to apply across many real projects.

Key terms.

• Formal verification: mathematically proving code always follows a defined set of rules.
• Fuzzing: automated testing that throws huge numbers of semirandom inputs at code to find crashes.
• Entry point: a test front door into a library; any crashing input is a bug.
• RISC-V: a processor instruction set, like x86 or ARM.
• Rocq: a proof assistant whose checker verifies each proof.
• musl: a lightweight C standard library, an alternative to glibc.

What the proofs assume.

Anthropic says the guarantees hold only under these conditions:

1. The program runs as a single-threaded, static RISC-V binary linked against musl.
2. It has a fixed memory budget.
3. It runs on Linux.
4. Inputs are under 64 MB.

Most deployments use x86 or ARM with dynamically linked glibc, which the proofs do not cover.

Formally verified does not mean bug-free.

Anthropic stresses that a proof only shows code meets its spec, not that the spec matches reality. AddressSanitizer does not catch every memory bug, and not every entry point in each library was verified, the company says.

What developers can do.

1. Review the subset of proofs and the RISC-V and OS semantics Anthropic is publishing.
2. Try Theorem's Claude skill to start verifying your own code.
3. Contact Theorem, which is offering to run the same pipeline for other open-source projects.

What's next.

Anthropic says proofs still take hundreds of millions of tokens, but expects costs to fall as models improve and proofs are reused. Extending coverage to x86 and glibc systems remains future work, according to the post.