Anthropic and Theorem used Claude to prove bounded no-crash properties for 239 fuzz-test entry points across 123 libraries in Google’s OSS-Fuzz project. The guarantees apply to specified inputs and a modeled computing environment.
The proofs address whether compiled programs would exit normally without a crash, memory-safety error or failed assertion for any input under 64 MB within the model. Anthropic described the work in an Oct. 22 research post and said it took a few weeks.
Anthropic expressed the expected outcomes of existing fuzz tests as properties of compiled RISC-V programs. Claude generated formal proof code, which Rocq’s kernel checked against those properties.
The analysis modeled each program as a single-threaded static binary, with Linux behavior and a fixed memory budget on RISC-V. The guarantee covers the specified entry points and conditions; it does not establish that the libraries have no other bugs.
Anthropic said Claude also patched bugs found during the work. The company is publishing selected materials, including proofs for targets that needed no code changes, specifications for targets it could not prove, and previously unpublished trusted components. Anthropic invited independent verification.
