Anthropic reports that Claude generated approximately 180 million lines of machine-checkable mathematical proofs covering 239 test entry points across 123 open-source software libraries. Published on October 22, the research, conducted with verification company Theorem, suggests that AI could automate part of the labor-intensive process of proving that software avoids specific classes of failures.
The researchers also reported discovering hundreds of bugs, including memory errors that conventional testing had missed. The proofs establish guarantees only for specified behaviors and operating conditions, so developers must assess whether those conditions match their deployed software.
How Claude turns software tests into mathematical proofs
Fuzz testing checks for failures by running software with automatically generated or modified inputs. Formal verification uses mathematical proofs to establish that a specified property holds for every input covered by the proof’s assumptions. Fuzz testing can reveal a failure in an individual test run, while verification can establish that a specific failure cannot occur within those conditions.
Producing these proofs has historically required considerable specialist work. Anthropic cites the seL4 operating system kernel, which took approximately two person-years to develop and about 20 person-years to verify. Automating proof generation could help projects adopt verification even when they cannot fund a dedicated team of specialists.
Researchers converted existing OSS-Fuzz tests into specifications that state which properties the software must satisfy. They then compiled the software into instructions for RISC-V processors and asked Claude to produce mathematical proofs about those compiled programs. Rocq, a proof-checking tool, checked whether Claude’s arguments satisfied the specifications.
If the process revealed a bug, Claude could patch the software and retry the proof against an updated specification. Rocq checked the revised argument, reducing the need for researchers to inspect the generated proofs line by line.
Anthropic’s technical appendix also explains how researchers compared test builds containing error-detection checks with ordinary builds. These comparisons establish whether guarantees proved for the test versions also apply to the corresponding software users run.
How verification uncovered bugs that fuzz testing missed
Anthropic reported bugs that required inputs conventional fuzz testing was unlikely to generate. A decompression error needed an input of approximately 20 MB with a particular arrangement, while an image-decoding defect required a 64 MB input and more than 2 GB of memory. Claude also rediscovered a known libexpat vulnerability triggered by deeply nested input.
Fuzzers can miss these failures when file sizes exceed their testing limits or their input-generation methods rarely produce the necessary combinations. Attempts to prove that a property holds across the specified input range can expose failures that individual test runs never reach.
An incomplete proof does not necessarily indicate a software bug; Claude may simply be unable to construct the required argument. Researchers need a counterexample, such as an input that violates the property under examination, to demonstrate a defect.
What Anthropic’s software proofs do and do not guarantee
The public proof repository contains proofs for 60 entry points across 25 libraries, a subset of the 239 entry points and 123 libraries in Anthropic’s experiment. Its documentation limits the guarantees to particular compiled programs and the code those entry points can reach. Defects such as incorrect results or certain memory leaks remain outside that coverage.
The main experiment covered RISC-V programs that run on a single execution thread with their required libraries bundled into the executable. The proofs assume modeled Linux behavior and fixed memory limits, with inputs capped at approximately 64 MB. Those guarantees do not automatically transfer to x86 or ARM builds, where processor behavior or runtime configurations may differ. Anthropic also reports preliminary x86 verification, but applying the approach to other production environments requires further evidence.
The published proofs do not establish that a program will finish running. Software could meet the verified safety conditions yet continue indefinitely, so a successful proof does not guarantee completion of its intended task.
Rocq checks whether a proof establishes the property stated in a specification; it cannot judge whether the specification covers the developer’s security requirements. A valid proof may therefore leave critical failures unaddressed. Developers still need to assess what the specification covers and whether its assumptions match their software.
AI reduced verification work, but total costs remain unclear
Anthropic reports that Opus 5.5 completed half of a 36-task verification benchmark with approximately 40% fewer tokens than Opus 5. In a separate experiment, agents used 17% fewer tokens when they could reuse one another’s proofs. These findings show reduced token consumption for the tested tasks, but the announcement does not establish the total cost of verifying a software library.
Costs would also include specialist review and the computing resources needed to generate and check proofs. Maintenance adds another expense: changes to a program or its dependencies may require teams to update the proofs and repeat verification.
Theorem’s OSS Verify program provides free verification for qualifying open-source projects and says proofs can take several days to generate. Accepted maintainers pay no direct fee, but the offer does not reveal the cost of producing or maintaining proofs at commercial scale.
How verified open-source libraries could benefit other applications
Proofs for widely used open-source libraries could give multiple applications reusable evidence of specific security properties. The potential reach is apparent in The Neuron’s PHP2Shell reporting, which showed how vulnerabilities in shared software can affect many applications.
Developers could add automated proof checks to their build processes if their library versions and configurations meet the verified assumptions. They would still need to check whether the rest of the application uses those libraries correctly.
Wider adoption depends on independent validation under production conditions and evidence that teams can afford to update proofs as software changes. AI could reduce the effort of generating proofs, but developers must establish that the verified properties address their applications’ security requirements.
