In a test, Anthropic's Claude found and fixed hundreds of bugs in 123 popular open-source software components (Anthropic, 2026). It then proved that, under set conditions, the software will not crash.

Ordinary security tests cover the inputs they try and nothing else. Run a trillion inputs against a program and find nothing, and someone can still find the one input nobody tried and break the software.

On October 22, Anthropic and a small company called Theorem reported a different kind of result. The proofs cover 239 entry points, the places where outside data enters a program, and show that none of them can crash on any input up to 64 megabytes (Anthropic, 2026).

Those entry points sit in 123 open-source libraries, the reusable building blocks that other programs borrow. A checking program verified each proof, so no person needed to read them. The result holds up and it has limits, and anyone who buys software should know where the limits are.

Volunteers had already written the hardest part of the proof

A proof starts with a precise statement of what the software must do, and writing that statement has kept this work rare. The team behind seL4, the core of an operating system, spent about 25 person-years building and verifying that one piece of software (Trustworthy Systems, n.d.).

Anthropic and Theorem reused statements that already existed. Google runs OSS-Fuzz, a free testing service for open-source software, and library maintainers had written tests for it.

Each test carries a built-in promise that the program must not crash. The team turned each test into a mathematical statement of that promise, and Claude wrote the proofs in a few weeks (Anthropic, 2026).

A checking program confirms each proof

Claude wrote about 180 million lines of proof in total. A typical proof runs to about 600,000 lines, for a program of about 18,000 machine instructions (Anthropic, 2026).

Nobody reads that much, so a checking program called Rocq confirms each step, and an auditor examines the checker.

The proofs cover the finished program the computer runs, so a mistake made while translating source code into that program cannot undermine them. Readers still have to trust two things: the written models of the chip and the operating system, and the exact statement each proof covers (Anthropic, 2026).

In February the same team reported more than 500 serious flaws that Claude Opus 4.6 found in open-source code (Axios, 2026), so the October work adds a proof that the repaired code holds up under set conditions.

The work is expensive today. Proofs can take hundreds of millions of tokens, the units of text a language model reads and writes, and Anthropic expects the cost to fall as models improve (Anthropic, 2026).

The proof covers one chip design, and suppliers ship on others

The proofs assume a program that does one task at a time, with a fixed amount of memory, running under Linux on a chip built to the RISC-V design (Anthropic, 2026). RISC-V, short for Reduced Instruction Set Computer, version five, is an open design from RISC-V International.

Anthropic says people run these libraries on x86 or Arm chips, the designs inside servers and laptops. Anthropic also says a verified program can still contain bugs, in the parts a reader must trust or outside what the proofs cover (Anthropic, 2026). The proofs also do not show that a program always finishes, so one could still run forever (Kingy AI, 2026).

A proof belongs to one specific program, so a supplier who calls a library proven may be describing a build that never leaves the lab. Anthropic's post includes one x86 example, a compression routine from the Linux kernel, so the gap may narrow (Anthropic, 2026).

A supplier's claim of proof means something after it names the program and the chip.

Fuzzing, the random-input testing described above, still has a job where proofs stop.

Trail of Bits took two bugs credited to formal verification in popular smart-contract protocols and found them again with a fuzzer, and the firm judged proof tools harder to use than fuzzers on complex code (Trail of Bits, 2024).

That work covered smart contracts, a different kind of software from these libraries. Fuzzing is easier to run, and a proof gives a firmer guarantee on the code it covers.

Outsiders can check a subset of the evidence today

Anthropic published a subset of the proofs on GitHub, along with the chip and operating system models. It held back proofs that could reveal unfixed bugs in open-source projects, and it released complete proofs for tests that needed no fixes, plus the statements for tests it could not prove (Anthropic, 2026).

Holding proofs back protects maintainers who have not shipped fixes, and it limits what outsiders can check.

One write-up of Theorem's public repository counts 60 entry points across 25 libraries (Kingy AI, 2026). The totals of 239 and 123 come from Anthropic.

Theorem will run the same process for other open-source projects through a service called OSS Verify (Anthropic, 2026). Maintainers who sign up get a proof, and buyers get a new thing to ask for.

A small startup wrote the models every proof rests on

Theorem supplied the written models of the chip and of Linux (DevOps.com, 2026). The company started in 2025, joined a Y Combinator batch that year, and lists a team of four (Y Combinator, n.d.).

One funding tracker records a $6.0 million seed round in January 2026 (VCBacked, 2026).

Anthropic published the models, so someone else could take them over. Linux keeps changing, and someone has to update the models each time.

Anthropic expects formal verification to become as practical as fuzzing for almost all production software soon (Anthropic, 2026). That forecast comes from a vendor, and a buyer who acts on it depends on whoever maintains the models.

A proof covers one program on one chip. Anything outside both has no guarantee.