Anthropic deployed Claude across 25 open-source projects to investigate attack surface reduction: restricting access to code that a particular deployment does not need to expose. The models identified 493 issues after examining more than five million lines of code. Among them was a 21-year-old configuration conflict in which an option intended to defer certificate authentication instead disabled it entirely, allowing a server configured for trusted clients to accept anyone.
In OpenSSH 10.4, Claude traced approximately 4,500 lines of post-quantum signature code that unauthenticated clients could reach even when administrators had excluded the algorithm. Representing about 16% of the daemon’s pre-authentication code, the finding prompted fixes in releases 10.5 and 10.6. Anthropic emphasises that reducing unnecessary reachability limits the potential severity of unknown vulnerabilities rather than eliminating them.
In a separate collaboration with software verification firm Theorem, Anthropic applied formal verification to 123 software libraries. Claude translated existing fuzz tests—automated checks using unusual inputs—into mathematical specifications, then generated proofs that 239 entry points would not crash under defined conditions. Roughly 180 million lines of proof code were checked by the independent tool Rocq. The process uncovered hundreds of bugs, some of which had survived years of testing; Claude also patched flaws and generated fresh proofs. One decompression defect required roughly 20 MB of unusually arranged input to trigger an out-of-bounds write. Nevertheless, the guarantees remain conditional: the work covers single-threaded, statically linked RISC-V programs within a modelled Linux environment. Proofs establish only the properties specified, and their validity depends on assumptions about the underlying system. Formal verification therefore does not certify software as universally bug-free.
