Anthropic uses Claude to prove security properties in 123 open-source libraries
Anthropic has used its Claude models to verify security properties across 123 open-source libraries in just a few weeks, a process that traditionally took years of specialist effort.
The research comes from Anthropic's Frontier Red Team, working with Theorem Labs. The team includes security researchers Keane Lucas, Chris Rohlf, Nicholas Carlini and Nickolai Zeldovich, among others. Their work addresses the growing concern that most software contains bugs that AI can now locate and exploit with relative ease.
From testing to proving
The researchers argue that conventional cyber defenses are no longer sufficient. "We need ways to prove that code is free of bugs," they state. Traditional security testing finds problems but doesn't guarantee their absence, while formal verification provides mathematical proof that code meets specific security properties.
We need ways to prove that code is free of bugs.
Assembly level breakthrough
Anthropic claims Claude can now verify security properties of large-scale production software at the assembly level—the low-level instructions a processor actually executes. This means proving what the machine will run, not just what programmers intended. The team previously analyzed 25 open-source projects covering over 5 million lines of code in C, C++, Java, PHP and Python, flagging 493 issues including 94 cases where security controls had been disabled.
Broader implications
While much AI security research focuses on offensive capabilities, Anthropic's approach shifts the defensive paradigm from "we tested it" to "we proved it." However, a proof is only as good as its specification, and gaps remain. The collaboration with Theorem Labs suggests Anthropic views this as both a research and tooling challenge. Whether this becomes standard practice will depend on how easily others can reproduce the results.
Related
