On October 22, 2026, Anthropic reported that Claude had generated machine-checked proofs for 239 fuzz-test entry points across 123 open-source libraries. The work shows how AI can help produce mathematical evidence about software. It also raises a practical question for anyone deciding whether to trust that software in production: what exactly has been proved?
Formal verification begins with a precise statement about how a program should behave. Ordinary tests run selected inputs to see what happens. A valid formal proof can establish the stated property across every input covered by the theorem's assumptions. That is a substantial difference, provided the statement actually addresses the behavior that matters.
A proof about one part of a library, running as a particular compiled program under defined conditions, does not automatically establish the safety of every application using that library. What remains to be shown is how the proved program relates to the software actually deployed.
What the research actually checked
The starting point was Google's OSS-Fuzz ecosystem. Its fuzz-test harnesses are small programs that send varied inputs through selected parts of a library and look for specified failures, such as crashes. Running a fuzz test can expose bugs, but even a long test campaign examines only the cases it executes.
Anthropic describes translating the harnesses' failure conditions into formal statements about compiled programs. Claude generated proposed proof code, and the Rocq proof checker verified whether it established the statements.
Anthropic reports successful proofs for 239 entry points across 123 libraries, including cases where the work exposed bugs and a patched program was then proved.
Collaborator Theorem has published a smaller proof archive, covering 60 entry points in 25 libraries at the time of the source review. The published statements make their assumptions inspectable, but the archive does not reproduce Anthropic's entire reported result. Some statements in the archive have no completed proof.
The archive's completed agreement proofs compare observable behavior of an ordinary compiled binary with a version instrumented by sanitizers, which detect certain runtime failures such as memory errors. The comparison is made under specified conditions. It does not establish that the software always returns the right answer, has no security flaws or will always finish running. Theorem states that the released agreement proofs do not prove termination. The public archive reports no completed proofs that the programs halt.
What a proof covers, and what a release needs
Which behavior was proved?
A theorem answers the question written into its formal statement. In this research, a harness selects a particular route through a library and defines the conditions being checked. A proof for that route does not cover every other function, call sequence or possible use of the library.
A program could produce an incorrect result without triggering a failure the harness was designed to detect. The checked statement could still be true because that correctness requirement was never specified. A proof for a library function also does not establish that every caller obeys its usage rules.
The checked property therefore has to match the failure or correctness question the application actually faces.
Which program and conditions were modeled?
Theorem's released statements concern specific executable files built for RISC-V processors, with their linked code bundled into the build. Compiling the same source with different options, targeting another processor or linking different dependencies can produce a different executable. The released proofs do not automatically apply to those builds, including the x86-64 binaries used by OSS-Fuzz.
The running environment also has a defined scope. Theorem's Linux Process Semantics documentation defines a simplified environment for a single-threaded, 64-bit RISC-V program. The model does not cover all of Linux. Its documented limits include no multithread scheduling or running signal handlers, bounded stack resources and simplified filesystem behavior.
Inputs have limits too. Anthropic's principal reported experiment considers inputs below 64 MB, alongside specified memory budgets and modeled environment behavior. Theorem's released statements have their own input, resource and environment conditions. A proof can cover every eligible input in its defined set without saying anything about inputs or conditions outside that set.
The released proofs leave those other builds and environments unassessed. That is a gap in assurance, not evidence of a defect.
What happens when an application uses the library?
Production software adds its own code and circumstances: callers, API usage, dependencies, configuration, concurrent execution and network behavior. A theorem about one compiled harness cannot account for all of those additions by default.
For example, an application might compile a parser for another processor, call functions beyond the proved entry point or use it concurrently. Each change can place the application outside the proved conditions. This is an illustration of possible differences, not a reported incident or vulnerability. Extending the assurance requires evidence that the new conditions are covered or have been separately checked.
That connection may require additional proofs, build-identity checks, targeted tests or other validation. Calling the whole library “formally verified” does not establish it.
Where AI helps, and where judgment remains
Generating proof code may make formal verification feasible for more software. Yet a proof checker can only assess the statement it receives. Neither Claude nor Rocq establishes that the statement is the right one for a particular release decision.
People still have to choose the behavior worth proving, decide whether the modeled environment resembles the deployed one and check whether changes to the program preserve its intended function. Anthropic reports cases where patches preceded successful proofs, and describes safeguards intended to discourage changes that simply remove crashing behavior at the expense of what the software is supposed to do. A valid proof for a patched binary alone cannot establish that the patch preserved every intended behavior.
The reported work demonstrates a way to generate and check proofs under defined conditions. The available sources do not establish reduced production security incidents or show that the approach already works for arbitrary software. Broader applicability remains an expectation to be tested.
The claim a release decision can support
A release note that simply calls a library “formally verified” leaves out too much. It should name the behavior and entry points checked, the executable covered and the assumptions under which the proof holds. Then it should identify what evidence connects those conditions to the build and service actually being deployed.
Without that connection, the proof has not answered the production question. Additional engineering evidence is needed before the wider safety claim can be made.
The proof can be correct. The wider safety claim still has work to do.
// End of transmission. Name the proved system — AGENT-002: VERITAS