Anthropic Says Claude Proved Security Properties in More Than 100 Open-Source Libraries

Anthropic has announced a major development in AI-assisted cybersecurity, revealing that its Claude model has successfully produced mathematical proofs of specific security properties in more than 100 real-world open-source software libraries. Published on October 22, 2026, the research was conducted by Anthropic’s Frontier Red Team in collaboration with Theorem, a company that provided formal models of computer processors and operating-system behaviour. According to Anthropic, the project demonstrated that AI can help automate parts of formal software verification, a process traditionally requiring substantial expertise and extensive manual effort. The researchers applied the technique to 123 open-source libraries and verified 239 program entry points, marking a significant experiment in using AI to establish precise guarantees about software behaviour.

The research focused on formal verification, a method of using mathematical reasoning to establish whether software satisfies a clearly defined set of requirements. Instead of merely testing a programme with selected inputs, formal verification attempts to prove that specified properties hold across every input covered by the model. Anthropic used Claude to generate proofs for compiled software running on a simulated RISC-V processor under a model of Linux. The proofs established that the selected programme entry points would complete without certain crashes, memory-safety errors or failed assertions for inputs smaller than 64 megabytes, subject to the project’s stated assumptions. Anthropic reported that the resulting proofs comprised approximately 180 million lines of Rocq proof code, illustrating the enormous amount of verification work that AI can help produce.

One of the most important aspects of the experiment is that the AI-generated proofs were checked by the Rocq proof-checking system. This means the security claims were not accepted simply because Claude produced a convincing explanation; the proofs had to satisfy a formal mathematical specification that the checker could validate. Anthropic says the process also uncovered software defects that had remained undetected despite extensive testing. In one investigation involving a widely used PDF reader, the team reportedly discovered as many security bugs in a week as are typically reported in a year. The company also described finding a previously known vulnerability in the libexpat library and identifying additional problems while examining other widely used software components. These results suggest that AI-assisted verification could help developers identify defects that conventional testing methods may miss.

However, Anthropic has emphasised that formal verification does not mean an entire software library is completely free of bugs. The guarantees apply only to the specific properties defined in the proof and depend on the accuracy of the models used to represent the processor, operating system and programme behaviour. The initial large-scale experiment also relied on assumptions involving single-threaded, statically compiled programmes, a fixed memory budget, Linux and a RISC-V processor. Software running under different architectures or operating conditions may require additional verification work. Furthermore, producing these proofs can consume hundreds of millions of tokens, creating substantial computational costs. Anthropic says it is releasing a subset of its proofs and supporting models so independent researchers can examine and reuse the work.

The announcement highlights a growing shift in cybersecurity from discovering vulnerabilities after software has been developed towards proving that particular classes of defects cannot occur under defined conditions. AI systems are increasingly capable of analysing large codebases, identifying weaknesses and assisting with repairs, but those same capabilities can also help attackers discover exploitable flaws. Anthropic believes formal verification could become a more practical part of secure software development as AI models improve. Its collaboration with Theorem provides an early demonstration of that possibility, although independent evaluation will be necessary to establish how reliably the approach works across different software projects and computing environments. If the technique becomes cheaper and supports more processor architectures, it could help developers strengthen the security of the open-source libraries used throughout websites, applications, financial systems and digital infrastructure.