Anthropic said in research published on 22 October 2026 that it had worked with Theorem to use Claude to prove security properties in compiled code from 123 open-source libraries. The proofs concern RISC-V assembly, the instructions executed by a processor, and give software projects a possible way to check for specified errors across a range of inputs rather than rely only on tests that run individual cases.
Key points
- Anthropic reports an experiment across 123 open-source libraries, with proofs about specified failures in RISC-V binaries.
- The guarantees depend on limits on input size and assumptions about how the programs run.
- The public proof collection covers fewer targets than the reported experiment and does not prove that programs halt.
Claude’s proofs across 123 libraries
Formal verification starts by expressing a rule about a program in mathematical terms, then proving that the program follows it. Anthropic says the work has historically demanded years of specialist effort: it gives the seL4 operating-system kernel as an example whose implementation took two person-years and whose formal verification took 20. For this project, Claude wrote proofs about executable artefacts from open-source libraries, rather than attempting to specify every intended behaviour of each library.
The experiment covered 239 fuzzing entry points across the 123 libraries, according to Kingy AI, a technical publication that examined the announcement and public proof index. An entry point is the small program through which a fuzzer feeds inputs to the code being tested. Kingy AI reports that Claude generated roughly 180 million lines of accepted Rocq proof code. Rocq is the proof system used to check whether the mathematical argument satisfies its stated proposition.
A fuzzer tries many inputs and observes what happens. A proof instead has to account for every input inside its defined scope. One way to make a useful proposition is to write a check into the entry-point program that aborts when a rule is broken, then prove that execution cannot reach that abort. Kingy AI contrasts an image decoder checked only for crashes with one whose output is compared against a reference implementation.
Opening an image file could carry a stronger assurance against a crash if the decoder, input and running conditions matched a completed proof. Correctly displaying the image would depend on a separate check of the result, rather than the absence of an error alone.
RISC-V proofs have defined boundaries
Anthropic says Claude proved that the covered programs always exit normally without memory-safety errors or failed assertions for every input smaller than 64 MB, every modelled Linux response and every modelled memory layout. The claim assumes a single-threaded, statically linked program with a fixed memory budget, running on a RISC-V CPU under Linux. Those conditions define the program and environment to which the proof applies.
The input limit is written differently in the technical account: Kingy AI reports that the driver refuses inputs of at least 64 MiB, a binary unit, while Anthropic’s announcement uses 64 MB. For a project considering the method, the precise input boundary belongs alongside the binary and the property being checked. A proof about a compiled program under those conditions is a narrower undertaking than a proof of every possible use of its source library.
Anthropic says Claude also found bugs that had survived for years despite trillions of test runs. Its proposed use of proofs addresses a limitation of testing: however many individual runs pass, they do not exhaust every input in a defined range. The resulting guarantee still follows the rule chosen for the proof, so a rule concerned with errors need not establish that a decoder produces the intended output.
The public collection covers 25 libraries
Anthropic says it is publishing a subset of the proofs together with its RISC-V and operating-system semantics, the mathematical descriptions needed to interpret program behaviour. Kingy AI counted 60 entry points across 25 libraries and 138 proved statements in the public index at the revision it inspected. Some entry points have more than one statement, including statements for different sanitizer configurations, so the count of proved statements is larger than the count of entry points.
The public index includes named targets in cJSON, simdjson, OpenSSL and zstd. A proof for a target concerns its specified statement, rather than every operation in the library containing it. The publication says it did not independently rerun the Rocq proofs or reproduce the full experiment.
The released proofs do not establish that the programs always finish running. Its account distinguishes a statement that excludes specified errors from one that proves termination: a program could continue indefinitely without producing the error the first statement rules out. That distinction also separates the public collection from Anthropic’s description of programs always exiting normally in the larger experiment.
Anthropic says it is withholding proofs that could reveal unpatched bugs. The company says Theorem is offering its verification pipeline to other open-source projects and is publishing a Claude resource for initial code-verification work.
