Anthropic uses Claude to prove security properties in 123 open-source libraries

Anthropic says its Claude models have verified security properties across 123 open-source libraries. The work took a few weeks. That timeline matters because formal verification, the method behind it, has historically demanded years of specialist effort per project. Compressing that into weeks changes who can actually afford mathematical proof that their code behaves. From finding bugs to proving their absence The research comes from Anthropic’s Frontier Red Team, working with a firm called Theorem Labs. The author list is long and includes security researchers Keane Lucas, Chris Rohlf, Nicholas Carlini and Nickolai Zeldovich, among others. The team’s framing is blunt. Most software is full of bugs, and AI can now locate and exploit those bugs with relative ease. Their conclusion follows from that premise. The researchers argue that conventional cyber defenses no longer cut it. “We need ways to prove that code is free of bugs.” Traditional security testing produces findings but not guarantees. Formal verification produces a mathematical proof that code satisfies a specific property rather than simply failing to find a problem. The catch has always been cost. According to the Anthro...