Anthropic Uses Claude to Verify Security in 123 Software Libraries

Anthropic and software verification company Theorem have used Claude to prove security properties in 123 real-world open-source software libraries, demonstrating how large language models can expand formal verification beyond highly specialized projects. The collaboration focused on executable code compiled for the RISC-V architecture and uncovered bugs that had escaped detection despite extensive testing.

According to Anthropic, the project represents the first large-scale effort to apply AI-driven formal verification to production software at the assembly-code level. The company published a subset of the resulting proofs, together with the RISC-V and operating system semantics needed to check and reuse them.

Formal verification uses mathematical reasoning to establish whether software satisfies specified properties. Unlike conventional testing, which examines selected executions, this approach attempts to prove that the defined requirements hold across all behaviors covered by the model and its assumptions.

Anthropic said the process historically required substantial specialist effort. Implementing the seL4 operating system kernel took two person-years, while formally verifying it required 20 person-years. As a result, the technique has largely been reserved for safety-critical applications, including aircraft avionics software.

For the new project, Claude worked across 123 open-source libraries to establish properties such as whether programs could finish execution without crashing under specified conditions. The proofs covered inputs smaller than 64 megabytes and modeled Linux operating system responses and memory layouts.

Anthropic said the guarantees apply under defined assumptions: programs must run as single-threaded, statically linked binaries with a fixed memory budget on a RISC-V processor using Linux. Within that model, the proofs establish that the programs exit normally without triggering memory-safety errors or failing assertions.

The results do not establish that the libraries are free of every possible defect. Instead, they demonstrate that formal methods can verify specific security properties across a wider range of real-world software than was previously practical.

Anthropic also reported that Claude discovered long-standing bugs during the verification process. Some had remained undetected despite trillions of test runs, highlighting the difference between testing individual executions and proving specified properties across a modeled set of possible executions.

Another challenge is defining correctness. Some programs have clear specifications, such as a PNG decoder that must translate a sequence of bytes into an image according to a defined standard. For applications such as text editors and web browsers, however, describing all intended behavior precisely is more difficult.

To address this problem, the researchers converted existing compilable test suites into specifications by encoding the requirement that every test must pass. They combined those specifications with a general model of how RISC-V-compiled binaries execute on Linux, allowing Claude to reason about program behavior at the assembly-instruction level.

Anthropic said the team also explored other applications of formal verification, including assessing the security of the zlib compression algorithm, proving behavioral equivalence for a Python interpreter written in Rust, and identifying persistent defects in critical software.

Theorem is making the verification pipeline available for other open-source projects and publishing a Claude skill intended to help developers begin verifying their own code. Anthropic said improvements in model capabilities and the reuse or adaptation of existing proofs could further reduce the cost of applying formal verification across software projects.