Anthropic and the verification company Theorem used Claude to prove, with maths checked by a computer, that parts of 123 open-source libraries cannot crash or misuse memory on any input under 64 MB. These libraries are shared code that programs use to open files such as images and archives. Testing tries some inputs, while a proof covers all of them, like calculating that a bridge holds every load up to a stated weight instead of driving trucks across it. Each library already had a fuzz test, which feeds it random inputs and flags crashes. The team turned each test automatically into a rule about the compiled machine code, the exact instructions the chip runs. Claude wrote proofs that the rule always holds, and a checking program called Rocq verified them: about 180 million lines, written in a few weeks.
Bad memory access is a leading cause of security holes, Anthropic notes, and such proofs were rare because they cost so much: the seL4 operating system kernel took two person-years to build and 20 to verify. Writing the new proofs exposed hundreds of bugs, which Claude patched, and Anthropic says some had escaped years of testing. One appeared only on an input of about 20 MB with a rare layout, while fuzzers usually stop near 1 MB. The guarantee assumes programs that run one task at a time on RISC-V chips under Linux, not the x86 or ARM chips most people use. Theorem now offers this free to qualifying open-source projects.
Read More: Anthropic’s free open-source bug scanner, a separate service that scans open-source projects for security bugs and emails the findings to maintainers
Sources:
- LLMs are making formal software verification feasible at a much larger scale (Anthropic)
- OSS Verify: free formal verification for open source (Theorem)
- Anthropic’s Claude now writes code and proves it safe automatically (The Decoder)
Disclaimer: For information only. Accuracy or completeness not guaranteed. Illegal use prohibited. Not professional advice or solicitation. Read more: /terms-of-service
Reuse
Citation
@misc{kabui2026,
author = {{Kabui, Charles}},
title = {Claude {Proves} {Parts} of 123 {Open-Source} {Libraries}
{Cannot} {Crash} on {Inputs} {Under} 64 {MB}},
date = {2026-11-10},
url = {https://toknow.ai/posts/claude-formal-proofs-123-open-source-libraries-memory-safety/},
langid = {en-GB}
}