Software verification reaches open source libraries as language models construct mathematical proofs

Automated reasoning systems can now generate hundreds of millions of lines of mathematical proof to verify that production software will not crash, finding subtle security flaws that bypassed trillions of test runs.

Computers run the modern economy on code that is fundamentally presumed to contain latent errors. Even foundational components that undergo decades of relentless scrutiny continue to conceal serious flaws. The Linux kernel, an operating system foundation deployed on billions of devices globally, recently disclosed more than 1,000 vulnerabilities despite receiving constant attention from human engineers and automated test suites.¹² In conventional engineering, testing functions by running a program repeatedly against sample data, observing whether the system behaves as intended, and repairing errors that reveal themselves along the way. Yet sampling inputs can never examine every path a computer program might take. A single uninspected combination of variables can trigger memory corruption, disable security boundaries, or grant an attacker control of a machine.

Bridging that gap requires moving past empirical testing into formal verification, a discipline that models computer code as a system of mathematical equations and calculates whether an unhandled error state is impossible. Historically, constructing these proofs demanded years of specialized mathematical labor, confining the method to aviation control systems or microkernels. A research effort by Keane Lucas and colleagues at Anthropic and the verification firm Theorem has demonstrated that automated reasoning systems can now generate these mathematical proofs across large collections of real-world software.³ Using the model Claude, the researchers produced machine-checked proofs covering 239 entry points across 123 open-source libraries from Google's OSS-Fuzz initiative, verifying that the programs will exit normally without memory-safety crashes for any input smaller than 64 megabytes under modeled system conditions.¹⁴

The resulting evidence demonstrates that machine learning models can construct valid formal proofs for production software directly at the assembly code level.¹³ Over the course of a few weeks of execution, the system generated roughly 180 million lines of proof code accepted by the Rocq proof checker, with individual proofs running to approximately 600,000 lines to verify binaries with a median length of 18,000 instructions in the RISC-V computer architecture.¹⁴ While working through the proofs, the system also surfaced long-standing bugs that had eluded trillions of automated test executions, including memory errors triggered only by rare file formats or unusually large files.¹

Why does software testing fail to catch critical vulnerabilities?

Conventional software testing fails to guarantee security because it operates by incomplete exploration rather than universal proof. In a typical fuzz test, a programmer writes an entry point that accepts variable inputs, while an automated test generator feeds the program millions or trillions of mutated data sequences in an effort to force an unexpected crash. For an error to appear, a specific sequence of bytes must enter the program, navigate past every intermediate conditional branch, trigger an arithmetic miscalculation or buffer overflow, and cause an observable system fault. If a bug requires an input that is 20 megabytes long with a specific internal structure, a test generator that operates primarily on files under one megabyte will never encounter the failure path.¹³

Formal verification alters this dynamic by establishing a comprehensive logical argument over every permitted input within a defined scope. To verify a software component, engineers first draft a formal specification, which is a rigid mathematical description defining acceptable system behavior. The specification establishes what must remain true during execution, such as requiring that memory allocations never exceed bounded buffers or that a decoder always produces valid output. A proof assistant then evaluates a logical proof demonstrating that the compiled machine instructions can never violate the specification, regardless of which bytes enter the program. If an execution path exists where an invariant breaks, the proof attempt fails, directing attention directly toward the flawed logic.

The historical barrier to this mathematical approach has been the sheer human effort required to author the proofs. In conventional computer science projects, formal proofs often run several times larger than the executable code they verify. When researchers formally verified the seL4 operating system kernel, writing the underlying software required two person-years of effort, while verifying the mathematical correctness proofs required 20 person-years of labor.¹³ Because human mathematicians had to author every lemma and invariant by hand, formal verification remained economically out of reach for general open-source software libraries.

How can artificial intelligence prove that code will never crash?

Automated language models solve the labor bottleneck by generating the millions of lines of intermediate proof steps required to verify machine instructions. Rather than constructing abstract source specifications from scratch, Lucas and colleagues converted existing fuzz tests from the OSS-Fuzz repository into formal mathematical targets. In OSS-Fuzz, developers construct entry harnesses that instrument C and C++ programs with AddressSanitizer, an automated compiler tool that forces an immediate crash whenever an application reads or writes memory outside allocated regions.⁴ The researchers translated the core assumption of these harnesses into a mathematical specification stating that the program must always complete execution without triggering AddressSanitizer crashes or failing internal assertions for any input below 64 megabytes.³

The verification pipeline operates on executable binaries compiled to the RISC-V instruction set architecture, linked against the musl standard C library.¹⁴ Theorem provided formal mathematical models representing how RISC-V processor instructions update register states and how a Linux operating system kernel handles system calls, process memory layouts, and process lifecycles.¹³ Working from these underlying models, Claude generated formal proofs in Rocq, a specialized interactive theorem proving language formerly known as Coq.³ The external Rocq proof kernel evaluates each proof step mechanically, ensuring that every assertion follows valid deductive rules.

