Proving the Foundation, Checking Every Change

In late October, Anthropic's Frontier Red Team, working with Theorem, published a remarkable piece of work. Claude produced machine-checked proofs that 239 entry points across 123 widely used open-source libraries will never crash on any input under 64 MB - roughly 180 million lines of proof, every line checked by an independent proof checker, Rocq. Along the way it found hundreds of real bugs, including some that years of testing had missed.

The seL4 microkernel took about 20 person-years to verify. Formal verification has always been the right answer that almost nobody could afford. This work changes that, and it is good news for everyone who cares about software that does what it should.

The post's conclusion is the part we keep coming back to. The authors predict that formal verification will soon be as practical as fuzzing for almost all production software, and that it will move "from bolted-on to built-in" - into development workflows and language design. We agree. It is the conviction our own work is built on.

One step in their workflow

There is a detail in the post that shows where the next layer fits.

When Claude found a bug, it was allowed to fix it. The patched code produced a new specification, and the patched program was proven crash-free again. The authors flag the risk themselves: a model could make any program "provable" by rewriting it into one that trivially never crashes. So they penalized patches, audited them, and offered Claude extra credit for proving which inputs a patch changes, and how few they are.

That is exactly the question we have spent the last two years building tools to answer: did this change alter only what it was meant to alter? It is a different kind of proof - not "this program never crashes" but "this version behaves like that version, except where we said it would differ." In their workflow it guards against reward hacking. In everyday development, it is the question behind every pull request, and we think it belongs in the workflow as a standard step of its own.

Two layers

The work Anthropic and Theorem published proves a property of a whole program: it never crashes, on any input, on a precisely modeled machine. Their Limitations section is unusually candid about what that does and doesn't cover, and it names the next frontier itself: specifying "what callers must do for each public function." That is a behavioral question.

Equivalence checking approaches behavior from a different direction. Instead of writing down what a function should do, it uses the version you already trust as the specification, and asks whether a changed version computes the same results for every input. If it doesn't, it returns the exact input where they differ.

The two layers fit together:

	Proving the foundation	Checking every change
What is proven?	A program never crashes - no memory-safety errors, no failed assertions - for every input under 64 MB.	A changed function computes the same results as the original for every input, or FMToolkit shows the input where it doesn't.
Under what conditions?	A formal model of a specific machine: single-threaded RISC-V binaries, statically linked against musl. Crash behavior depends on the machine, so the model matters.	The source-level behavior of typed Python functions. Equivalence is about what code computes, not the chip it runs on, so the answer doesn't depend on the architecture (unless you are comparing compiler output itself).
When does it run?	Once per library, with proofs reused as the code evolves - the foundation everything else builds on.	On every change, in the pull request, in seconds.

Prove the foundation once. Check every change as it lands. A library proven never to crash is a better base for every function built on it; a check that every change preserved behavior keeps those guarantees from eroding one commit at a time.

What we've learned running this loop

In June we published an experiment that put this layer inside an AI coding loop. An LLM proposed optimizations for 214 functions in the maths/ directory of TheAlgorithms/Python. FMToolkit, our equivalence checker, decided which ones were kept. It accepted 28, 14 of them with complete proofs; rejected seven plausible-looking rewrites with concrete counterexamples; and discarded everything it could not verify. Every commit carried its verdict and confidence level. No human reviewed anything until the evidence was already in the log.

One accepted change, at 0.95 confidence rather than a full proof, turned out to be wrong. Because the confidence level traveled with the commit, we found it, reverted it the same day, and filed the engine bug. We published that too. Grading trust, and carrying the grade with the change, is most of what makes a loop like this safe to run unattended.

A small example shows the kind of thing this layer catches. A function rounds amounts with int(x + 0.5). A cleanup - the kind an AI assistant suggests - replaces it with Python's built-in round(x). Every test still passes. FMToolkit returns not equivalent at x = 0.5: the old code gives 1, the new code gives 0, because Python's round() sends halves to the nearest even number. Neither rule is wrong. But the behavior changed in a commit labeled "cleanup," and now a person gets to decide whether it should have. There are more worked examples in our articles.

Some honest limits. FMToolkit works on typed Python functions today; C and Fortran support are in development. It proves equivalence, not correctness: if the original had a bug, a proven-equivalent copy has it too. Most checks finish in under a second, harder functions can hit a 30-second limit and come back as a timeout rather than a verdict, and every result states its confidence.

Where this goes

Anthropic's post ends by encouraging others to experiment. Here is ours, and an offer.

If AI agents are going to write and patch code at the pace this work suggests, every agent loop needs a gate that decides which changes are kept - fast, automatic, and grounded in proof rather than another model's opinion. An equivalence checker can be that gate: in a pull request, in CI, or inside an agent's own loop in tools like Claude Code. Foundation proofs and change-level checks belong in the same workflow, and we would welcome the chance to compare notes with the teams building the first layer.

FMToolkit is backed by the DARPA Embedded Entrepreneur Initiative and available now as a GitHub App. The free launch plan includes everything, including the coverage assessment that shows which of your functions are in scope today. Or start a conversation with our team.

---

Sources: Anthropic, "Formal verification" research post (Frontier Red Team, Oct 22, 2026); Theorem and OSS Verify.