Anthropic and Theorem report AI-written proofs for open-source fuzz targets

Anthropic published research with Theorem on October 22 reporting that Claude produced formal security proofs for 239 fuzz-testing entry points across 123 open-source libraries. The work turns existing tests into mathematical statements about compiled programs, then uses an independent proof checker to validate the generated arguments. During the process, the model also found and patched bugs that prevented those statements from holding.

The guarantees apply within a defined execution environment: static, single-threaded RISC-V binaries linked against musl, running in a model of Linux processes with fixed memory budgets. The technical appendix specifies inputs smaller than 64 MiB, and Theorem's driver documentation says files at or above that size are refused. The theorem's premises also determine which operating-system responses, memory layouts and resource conditions are covered.

The pipeline works with a library's existing fuzz harness, whose assertions can encode properties such as successful compression and decompression. It compares ordinary binaries with versions containing sanitizer checks and reasons about their observable behavior. In the appendix, crashes include faults, aborts and behavior absent from the process model. Claude constructs the arguments in Rocq, while Rocq's kernel checks whether they establish the required statements.

The trust boundary remains concentrated in the formal machine and process models, the exact theorem statements and the checker itself, including the supporting tools and environment needed to check each binary. Coverage follows the code reached through the chosen entry point and the checks present in the binary. Properties outside those checks, and differences between the model and deployed hardware or operating systems, remain relevant when applying a result to production software.

Patching introduced a separate challenge: an agent could make a no-crash claim easy by removing meaningful program behavior. Anthropic says the experiment penalized every patch and awarded extra credit for proving which inputs a change affected and how limited that set was. Researchers also recorded and audited patches for these shortcuts. After a modification, the specification was regenerated and the model attempted to prove the statement about the revised program.

The public material is a subset of the research results. At the time of review, Theorem's proof repository listed 60 entry points in 25 libraries, with proofs checked using Rocq 9.2.0. It pins the compiled binaries and records the associated statements and assumptions. The published release contains agreement proofs, which compare behavior and exclude specified errors; those proofs can still permit a run that never ends. Termination requires a separate theorem.

The expert discussion in Anthropic's appendix describes proofs that are much more verbose than a human specialist would usually write. Agents repeatedly spelled out register contents, memory addresses and execution branches, while also developing some familiar abstractions. The analysis treats better modular structure as an open question for extending this approach to more complex programs. It separates a proof's mathematical validity from the efficiency and organization of producing it.

Theorem is also offering its OSS Verify pipeline without charge to qualifying open-source projects. Eligibility is reviewed individually, considering maintenance, usage, licensing and the project's position on security boundaries or beneath other software. The program prioritizes widely used infrastructure and reports discovered bugs privately to maintainers. Its documentation says proofs can take days to produce and may be updated after completion, tying each result to specific program builds.