Anthropic Says Claude Formally Verified 123 OSS Libraries in Rocq, Caught Bugs Missed by Trillions of Tests
Summary
Anthropic's Frontier Red Team published research on Oct 22 showing Claude generated roughly 180M lines of Rocq formally verifying security properties at the RISC-V assembly level for 239 fuzz-test entry points across 123 open-source libraries, in collaboration with Theorem. The run uncovered hundreds of bugs, including flaws that had escaped trillions of automated test runs. Opus 5.5 proved half of 36 benchmark tasks with 40% fewer tokens than Opus 5, and shared-workspace agents cut token usage 17% versus solo runs.
Shared on Bluesky by 3 AI experts
-
John David Pressman @jdp.extropian.net
It begins. www.anthropic.com/research/for...
View on Bluesky → -
Formal methods becoming orders of magnitude easier to do is a huge deal for software security.
View on Bluesky →
Originally reported by anthropic.com
Read the original article →Original headline: Anthropic Says Claude Formally Verified 123 OSS Libraries in Rocq, Caught Bugs Missed by Trillions of Tests