Anthropic’s Frontier Red Team, in collaboration with Theorem Labs, has utilized Claude models to perform formal verification on 123 open-source libraries. The process, which typically requires years of expert labor per project, was completed in a few weeks.
The verification process operates at the assembly level, analyzing the low-level instructions executed by processors. This approach provides mathematical proof that code adheres to specific security properties, moving beyond traditional testing methods that only identify potential issues.
This initiative is part of Anthropic’s broader strategy for defensive open-source security, which includes the OSS Scanner project. Previously, the team conducted an attack-surface analysis on 25 open-source projects, covering over 5 million lines of code written in C, C++, Java, PHP, and Python.
The prior analysis identified 493 issues, including critical vulnerabilities and 94 instances where security controls were disabled. The current research aims to shift security standards from simple testing to formal verification, addressing the historical cost and time barriers associated with such proofs.
