loading
loading
Anthropic's Claude Proves 239 Open-Source Libraries Crash-Free, Exposing Fuzzing Blind Spots Anthropic and Theorem used Claude to produce machine-checked no-crash proofs for 123 open-source libraries at the assembly level, uncovering long-latent bugs. - Anthropic and Theorem used Claude to formally verify 123 open-source libraries at the RISC-V assembly level. - Claude produced ~180 million lines of Rocq proofs covering 239 fuzz entry points in a few weeks. - Proofs guarantee no crash on any input under 64 MB, including AddressSanitizer violations. - Process uncovered bugs fuzzers miss, including a decade-old latent logic bug and CVE-2026-56132. - Opus 5.5 completes proofs with roughly 40% fewer tokens than Opus 5; shared workspaces save another 17%. - Proofs, semantics, and a Claude skill are open-sourced for reuse. Anthropic’s Frontier Red Team and Theorem used Claude to generate machine-checked proofs for compiled code from 123 open-source libraries. In their report, the researchers say the system also found and patched flaws that libraries had collectively undergone trillions of fuzzing runs without exposing. The results suggest that automated proof generation could make formal verification practical for widely shared software components. A 20-person-year baseline Formal verification uses mathematical proofs to establish that software satisfies a precise property under stated assumptions. Tests and fuzzers reveal failures among the inputs they execute. A formal proof covers every input allowed by its theorem and execution model. The seL4 microkernel illustrates the historical cost. Its implementation took about two person-years, while verification required about 20 person-years. That tenfold increase has largely confined full-system verification to avionics, operating-system kernels, cryptographic code, and other projects that can support specialist teams. The Anthropic and Theorem pipeline completed the following work over several weeks: A typical proof therefore contained about 33 proof-script lines for each target instruction. Those counts describe generated checker input, not human-authored complexity. The pipeline produced individual proofs without manual proof engineering, while humans supplied the models, tooling, harnesses, and overall verification design. Fuzz harnesses become theorem statements An OSS-Fuzz harness gives a fuzzer a callable entry point, converts arbitrary bytes into program input, and defines conditions that count as failures. The researchers reused those harnesses as specifications, avoiding the broader and often ambiguous task of defining complete library correctness. - The pipeline compiled each library and its fuzz harness into a static RISC-V binary linked with musl libc. - AddressSanitizer instrumentation converted covered memory errors into observable crashes. - The theorem stated that no input up to 64 MB could make the entry point crash under the modeled execution environment. - Claude generated Rocq proof scripts, investigated blocked proofs, patched discovered defects, and tried again. - Rocq’s proof kernel checked every proof step mechanically. Rocq, formerly known as Coq, is an interactive theorem prover with a small proof-checking kernel. Claude’s generated scripts can be large or difficult to read without weakening the result, because the kernel accepts a theorem only when every inference follows from the formal rules. For theorem checking, the team identifies three central elements in the trusted computing base: - The formal models of RISC-V instructions and Linux processes - The exact theorem statements - The Rocq proof checker Review can therefore concentrate on whether the models and theorem express the intended guarantee. The checker handles the 180 million lines of generated proof script. Rare inputs reveal fuzzing blind spots Proof attempts forced Claude to account for paths that random or coverage-guided input generation had failed to reach. In one library, the system found a counter underflow in a bundled decompressor that could cause an out-of-bounds write. Triggering the flaw required an input of roughly 20 MB with a rare layout, while the report says many fuzzing campaigns cap inputs near 1 MB. The researchers also reported several other findings: - An out-of-bounds image-decoder read requiring a 64 MB input and more than 2 GB of memory - A rediscovery of CVE-2026-56132 in libexpat - A file-access restriction that some execution paths failed to enforce - As many security bugs in one week of work on a widely used PDF reader as that project typically receives in a year Large inputs, high memory requirements, and narrow structural constraints make these cases expensive for fuzzers to discover. Symbolic proof must cover them whenever they remain possible under the theorem. No-crash proofs reach program behavior Fuzz harnesses can encode semantic properties by deliberately crashing when an invariant fails. A proof of crash freedom then establishes that invariant for every permitted input, subject to the same model and bounds. The LZO harness, for example, crashes when compressing and then decompressing data fails to reproduce the original input. Proving that the harness cannot crash establishes the round-trip property across the verified input domain. The cpp-httplib proof required a deeper machine-code invariant. To exclude stack overflow in the recursive destructor for std::set, Claude had to establish that libc++’s red-black tree remains logarithmically balanced. The final proof therefore covered an internal data-structure property needed to guarantee bounded recursion. Token costs start to fall Large proofs still consume hundreds of millions of model tokens, making inference cost and model efficiency central constraints. Anthropic compared several models on 36 smaller verification tasks and measured how the completion rate changed with token budget. Opus 5.5 solved half of the benchmark tasks with about 40% fewer tokens than Opus 5. Shared proof workspaces also reduced token use by 17% compared with isolated agents. Agents reused completed components for recurring obligations such as C runtime initialization and AddressSanitizer setup, and some completed tasks that they had previously failed alone. The guarantee has firm boundaries Anthropic’s result establishes a narrower guarantee than a general bug-free designation. Its scope follows directly from the theorem, build configuration, instrumentation, and machine model. Source-level security claims also depend on the compiler and AddressSanitizer instrumentation mapping relevant defects into behavior represented by the theorem. A valid proof can establish an incomplete specification perfectly, so theorem review remains a human responsibility. The team released a proof archive, the machine semantics, and a Claude skill for adding projects to the pipeline. Theorem is also offering to run the system on open-source projects by request. Shared libraries improve the economics Production software concentrates heavily around dependencies such as glibc, OpenSSL, cURL, and zlib. A proof generated for the exact version and build configuration used by many downstream projects can spread its cost across that entire user base. Practical adoption will require support for common architectures and libc implementations, reproducible builds, careful theorem review, and continuous verification as dependencies change. The reported work supplies evidence that language models can automate much of the proof construction, which has historically been the most labor-intensive part of applying formal methods to real-world code.
document fetched 2026-10-23 20:28