The work targets compiled RISC-V binaries and turns existing fuzz tests into specifications that the corresponding program does not crash.
The reported proofs cover inputs below 64 MB and show normal exits without memory-safety errors or failed assertions for modeled Linux responses and memory layouts. Anthropic says the proof corpus totals roughly 180 million lines, and that the process found bugs that had survived extensive fuzzing. It is publishing a subset of the proofs plus RISC-V and OS semantics.
Theorem is offering the pipeline for other open-source projects and publishing a Claude skill intended to help developers begin verification. The source does not establish that the libraries are free of all bugs or vulnerabilities: the claims are limited to the stated properties, inputs, architecture, operating-system model, and assumptions, including single-threaded static binaries and a fixed memory budget.