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. A test can express a useful guarantee by failing whenever that rule is broken, so proving it cannot fail also establishes the rule.
Anthropic says the effort uncovered bugs while Claude was trying to complete proofs. The model patched affected code before proving the revised version; proofs that could expose unpatched vulnerabilities are being withheld.
Your software build still needs its own evidence
The published proofs apply to specific static binaries built for the RISC-V processor architecture and a model of Linux. They don’t establish the same result for an x86 or Arm build used by your hosting provider.
The repository also excludes several wider promises: checking one entry point does not cover an entire library, and errors outside the specified checks can remain. None of its released proofs rules out a program running forever.
For a development team, the useful question is which binary and behavior a proof covers. A library name alone cannot answer that. Changing the build or calling the library through another path can put your application outside the demonstrated guarantee.
The cost depends on how much proof work can be reused
Producing the proofs can consume hundreds of millions of tokens. In a separate 36-task comparison, Anthropic says Opus 5.5 proved half the tasks using roughly 40% fewer tokens than Opus 5.
Its experiments also let agents reuse earlier proof files. Much of the shared work concerns components that different programs have in common, reducing the amount of reasoning that must be written again for another library.
Maintainers can apply to Theorem’s free program for qualifying open-source projects. Its submission process requires a project description, build environment and build script, so this is work for the software’s maintainers rather than a security setting a site owner can switch on.
Source: Anthropic
Start the conversation by posting the first comment