TL;DR: Claude wrote proofs that rule out specified crashes in selected test programs; a separate checker checks the logic.

Anthropic and Theorem report doing this for 239 test entry points across 123 open-source libraries. Some tests encode useful properties, such as getting the original data back after compressing and decompressing it.

The October 22 release includes a subset of the proofs. The guarantees apply to selected compiled programs under a modeled RISC-V/Linux environment, input-size limits and memory budgets. They do not certify an entire library or its usual desktop/server build.

Public proof statements and limits