Anthropic and Theorem reported on October 22 that Claude had produced no-crash proofs for 239 testing entry points across 123 open-source libraries. The work turns existing fuzz tests into mathematical claims about compiled programs, extending the check beyond inputs a fuzzer happens to try.
The boundaries matter immediately. The work targets single-threaded RISC-V Linux binaries with input and memory limits. The released subset does not rule out a program running forever. We read the primary documentation but did not run the proof checker.
What the proof establishes
A fuzz test feeds inputs into a selected part of a library and looks for failures. In Anthropic's experiment, the library and test become a compiled executable. Claude writes a proof about that executable, and the Rocq proof checker checks it against a formal specification. The researchers say Claude patched bugs during the process, then proved claims about the resulting code.
The public repository at commit 98e995d lists proofs for 60 entry points in 25 libraries. That's a subset, separate from the larger research result. Its documentation describes agreement between ordinary and sanitizer-instrumented builds: within the stated conditions, neither reaches an error, and both have the same observable behavior.
For a maintainer, the first question is which compiled artifact the guarantee covers. Theorem's scope documentation ties each statement to exact binary bytes identified by a SHA-256 hash. Another compiler, different flags or another processor architecture falls outside that claim. A proof for the supplied binary doesn't certify the version you built for production.
No crash doesn't establish termination
The release documentation distinguishes error freedom from a guarantee that execution ends. None of its released proofs establishes the latter. That distinction matters for a parser exposed to untrusted input: a service can become unavailable if a request never finishes, even without a memory error.
Coverage also depends on what the test checks. Theorem's documentation excludes memory leaks and reads of uninitialized memory from the checks supplied by this toolchain. It limits input files to less than 64 MiB. A maintainer still needs to inspect the test's properties and the process model before deciding which failure modes have been addressed.
What maintainers can request
Theorem is offering OSS Verify free to qualifying open-source projects. Only core maintainers can enroll a project. Eligibility considers maintenance activity and use, with priority for widely used infrastructure. Enrollment requires build files and static RISC-V binaries, so an existing OSS-Fuzz setup may need porting.
The program's terms also leave review work with maintainers. Findings and patches come from AI models, and Theorem doesn't promise human review before sending them. It says it reports bugs privately and sets no disclosure deadline. Treat a suggested patch as code to review, including whether it preserves the behavior callers need.
Watch for independent rechecks of the published artifacts and proofs covering more deployment configurations. For now, the useful evidence is a statement attached to a particular binary. A project adopting it needs to preserve that connection when it builds and ships its software.