Anthropic shows LLMs can formally verify assembly code at scale across 123 open-source libraries

Anthropic and Theorem used Claude to prove that RISC-V programs from open-source projects in OSS-Fuzz handle memory safely. They created 180 million lines of proofs checked by a computer and found bugs that earlier testing had missed.

Anthropic has shown that large language models can now use mathematical proofs to check software on a very large scale. Until now, this kind of careful checking was mostly used for software where safety was especially important. Working with Theorem, Anthropic used Claude to check memory safety in 123 open-source software libraries turned into RISC-V assembly code, a low-level form of computer instructions. This was the first time AI-powered formal verification had been used on such a large number of real, compiled programs.

The team started with existing software tests from Google's OSS-Fuzz project. They turned these tests into exact mathematical rules saying that each program must never crash when given any input smaller than 64 megabytes. Claude then wrote mathematical proofs using a tool called Rocq, which checked each proof automatically. In total, the team proved that 239 entry points, or places where programs begin running certain operations, were safe across 123 libraries. The proofs contained about 180 million lines of code.

"We proved that these programs will always exit normally without triggering memory-safety errors or failing assertions, for every input less than 64 MB and every modeled Linux operating system response and memory layout," the Anthropic team wrote. In simpler terms, they proved that the programs would finish normally without certain memory errors or failed checks, even when the operating system responded in different ways or memory was arranged differently. These proofs apply to RISC-V programs running on Linux that use only one thread, have all their code included in the compiled program, and have a fixed amount of memory available.

While doing this work, Claude found hundreds of bugs that had gone unnoticed even after trillions of automated tests called fuzzing runs. One bug in a program that decompresses data caused a counter to drop below its allowed value. It happened only with 20 MB inputs and an unusual memory arrangement. Another bug in an image decoder made the program read outside the memory area it was supposed to use. That bug needed a 64 MB input and more than 2 GB of memory to appear. Claude also found a previously known security problem, CVE-2026-56132, in libexpat, which needed input with many layers nested inside one another. It also discovered a logic error that meant a feature meant to restrict access to files did not always enforce those restrictions.

The proofs checked the actual compiled RISC-V instructions instead of the original source code written by programmers. Theorem supplied exact mathematical descriptions of how RISC-V instructions work and how Linux programs behave. Rocq's built-in checking system, called its kernel, then checked each proof against the rules. This means developers do not have to trust the millions of lines of proof code themselves. They only need to trust the mathematical models, the statements being proved, and the Rocq checker.

"This doesn't mean these libraries contain no bugs," the researchers explained. "It means that any remaining bugs either are to be found within the artifacts listed above or are outside the scope of Claude's proof." In other words, the proofs give strong guarantees about the specific things they check, but they do not promise that every possible problem has been removed.

Reusing proofs made the work much faster and cheaper. When AI agents worked in a shared space and could copy proofs written by other agents, they used 17 percent fewer tokens, the pieces of text AI models process. In the OSS-Fuzz project, agents took completed proofs and changed them to work with new programs. Many shared parts stayed almost exactly the same across different libraries, especially the parts that set up the C runtime and AddressSanitizer, a tool used to find memory errors.

Anthropic also tested other ways to check software beyond the OSS-Fuzz project. In one experiment, Claude wrote an exact mathematical description of RFC 1950, the standard for the zlib data format. It then proved that the Linux kernel's zlib implementation followed that standard at the x86 machine-code level. To do this, it used descriptions of x86 instructions that Claude had also created. In another experiment, Claude built a Python interpreter, a program that runs Python code, using the Rust programming language. It then used a verification tool called Verus to prove that the interpreter followed CPython's rules. When tested with 1.7 million randomly generated programs, its behavior matched CPython 99.95 percent of the time. In another test, Claude tried to verify a widely used PDF reader and found as many security bugs in one week as are normally found in a whole year.

Newer AI models are also making this work less expensive in terms of tokens. In a test involving 36 verification tasks taken from real OSS-Fuzz code, Opus 5.5 finished half of the proofs while using about 40 percent fewer tokens than Opus 5. The researchers believe token use will keep improving as AI models receive more training on long, difficult verification tasks.

There are still important limits. The proofs only cover RISC-V programs that use one thread, include all their code in the compiled program, and use a C standard library called musl libc. Most real-world software instead runs on x86 or ARM processors and loads shared code while running, often using glibc. AddressSanitizer also cannot detect every kind of memory-safety problem. The team did not verify every entry point in every library. And real programs can use library functions incorrectly, which may damage memory in the program that called the library even when the library itself works as expected.

The team concluded that formal verification, which uses mathematical proofs to check software, used to be practical mainly when experts built special guarantees for software where safety was extremely important. They believe it will soon become about as practical as fuzzing is today for almost all software used in real products. Theorem is offering to use the same process to check other open-source projects. It has also published a Claude skill that helps developers begin verifying their own code.

The proofs, exact rules, and mathematical models created during this project are available so other people can check them independently.