Because the Rocq proof checker enforces mathematical validity, human software engineers do not need to read the 180 million lines of generated proof code. The integrity of the security guarantee relies on a small trusted computing base consisting of the formal models of the RISC-V processor, the modeled Linux process behaviors, the theorem statements, and the Rocq checking engine itself.¹³⁴ If the proof checker accepts the generated proof script, developers know that no input within the 64-megabyte boundary can trigger a memory violation under the modeled processor rules.

During proof generation, the reasoning model frequently encountered code paths where the proof could not close because the underlying library harbored genuine defects. To prevent human intervention from halting the pipeline, the researchers allowed Claude to draft repair patches for the software, regenerate the formal target specification against the patched assembly code, and resume the proof.¹⁴ This recursive process surfaced hundreds of obscure bugs across the OSS-Fuzz libraries. In one decompression library, the system uncovered a counter underflow that provoked an out-of-bounds write, which required an input of approximately 20 megabytes with a rare internal structure.¹ In an image decoder, it identified an out-of-bounds read that manifested only when processing a 64-megabyte file demanding more than two gigabytes of system memory.¹ It also identified logic errors that never triggered a crash, including an access control flaw where an application failed to enforce file-loading restrictions.¹

Beyond basic memory safety, the researchers applied similar techniques to prove functional equivalence in existing codebases. In one evaluation, Claude drafted a formal specification for RFC 1950, which defines the zlib compression standard, and proved that the zlib implementation inside the Linux kernel satisfies the specification on compiled x86 binaries.¹³ In another test, the model built a Python interpreter in the Rust programming language and verified it against formal CPython semantics using the Verus verification engine, subsequently matching CPython output across 99.95 percent of 1.7 million randomly generated test scripts.¹³

What gaps remain between mathematical proofs and real world execution?

A mathematical proof cannot guarantee absolute security because it verifies code only against an idealized model of execution. The proofs produced in this research do not mean the verified software libraries are free of all bugs. Instead, they demonstrate that a compiled binary will not crash under specific, constrained assumptions: a single-threaded static RISC-V program executing with a fixed memory budget on a modeled Linux operating system.¹² In production deployments, applications run on x86 or ARM processors, use dynamic linking against glibc, and handle concurrent operating system threads, conditions that diverge from the verified environment.¹⁴

The proofs also do not establish that a program will halt. As repository documentation confirms, none of the generated proofs establish a termination statement, meaning a program could enter an infinite execution loop without triggering an illegal memory access.⁴ Furthermore, the proofs operate over memory bounds of two gigabytes for AddressSanitizer builds and 16 gigabytes for UndefinedBehaviorSanitizer configurations, leaving behaviors beyond those thresholds unproved.⁴ AddressSanitizer itself catches specific categories of memory corruption, but it does not evaluate business logic errors, authorization decisions, or cryptographic strength.

Generating proofs at this scale requires substantial computational resources, with proof attempts consuming hundreds of millions of language model tokens. In empirical benchmark runs across 36 small verification tasks derived from OSS-Fuzz, the newer Claude Opus 5.5 model solved half the benchmark using approximately 40 percent fewer tokens than Claude Opus 5.¹³² The researchers also observed that proofs contain reusable components, particularly routines that initialize the C runtime and memory sanitizers. When autonomous agents were permitted to share completed lemmas across a collaborative workspace, their overall token consumption dropped by 17 percent compared with agents working in isolation.¹³

As verification models advance, software maintenance may shift toward treating test suites as formal specifications. Theorem has established an enrollment workflow to evaluate additional open-source libraries, offering to verify qualified public repositories that supply reproducible build scripts and fuzzing targets.¹²⁴ If formal proof generation can be integrated directly into continuous integration workflows, software security may gradually transition away from reactive patching toward mathematical assurance established at the compiler level.

Save this story

The record

27 sentences trace to 4 sources.

All 4Documents 1Records 0Reporting 3People 0

1. 1 A Anthropic Document · anthropic.com · 22 Oct 2026 LLMs are making formal software verification feasible at a much larger scale See the source
2. 2 G GIGAZINE Third-party reporting · gigazine.net · 23 Oct 2026 「バグのないソフトウェア」の実現を目指してAnthropicが「AIを用いて数学的にバグがないことを証明する」という手法を開発 See the source
3. 3 C CellCog Third-party reporting · cellcog.ai · 22 Oct 2026 Anthropic Formal Verification: Claude Proved 123 Libraries See the source
4. 4 K kingy.ai Third-party reporting · kingy.ai · 22 Oct 2026 Anthropic Formal Verification: Claude’s Proofs and Their Limits See the source