Anthropic deployed Claude across 25 widely used open-source projects to investigate attack surface reduction: limiting access to code that a particular deployment does not need to expose. After examining more than five million lines of code, the models flagged 493 issues. These included a 21-year-old configuration conflict in which a setting intended to delay certificate checks disabled them instead, allowing untrusted clients to connect. In OpenSSH 10.4, Claude identified roughly 4,500 lines of post-quantum signature code accessible before authentication, even when administrators had excluded the algorithm. Maintainers issued fixes in releases 10.5 and 10.6. The approach does not eliminate unknown vulnerabilities; it reduces their accessibility and potential severity.
In a separate collaboration with software verification firm Theorem, Anthropic used Claude to formally verify security properties across 123 software libraries. The model converted existing fuzz tests, which try unusual inputs, into mathematical specifications and generated proofs that 239 program entry points would not crash under defined conditions. Working with RISC-V machine instructions, Claude produced roughly 180 million lines of proof code, which a separate tool, Rocq, checked. The process uncovered hundreds of bugs, including defects that had escaped years of automated testing. Claude also patched problems and generated fresh proofs for the revised code.
These guarantees remain narrowly scoped. The verification covered single-threaded, statically linked RISC-V programs in a modeled Linux environment, rather than every configuration used in practice. Proofs establish only the properties their specifications describe, and their reliability depends on assumptions accurately representing processors and operating systems. Anthropic expects improved models and reusable proofs to lower verification costs.
