Anthropic Uses Claude to Formally Verify 123 Open-Source Libraries, Condensing Years of Work into Weeks

Anthropic announced its Claude models verified security properties across 123 open-source libraries at the assembly level. The verification project, conducted by the Frontier Red Team and Theorem Labs, took a few weeks to complete. Formal verification produces a mathematical proof that code satisfies a specific property, a method that has historically required years of expert effort per project. The verification follows a previous Anthropic attack-surface analysis on 25 open-source projects, which scanned over 5 million lines of code and flagged 493 issues, including 94 cases with disabled security controls. Researchers noted that while formal verification proves code meets a stated specification, any gap in that specification remains a vulnerability. "We need ways to prove that code is free of bugs." — Anthropic Frontier Red Team