Anthropic says Claude has produced security proofs for 239 test entry points across 123 open-source libraries. Its October 22 research with Theorem covers particular compiled programs under stated conditions, rather than certifying entire libraries as bug-free.

Some of those proofs are now public, giving developers a way to inspect the guarantees. The released repository currently covers 60 entry points in 25 libraries, including parts of OpenSSL, simdjson and zstd.

A proof covers more inputs than a test run

Fuzz testing feeds generated inputs into software to find failures. Formal verification instead establishes that a stated rule holds for every input within its assumptions. Claude writes the proof, and the Rocq proof checker checks the reasoning.

Theorem’s description of the process starts with existing fuzz tests and their compiled machine instructions.…