Anthropic says Claude and verification company Theorem produced proofs covering 239 fuzz-test entry points in 123 open-source libraries. The October 22 report describes a way to prove that particular tests cannot uncover a crash within defined input and execution limits, rather than relying only on trying more sample inputs.
The public repository currently lists proofs for 60 entry points in 25 libraries. Anthropic says it is releasing completed proofs for tests that did not need patches, together with supporting components and specifications for other tests. The published subset should not be confused with the larger experiment.
What the Proofs Cover
A fuzz test feeds generated inputs into a specific part of a program to look for failures. Here, the team compiled tests into RISC-V machine code and used Claude to write mathematical proofs that Rocq, a proof assistant, checks against a formal specification.
The experiment covers inputs of roughly 64 MB and assumes a single-threaded static binary, a fixed memory budget and a modeled Linux environment. The public project specifies 64 MiB input bounds; each theorem defines the precise conditions it covers.
That distinction matters for maintainers: a proof about one compiled entry point does not certify the whole library, another processor architecture or every possible operating-system interaction.
The repository’s documentation also says the release does not rule out runs that never finish. Errors outside the runtime error checker’s tests, including some wrong results and memory leaks, can remain. Its Linux process model is incomplete and makes assumptions, so a checked proof still depends on the specification and trusted model matching the real program.
A Free Route for Qualifying Maintainers
Theorem is offering its OSS Verify program free to qualifying open-source projects. Only core maintainers can enroll a project. The program considers maintenance, adoption, an OSI-approved license and the project’s security role, prioritizing widely used infrastructure.
Enrollment uses a pull request with project metadata and build files. Existing OSS-Fuzz configurations can be a starting point, but the program requires static RISC-V binaries, so builds may need porting. Proofs can take several days; this is not an instant scan of any uploaded application.
Theorem says it privately reports bugs found during verification. Findings and patches are generated by AI, and the program does not promise human review before delivery. Maintainers still need to assess proposed changes and the exact guarantees attached to their builds.