Claude’s proofs across 123 libraries make the limits of “verified” worth reading

Read the theorem before the victory lap

“Verified” is most useful when followed by a description of exactly what was verified. Anthropic’s October 22 research announcement, produced in collaboration with Theorem, reports security proofs across 123 open-source libraries using Claude. That is an ambitious application of AI to software assurance. It is not a declaration that those libraries are now free of every possible bug.

The work concerns compiled programmes at the RISC-V assembly-code level. Anthropic says Claude proved that selected executable artefacts would exit normally without specified crashes for inputs below a defined size, across modelled operating-system responses and memory layouts, subject to stated assumptions. The company is publishing a subset of proofs and the associated semantics so others can inspect and check them.

Those boundaries are not qualifications to hide at the end. They explain the achievement. The claim is stronger than observing that a programme passed a collection of tests, but narrower than saying every use of an entire library is secure. Keeping both sides in view is the difference between understanding formal verification and using the phrase as a marketing label.

Testing samples; a proof describes a set

A conventional test exercises a particular case. Fuzzing generates many cases in search of failures. A formal proof instead reasons about all cases encompassed by a specified model and claim. Anthropic’s project uses fuzzing entry points as starting places for those claims. The route matters: the work does not magically include every operation a library exposes merely because the library’s name appears in the research.

The model writes the proof, but an external proof checker determines whether it is accepted. Theorem’s official OSS Verify page identifies the Rocq kernel as the checker for its delivered proofs. This creates an important separation between generating an argument and checking its formal validity. A persuasive explanation from a language model is not itself the security guarantee.

A binary-level approach also changes what is being described. Theorem says its theorem concerns the compiled fuzz test, rather than just a translation of the source code. That can bring the claim closer to the instructions the modelled processor executes. It does not make the model identical to every processor, runtime library or deployment configuration used in the real world.

Sometimes the proof followed a patch

There is a consequential step between finding a problem and reporting a successful proof. Anthropic says Claude was allowed to patch code when its proof attempts exposed bugs. Those changes caused the specification to be regenerated, and Claude then proved the new specification for the patched code. Some guarantees therefore concern changed artefacts, not necessarily the unmodified upstream releases of the libraries named in the project. The team says the complete proofs it is publishing are for fuzz tests that did not require patching.

A proof of the stated no-crash property does not, by itself, establish that a patch preserves every intended behaviour of the original programme. Functional changes need their own review against the relevant requirements. This is a boundary of the guarantee, not a finding that a particular patch damaged a library. For someone reproducing the work, identifying the exact patched or unpatched artefact is part of interpreting the result, rather than a clerical detail to leave until deployment.

The machine model is part of the result

Anthropic lists single-threaded, static RISC-V binaries linked against musl libc among its assumptions. It explicitly notes the gap between that environment and common x86 or ARM deployments dynamically linked against glibc. A proof for the modelled environment cannot simply be relabelled as a guarantee for those other environments. Closing the gap would require appropriate models and additional verification.

The claim’s input-size boundary also matters. Anthropic describes inputs under 64 MB; Theorem’s product page specifies up to 64 MiB for its compiled fuzz-test guarantee. This article does not turn those differently worded descriptions into an unqualified promise covering arbitrarily large input. The exact theorem delivered for a programme is what would determine its bound.

Coverage is another constraint. Anthropic says it did not verify every entry point in each library, that covering entry points would still not necessarily cover the whole library, and that misuse by a caller could create problems outside the proved property. It also notes that AddressSanitizer does not detect every memory-safety bug. These limitations describe what the reported proofs do not establish; they are not evidence that the proof checker failed.

The specification can still be the wrong promise

A valid proof can show that a programme meets a specification without showing that the specification captures everything a user needs. Anthropic states this explicitly: the checker cannot tell whether the spec matches reality. For a developer evaluating the approach, the human-readable claim and its assumptions therefore deserve at least as much attention as the fact that a checker accepted a proof.

As an illustrative example, a programme might never crash for the specified inputs yet return an incorrect result that the specification does not forbid. That would not contradict a no-crash proof. It would reveal that correctness of the output was a different property. The example is not a bug reported in this research; it shows why precise claims are essential to interpreting the result.

Theorem is offering its OSS Verify initiative to qualifying open-source projects for free, according to its official page. That is an invitation to a defined programme, not a guarantee of universal eligibility, immediate coverage or free verification of every commercial application. Developers would still need to establish what their programme’s theorem says and whether its model is relevant to the deployment they care about.

A new deliverable for a release process

The research suggests a practical direction for developer tooling: proofs could become reviewable release artefacts alongside tests and source changes. A team considering that workflow would need to know which binary the proof binds to, which specification it checks and what changes require a new proof. These are implications of the approach, not a report that an industry-wide release process has already changed.

Anthropic’s report remains a participant-authored research account, and Foundra has not independently executed the published proofs. Its importance is the prospect of reducing the effort involved in producing machine-checkable guarantees at a larger scale. The useful next question is not whether AI has made software “safe.” It is which precisely stated property can now be checked, for which executable, under which assumptions—and how much engineering work that saves.