Claude Takes Software Security Beyond Bug Detection

By Suad Seferi · 26 October 2026 at 09:19

Anthropic has demonstrated that its Claude AI models can generate mathematical proofs of specific software security properties, offering a new approach to detecting vulnerabilities and verifying that code behaves as intended. In research published on October 22, Anthropic reported that Claude, working with software verification company Theorem, produced machine-checked proofs covering 239 test entry points across 123 open-source libraries. The work goes beyond conventional AI-assisted vulnerability detection. Instead of searching for bugs and reporting potential weaknesses, Claude generated mathematical proofs showing that certain programs cannot crash under precisely defined conditions. The findings suggest that a security technique historically reserved for highly specialised software projects could become more accessible to developers. From finding vulnerabilities to proving their absence Traditional software security testing involves running programs, examining their behaviour and attempting to identify weaknesses. Automated tools can execute millions or billions of tests, but they cannot guarantee that every possible input or execution path has been examined. Formal verification takes a different approach. Rather than testing a program against selected inputs, developers define mathematical rules describing how the software should behave. A formal proof then establishes whether those rules hold for every possible execution within the specified conditions. The difficulty has always been the work required to produce these proofs. They can be considerably larger and more complicated than the software being examined. Anthropic's research explored whether AI could handle much of that complexity. Working with Theorem, researchers used Claude to generate proofs for software included in Google's OSS-Fuzz project, which continuously tests open-source libraries for security problems. The researchers compiled the software into RISC-V machine instructions and used mathematical models of the processor and Linux operating system to establish the conditions that needed to be verified. Claude then generated proofs using Rocq, a formal proof system that independently checks whether mathematical arguments are valid. This distinction matters. The security result does not depend solely on Claude claiming that the software is correct. A separate mathematical proof checker evaluates the generated evidence. Across the experiment, Claude produced approximately 180 million lines of proof code. According to Anthropic, the verified test entry points cannot experience the specified crashes or memory-safety failures for inputs smaller than 64 MB, provided the assumptions used in the verification model hold. Claude uncovered bugs that traditional testing had missed The process also revealed vulnerabilities. Anthropic reported discovering hundreds of bugs while attempting to establish the proofs. Some had remained undetected despite extensive automated testing. One example involved a decompression library. Claude identified a counter underflow that could cause an out-of-bounds memory write, but only when the program processed an input of approximately 20 MB with a particularly unusual arrangement. Such conditions can be difficult for conventional fuzzing tools to discover because they typically concentrate on smaller inputs and previously observed execution paths. The researchers also described memory-access problems in image-processing software and the rediscovery of a vulnerability in the widely used libexpat XML parsing library, identified as CVE-2026-56132. During the experiments, Claude was allowed to modify code when it encountered problems that prevented a proof from being completed. The verification process then continued against the modified software. That does not mean every discovered issue has already been corrected in the upstream open-source projects. Anthropic has withheld some proofs that might disclose unpatched vulnerabilities. The findings nevertheless demonstrate an additional use for AI in cybersecurity: attempting to establish a proof can expose weaknesses that existing testing methods have failed to identify. Does this mean the software is completely secure? No, and Anthropic explicitly acknowledges this limitation. The research does not establish that all 123 libraries are free from vulnerabilities. The proofs cover particular test entry points, specific security properties and a defined execution environment. The primary experiments involved single-threaded, statically linked RISC-V programs running under a mathematical model of Linux with a fixed memory budget. Most production software operates in more complicated environments, commonly using x86 or ARM processors, additional dependencies and different operating-system configurations. A successful proof under one set of assumptions does not automatically extend to those environments. There is another important limitation: formal verification can establish that software satisfies a specification, but it cannot guarantee that the specification describes everything the software should do. A program might satisfy its mathematical requirements while still containing vulnerabilities outside the properties being checked. The reliability of the underlying processor and operating-system models, as well as the proof checker itself, also remains essential. For these reasons, formal verification should be considered an additional security mechanism rather than a replacement for code reviews, penetration testing, vulnerability management or existing secure-development practices. What changes for software developers? The most significant implication concerns how software security could eventually become part of routine development. Today, developers commonly rely on automated tests, static analysis, dependency scanning and security reviews. Formal verification has generally remained outside ordinary development workflows because of its cost and comple…