Anthropic used Claude to formally verify 123 open-source libraries at the assembly level

Anthropic verified 123 libraries with machine-written proofs

In an October 22 research post that reached the front page of Hacker News, Anthropic says it used Claude to generate formal correctness proofs for 123 real-world open-source libraries, proving security properties directly on compiled RISC-V assembly rather than on source code. The project was run with the verification company Theorem, and Anthropic believes it is the first large-scale attempt to apply AI-driven formal verification to production software at the assembly level. While constructing the proofs, Claude also turned up bugs that had eluded detection for years, even in code that had been subjected to trillions of test runs.

Why formal verification stayed impractical

Ordinary testing can only sample behavior. Fuzzing, which feeds enormous numbers of generated inputs into a program hoping to trigger a crash, is inherently brute force: the input space is infinite, so no amount of fuzzing can rule out every failure path. Formal verification takes a different route. Developers translate code into a mathematical model and attempt to prove that it always obeys a set of stated rules. If a proof fails, the nature of the failure points toward a possible bug; once every failure is fixed and the proof goes through, the code is guaranteed free of bugs that would violate those rules.

The historical catch is cost. Anthropic notes that proofs can far exceed the size of the code they cover and demand a rare, specialized skill set. The seL4 kernel took roughly two person-years to implement but around twenty person-years to formally verify, which confined the technique to domains like avionics. According to Anthropic, frontier models change this economics because they can autonomously push through the enormous proof workload that made verification impractical for ordinary projects.

From fuzz tests to specifications

The hardest part of verification is stating what "correct" even means. A PNG decoder has a natural specification in RFC 2083; a web browser or text editor does not. Anthropic's workaround was to derive specifications automatically from the projects' own test suites — the spec simply says the suite always passes.

In practice, the team took fuzzing entry points from Google's OSS-Fuzz program, which continuously fuzzes open-source C and C++ projects, and asked Claude to prove, over the compiled RISC-V instructions, that no input up to 64 MB can cause a crash. Once that is proven, further fuzzing of that entry point adds nothing: a fuzzer samples from an infinite input space, while the proof covers all of it.

Specifically, Claude proved that these programs always exit normally, without memory-safety violations or failed assertions, for every input under 64 MB and every modeled Linux response and memory layout. The guarantees assume a single-threaded static binary, a fixed memory budget, a RISC-V CPU and Linux. Anthropic is explicit that this falls well short of eliminating every possible bug, but frames it as a credible path toward broader coverage.

What is being released

Anthropic is publishing a subset of the proofs along with its formal semantics for RISC-V and the Linux environment, so that anyone can audit and reuse them. Theorem says it will run the same pipeline for other open-source projects and has released a Claude skill to help developers begin verifying their own code. The post also describes early explorations of other verification tasks: assessing the security of the zlib compression algorithm, proving behavioral equivalence of a Python interpreter written in Rust, and digging out long-standing flaws in critical software.

Why it matters

Anthropic's stated motivation is defensive. LLMs are increasingly good at locating flaws and at chaining individually harmless bugs into serious exploits, and the Linux kernel alone recently saw more than 1,000 disclosed vulnerabilities. Testing, however extensive, can demonstrate the presence of bugs but never their absence; proofs can, within the boundaries of their specifications and assumptions. If the cost of writing proofs keeps falling as models improve, and reusable proofs accumulate across codebases, formal verification could shift from an avionics-grade luxury to a routine part of securing everyday open-source software. The caveats matter — the guarantees here hold only for bounded inputs, single-threaded binaries and a modeled operating system — but a demonstration that a model can now do work that once consumed person-decades changes what "tested" can plausibly mean for real codebases.