Claude formally proves the security of 123 open source libraries and finds hundreds of bugs

In a few weeks, Anthropic's Frontier Red Team has sent Claude about 180 million lines of evidence in Rocq, a formal audit work so far reserved for small programs.

Anthropic claims that large models finally make formal verification workable on a large scale. His Frontier Red Team team, associated with Theorem, asked Claude to mathematically demonstrate security properties at 239 entry points in 123 open source libraries, including cpp-httplib, libcups, FreeRDP, libzmq, implementations of zlib and other projects followed by Google's OSS-Fuz. The set represents about 180 million lines of evidence in the Rocq assistant (ex-Coq), around 600,000 lines for a median binary of 18,000 RISC-V instructions.

Bugs found on the way

It was by failing to prove certain specifications that Claude discovered hundreds of defects: a counter that goes below zero and causes an out-of-limit write with entries of about 20 MB, an out-of-limit read in an image decoder requiring 64 MB of input and 2 GB of memory, or the CVE-2026-56132 fault in libexpat, triggered by deeply intertwined data. Logical bugs, such as unapplied file loading restrictions, are also included in the list.

Guarantees remain limited: mono-thread static binary, RISC-V architecture, Linux, fixed memory budget and less than 64 MB entries. Anthropic publishes complete evidence of tests that did not require corrective action, unproven specifications and its RISC-V semantics and system; Theorem proposes to extend the approach to other projects and broadcasts a dedicated Claude skill. According to the ticket, Opus 5.5 solves half of 36 verification tasks with about 40% less tokens than Opus 5.