A notification pops up in the bottom-right corner of your screen: the agent has finished modifying the code for a live production service and ran the continuous integration pipeline, and all tests passed. With your cursor hovering over the merge button, do you dare merge the code directly into the production branch?
Most engineering leaders would hesitate. Over the past few years, the marginal cost of having large language models write code and call tools has dropped month after month. You used to worry that the model couldn’t write code that runs; now you worry that you don’t dare merge the code it writes directly into the production trunk.
One path is process determinism. Using hardcoded orchestration logic and fixed state machines, you prescribe every step of the agent’s actions in advance. Which file the model reads first and which API it calls second are all hardcoded ahead of time. The other path is result determinism. You only define what the finish line looks like, leaving the model to decide on its own how to break down tasks, inspect error messages, and modify code along the way.
I previously unpacked these two paths in an article on the Claude Code dynamic workflow. That piece started with RAG: traditional RAG hardcodes a search-then-answer pipeline in code, which makes the workflow stable, but its ceiling is limited by how many scenarios the designer can anticipate; agentic RAG hands the search strategy over to the agent, which is flexible, but intermediate results and strategy are crammed into the same context window, making it easy to lose state over long runs. The answer offered by Anthropic’s dynamic workflow is not an either-or choice, but layering: hand control flow to scripts, execution to the agent, and verification to cross-checking across multiple agents. Control flow is process-deterministic, execution is result-deterministic, and verification remains result-deterministic because the evaluation criteria are written in natural language and applied by the agents themselves.
Many people misunderstand formal verification, viewing it as a rigid dogma that locks down every step. In reality, it is the ultimate version of result determinism. What makes it fascinating is that it pushes the verification layer in the layered architecture above one step further. Rather than settling for having a few agents vote that a conclusion is probably reliable, it requires writing the success criteria as a formal specification and having a machine checker verify the proof line by line. In other words, the referee at the finish line of result determinism is replaced—shifting from an agent’s judgment to a mathematical certificate. Control flow can still be left to the agent to explore freely, and execution remains free as well; the change happens in the verification layer, where the standard shifts from natural-language consensus to an exhaustive, machine-checkable proof. Only when the acceptance criteria are rigorous enough to leave no blind spots can the system truly let go of control over the process.
That article also noted a TDD paradox: when an agent was required to strictly follow a TDD workflow without knowing which tests were relevant to the current change, the regression rate actually rose from 6% to 10%. Pure process constraints under incomplete information can be worse than no constraints at all. Formal verification does not belong to this category of pure process constraints. It does not dictate what the agent must write first or second; it only stipulates that at the end, the agent must hand in a proof that passes machine checking.
So is the finish-line referee we currently assign to agents reliable enough? For the vast majority of engineering teams, that referee is nothing more than unit testing, integration testing, or fuzzing. You hook the model up to a continuous integration pipeline and let it modify code, run tests, read logs, and fix bugs on its own. This closed loop works smoothly enough on simple tasks. In principle, however, it faces an insurmountable ceiling.
No matter how many edge cases you write by hand, or how many rounds you run a random-input fuzzer across a cluster, testing is by nature sampling. When all tests pass, it tells you only one thing about the program: across the small, finite subset of sampled inputs you tried, the program happened not to crash. As for the vast sea of untested inputs—whether one of them might trigger an out-of-bounds memory access in some obscure corner—a sampling mechanism can make no promises whatsoever. In a technical essay by Lean creator Leonardo de Moura on February 28, 2026, he drew this exact distinction regarding AI software verification. Testing, he pointed out, can give engineers confidence, but only mathematical proof can provide a guarantee.
Just how large is the blind spot of sampling-based testing? Even in battle-tested industrial code, bugs that slip through the net are everywhere. On October 22, 2026, the official Anthropic research blog disclosed a joint verification effort conducted with partner Theorem. The research team deliberately selected a set of mature open-source libraries for verification. Every one of these libraries had long been integrated into the open-source fuzzing platform OSS-Fuzz, subjected year-round to high-intensity bombardment by automated random inputs. In theory, any easy-to-hit vulnerabilities should have been wiped out long ago. Yet when researchers attempted to construct mathematical proofs for these libraries using formal methods, the model—in the process of working through the proofs step by step—uncovered a batch of real memory bugs that had long evaded fuzzing.
One of them was in a widely used decompression library. Given a specially crafted, rare input of roughly 20 MB, an internal counter would decrement past zero and underflow, directly causing an out-of-bounds memory write.
Another was in a common image decoder. Triggering its out-of-bounds read required a 64MB input and more than 2GB of memory.
A third example was even more subtle. The caller had to invoke APIs in a specific sequence across two handles pointing to the same file in order to trigger an out-of-bounds read.
The same experiments yielded further results across foundational open-source libraries. They independently rediscovered CVE-2026-56132 in the XML parsing library libexpat. And while attempting to verify a widely used PDF reader, they found as many security vulnerabilities in a single week as are typically reported for that reader in an entire year.
Why didn’t continuous fuzzing catch these bugs? Because fuzzing generates test cases through random mutation. As a result, those test cases tend to stay within relatively short byte lengths. Hitting upon a specific 20MB permutation of bytes, or stumbling into a complex cross-handle state sequence by sheer probability, is simply too difficult.
Using sampling-based tests as the sole referee for agents introduces another problem: if an agent optimizes solely for “passing existing tests,” it may even learn to write opportunistic patches that paper over surface-level errors, calling the job done as long as it fools the test script. To truly establish a floor for agent-written code, the engineering world must break out of the habit of plugging in concrete numbers and running the program, and upgrade its finish-line acceptance criteria from sampling tests to mathematical proofs that cover all possible inputs.
Many programmers wave their hands in dismissal the first time they hear that a program can be proven never to crash on any input. No matter how much compute you have, how could you possibly enumerate every possible input?
A quick math calculation shows why. Even for a byte stream no longer than 64MB, the number of possible inputs far exceeds the number of elementary particles in the observable universe. No matter how many processors we pack into data centers, we could never run through every possible input.
The reason exhaustive verification feels impossible to us is that during everyday debugging and testing, we think about code by running it. We are used to feeding a function a concrete input value, letting it execute step by step, and checking whether the resulting output is correct. Formal verification works nothing like that. From start to finish, it never needs to run the program being verified; instead, it turns software testing directly into an algebraic proof problem on paper.
Let’s walk through the simplest possible example. Every programmer
has written an abs function. Suppose our code is
straightforward, with just one conditional branch: if the input integer
x is less than 0, the function returns -x.
Otherwise, it returns x directly.
Now let’s prove a property: no matter what x the user
passes in, the return value of this function is always greater than or
equal to 0.
Following a software engineer’s intuition, we would pick a few
concrete values to test—say, -100, -1,
0, 1, 99, and some edge cases—and
check whether the outputs are all non-negative. Once we see the expected
outputs, we consider the program correct. In a formal proof, however, we
never assign any concrete value to the variable x. We treat
x directly as an algebraic symbol representing any possible
user input. Then we reason logically based on the structure of the
code—specifically, its conditional branches. Following the condition in
the abs function, all possible inputs naturally split into
two mutually exclusive and collectively exhaustive logical branches.
For the first branch, the precondition is x < 0. In
this branch, the code returns -x. By elementary algebra,
since x < 0, -x must be greater than 0,
which satisfies the requirement that the return value be greater than or
equal to 0.
The second branch carries the precondition x >= 0.
Here the code directly returns x itself, which also
naturally satisfies the requirement of being greater than or equal to
0.
Now we put the two branches together. Every possible input case has been accounted for, with nothing slipping through the cracks.
This small example also clearly illustrates how sensitive symbolic
reasoning on paper is to implementation details. In a real computer,
integers are not the infinitely extending integers of a math textbook;
they are fixed-width two’s complement integers. In two’s complement
representation, the range of negative numbers extends one further than
that of positive numbers, leaving a minimum negative value. If we carry
out our symbolic derivation for x over fixed-width two’s
complement integers, then when x takes that minimum
negative value, negating it to compute -x causes an
arithmetic overflow, and the resulting value is still negative.
When this happens, the symbolic derivation gets stuck on the first branch and the proof fails to go through. That forces the developer to go back and either fix the overflow bug or exclude the minimum negative value in the interface precondition.
Looking back at the entire verification of the abs
function, we didn’t run a single concrete calculation in a simulator,
yet in one stroke we pinned down the behavioral boundaries of the
program across all possible valid inputs. Treating inputs as symbols and
performing logical deduction over those symbols is the key to this step.
Once we translate the exact meaning of a programming language or each
processor instruction into mathematical definitions, the execution of a
piece of code becomes equivalent to a chain of logical implications.
The low-level proof work that Anthropic and Theorem had Claude perform starts with this exact kind of symbolic case analysis. Real industrial software repositories, however, are nowhere near as simple as an absolute value function. Production code is full of memory blocks mutated through pointers and loops whose iteration counts are unknown ahead of time. Once you introduce these constantly changing states, how symbolic reasoning on paper can continue determines whether formal verification succeeds or fails.
Engineers familiar with systems programming tend to ask a sharper question after seeing symbolic reasoning on a pure function: real C standard libraries and compiler-emitted binaries are full of pointer addressing, heap allocations, and global state mutations. How can a static method that looks like elementary algebra handle constantly changing program state?
To understand this, we first need to see how formal proofs describe computer memory mathematically. To a hardware engineer, memory is rows of storage cells that can be rewritten at will using high and low voltage levels. Formal logic expresses it differently. At any given moment, the entirety of memory can be represented as a mathematical function mapping memory addresses to byte values. Give it a memory address as input, and it outputs the byte value stored at that address.
When a program executes a memory-write instruction to change the value at a specific memory address to a new value, the proof system does not need to alter any physical storage. It simply defines a new logical memory function. This new memory function returns the newly written value at the modified address, and returns the value of the old memory function at every other address.
To put it in terms more familiar to programmers, you can think of all of memory as a state machine. Every byte in memory is part of the state, and executing an instruction transitions the state machine from its current state to the next. A single-step memory read or write, or a register update, is just one state transition in this machine. Because the transition rules are deterministic, we can follow the state machine step by step in our logical deduction. The real headache is loops and recursion, because how many times they transition depends on the input.
Everyone has written a loop that sums the elements of an array. When you write that code, the program hasn’t run yet and hasn’t received an actual input array. At that point, there is no way to know in advance whether the loop will run ten times, a million times, or ten million times.
If the loop ran a fixed three times, things would be easy: the proof
tool could simply duplicate the loop body three times into three
sequential instructions and apply the symbolic reasoning described
earlier. But if the number of iterations is determined by a symbolic
input length n, we cannot exhaust all possible execution
paths by unrolling the code infinitely. Suppose we want to prove that
when an array-summing loop exits normally, the accumulator variable
sum equals the exact sum of the array’s n
elements, and that throughout execution the memory index i
never goes out of bounds. In that case, unrolling the code simply
doesn’t work.
How, then, can we prove state changes across an arbitrary length
n all at once without unrolling the loop? Formal
verification brings in mathematical induction. And the key to making
induction work on code is finding a logical property that holds true at
the boundary of every loop iteration—what we call a loop invariant.
Take the array-summing example above. The prover needs to construct a
logical property that spans every iteration of the loop: before the
i-th iteration, the value of sum is the exact
sum of the first i elements of the array, and
i lies between 0 and n.
Once you find this invariant, what was an infinite family of loop
paths collapses into a finite three-step deduction. Step one is
verifying the base case: you prove that before entering the loop, in the
initial state where both i and sum are
initialized to 0, the property holds.
Step two is verifying the inductive step: you assume the property holds before a given iteration begins, step through the loop body’s valid memory read and addition update once, and prove that the property still holds before the next iteration begins.
Step three is verifying termination: when the loop exits normally
because i == n, combining the invariant with the exit
condition immediately yields that sum equals the sum of all
n elements.
Once these three steps are complete, no matter how many times the loop executes in practice, its behavior is completely pinned down. Thus, even when a program has state and loops, proving it is logically feasible—but the cost is steep. That steep cost lies primarily in discovering loop invariants. Given a candidate invariant, a computer can easily check whether it is correct. Yet figuring out how to construct an invariant across tens of thousands of low-level instructions involving pointer offsets, conditional branches, and bitwise operations—one strong enough to imply the desired safety property while remaining preserved across every state transition—used to depend entirely on human experts.
The official Anthropic research blog cites a classic study on the seL4 secure microkernel. When that research team tallied the human effort involved, implementing the microkernel’s functionality took roughly 2 person-years, whereas the experts who formally verified it spent around 20 person-years.
Similarly, in Anthropic and Theorem’s binary verification project for open-source libraries, the median size of a verified binary module was only about 18,000 RISC-V instructions. Yet spelling out every state transition and loop invariant meant that a single corresponding formal proof often ran to roughly 600,000 lines. Previously, this grueling labor—requiring human experts to spend years handwriting hundreds of thousands of lines of proof to piece together invariants—was the primary bottleneck holding back formal verification. Today, it has become the exact wedge through which Claude is entering and reshaping the division of labor in software engineering.
At the mention of using a large language model to write a 600,000-line formal proof, any engineer who has been burned by model hallucinations in production will hesitate: how can we possibly trust a mathematical proof written by a probabilistic model that can confidently hallucinate basic multi-digit arithmetic as a security credential?
This question puts its finger on the single most important engineering decision in modern theorem-proving systems. The reason engineering teams dare let a stochastic large language model freely explore a massive proof space is that the entire verification stack is cleanly separated from bottom to top into three layers. At the very bottom sits a tiny, deterministic proof-checker kernel. The middle layer is the formal specification that defines what counts as correct. Only the top layer—proof search, which aims solely for result determinism—is handed over to the agent to explore freely.
In this three-layer architecture, the proof-checker kernel at the bottom is an uncompromising gatekeeper at the finish line. Whether an engineering team uses the Rocq proof assistant (renamed from Coq) or Lean, which has gained tremendous momentum in mathematics and software verification in recent years, the core foundation is a tiny checking program that operates strictly according to fixed rules.
This kernel does not help you find invariants; its sole job is to check line by line whether a submitted proof term violates basic logical axioms. As Leonardo de Moura also emphasized in his February 28, 2026 technical essay, the trusted kernel of a proof system should be as small as possible. To make this foundation even more solid, the Lean community has even written multiple independent reimplementations of the checker kernel for cross-verification, including Lean4Lean in Lean and nanoda in Rust.
Because the bottom-layer checker is completely process-deterministic, it doesn’t matter if Claude hallucinates ten thousand times or wanders down countless dead ends while searching for invariants and piecing together lemmas. If the final submitted proof contains a single logical leap or type mismatch, the underlying checker will immediately flag an error and reject it. Engineers do not need to trust Claude’s long trial-and-error process; they only need to trust that the tiny checker ultimately gave the green light. This brings us right back to the distinction at the beginning: the bottom-layer checker is process-deterministic, and in fact it is the most strictly process-deterministic link in the entire system. Precisely because it locks down the finish line, Claude above it is free to find its way through result determinism. Buying result determinism with process determinism is what this layer is all about. Of course, that does not mean the entire system only needs to trust this kernel—the formal semantics, theorem statements, and underlying dependencies remain inside the trust boundary.
With the underlying checker providing a backstop, the project released by the Anthropic and Theorem teams on October 22, 2026 scaled this three-layer division of labor to an industrial level. How did they handle the formal specifications in the middle layer? To avoid the tedious work of writing formal specifications from scratch by hand, the researchers took existing test harnesses from the open-source fuzzing project OSS-Fuzz and translated their test targets directly into formal specifications. The criterion was: under the specified input bounds and environmental assumptions, the existing fuzz harnesses never crash—including crashes triggered by ASan checks or test assertions. This is not equivalent to ruling out all memory safety errors.
Next, they fed the compiled RISC-V binary machine code along with the system call and memory layout models from the Linux process formal semantics repository to Claude, letting the agent infer loop invariants on its own, decompose helper lemmas, and iteratively refine its proofs by interacting with the Rocq checker.
Under the assumptions of single-threaded execution, static linking, a fixed memory budget, and running on Linux and the RISC-V architecture, the research team successfully produced machine-checked crash-freedom proofs for 123 open-source libraries and 239 fuzzing harnesses. These proofs cover, in one stroke, all arbitrary inputs smaller than 64MB as well as all modeled operating system responses and memory layouts. In total, the project generated roughly 180 million lines of kernel-checked Rocq proof code. A representative subset of these results has been published in an open-source proof subset repository.
To keep the agents producing reliably across proof searches spanning hundreds of thousands of lines, the engineering team also closed off loopholes in training and orchestration. A workflow like this carries a risk of reward hacking: the model might modify the program into a version that trivially never crashes, rendering any theorem provable. To prevent this, the researchers penalized any patch, awarded bonus rewards for proving which inputs a patch changed and how narrow the change was, and logged and audited all patches.
On the compute side, a single proof can consume hundreds of millions of tokens. Across 36 small verification tasks built from real OSS-Fuzz code, Opus 5.5 required roughly 40% fewer tokens than Opus 5 to prove half of the tasks. Allowing multiple agents to share already-proven intermediate lemmas saved an additional 17% of tokens and even enabled agents to complete proofs that would otherwise have failed.
This engineering paradigm—using large models to drive proof search while relying on a minimal trusted kernel to guarantee correctness—is transforming the entire formal methods ecosystem. In his February 28, 2026 essay, Leonardo de Moura noted that Claude, with no specialized proof plugins and no fine-tuning for theorem proving, independently translated the C implementation of zlib into Lean and completed a machine-checked proof of its round-trip property: that compressing and then decompressing always restores the original input. Both mathematical theorem proving and program verification are advancing in tandem. The AlphaProof Nature paper showed how Google DeepMind’s system solved 4 out of 6 problems at the 2024 International Mathematical Olympiad, scoring 28 points and reaching silver-medal level. Driven by agent compute, these advances are making the 1990s vision of proof-carrying code viable at industrial scale.
Once technical decision-makers understand how an agent trades hundreds of millions of tokens for a machine-checked mathematical proof, the next step is to run the practical engineering economics. Now that we can use formal proofs to verify over a hundred open-source libraries, should we immediately replace all our everyday application testing pipelines with formal verification?
In the past, doing formal verification meant finding someone well-versed in formal methods to sit in front of a computer, stare at the code for a long time, and work out the invariants by hand. It was deeply specialized craftwork. People with the right expertise were scarce to begin with, and finding invariants was time-consuming. Because expert time and attention were limited, formal verification could only be applied to high-end bespoke systems like aerospace flight control, core cryptographic algorithms, and the seL4 microkernel—high-value systems that could afford dedicated expert hours.
Now Claude has taken over the most time-consuming, labor-intensive manual task: finding invariants. What used to be grueling work requiring massive hours from scarce experts has turned into compute that can be purchased on demand from data centers and billed by the token. As the way we find invariants changed, the economics of the entire technology flipped with it. It is like moving from a world where you could only commission a structural inspection for a single high-profile building to one where you can prioritize inspecting the public utility pipes shared by the entire street. When compute can be bought at any time, budgets no longer need to be reserved exclusively for a handful of high-value bespoke systems. The more widely a foundational shared library is called by tens of thousands of software packages across the industry, the broader the payoff once it is verified—and the more it deserves to be first in line for investment.
The core fulcrum supporting this economic reversal is the highly concentrated dependency sharing in modern software ecosystems. On September 29, 2026, partner Theorem published a modeling analysis on verifying the software stack. The analysis was based on a September 16, 2026 snapshot of the open-source nixpkgs repository from the nixos-26.05 channel. That repository contained 28,650 packages and 123,471 binaries, totaling 153.7 GB of machine code.
Theorem’s self-reported dependency analysis shows an exceptionally high degree of low-level reuse across the software stack. Verifying just the core 9 MB of shared-library machine code covers roughly two-thirds of the code dependencies across the entire repository. Expanding verification to 170 MB of shared libraries covers 80% of dependencies, and verifying 1.4 GB covers 90%. According to the team’s self-reported benchmark tracking data, between May and September 2026, the speed of model-driven formal verification doubled roughly every 1.9 months, starting from a baseline of about 0.5 KB of machine code verified per hour at roughly $40 per KB.
The research group further assumed that model verification capability will continue to double every two months going forward. That self-reported projection rests on a fairly optimistic assumption—four times faster than research institute Epoch AI’s estimate that general large model capabilities double every eight months. Under that premise, Theorem’s self-reported estimate puts the cost of verifying 95% of all machine code in the nixpkgs repository by the end of 2027 at roughly $134 million.
We can run another calculation. If we did not leverage shared underlying dependencies and instead had every package redundantly verify its own runtime dependency closure, the total cost would skyrocket from roughly $6.4 billion under partial reuse to about $190 billion. In the same self-reported analysis, Theorem also worked through a concrete case study: formally verifying OpenSSL would cost roughly $220,000, but once the proof is complete, the amortized verification cost across every package that directly or indirectly depends on OpenSSL comes to only about $14 per package.
For engineering teams, this draws a clear decision boundary: for top-level application code whose requirements change weekly and whose lifespan is measured in months, spending hundreds of millions of tokens to piece together loop invariants is still not worth the cost; but for foundational public libraries at the bottom of the dependency tree, whose interfaces are relatively stable and reused by countless upstream applications, using compute for a one-time buyout of result determinism on core properties has become a sound investment.
Yet while compute can amortize the drudgery of finding invariants, it cannot bridge three inherent gaps in formal verification. The first gap is that a mathematical proof is only ever accountable for the restricted properties written into the specification and environment model. Anthropic and Theorem’s engineering practice verifying 123 open-source libraries shows us that their crash-freedom guarantee for inputs under 64MB rests strictly on modeling premises of single-threaded execution, static linking against the musl standard library, a fixed memory budget, and the RISC-V processor architecture. In real cloud production environments, however, the vast majority of services run on x86 or ARM processors, dynamically link against the complex behaviors of the glibc standard library, and constantly contend with multithreaded concurrency races. Moreover, safety specifications translated from AddressSanitizer (ASan) checks do not catch every class of memory error in the first place. Code branches not reached by the test harness, dead code, and parameter misuse where callers violate preconditions likewise fall outside the umbrella of the mathematical guarantee. Decision-makers who mistake a crash-freedom certificate for the elimination of all security vulnerabilities or business-logic flaws can easily step into a void in real-world scenarios outside the modeled boundary.
The second gap compute cannot buy its way across is the accuracy of the specification itself. The third gap is the scrutiny of the trusted computing base. Even though we do not need to trust Claude’s reasoning process during proof search, that does not mean the overall engineering effort only has to trust the tiny Rocq checker kernel. Across Anthropic and Theorem’s verification chain, the trusted base remains a checklist that human experts must guard vigilantly. It includes the Rocq checker itself, the manually or semi-automatically modeled formal semantics of the RISC-V instruction set, the semantics of Linux processes and system calls, whether the theorem statement—that is, the safety specification—was written without error, and lower-level indirect dependencies including the physical chip hardware, the host operating system, and the OCaml compiler used to compile the checker.
If the semantics of the underlying instruction set miss a hardware edge case, or if the theorem statement bakes an unreasonable premise in as a default assumption, even the most uncompromising checker will happily sign off on an empty guarantee detached from physical reality. Now that models have commoditized the heavy labor of finding invariants through compute, the truly irreplaceable core work of software engineering has come into sharp relief. Just as Leonardo de Moura judged on February 28, 2026, as writing implementation code and searching for proofs grow ever cheaper, writing specifications that accurately define what a system is actually supposed to do—together with rigorous auditing of the trusted base—will ultimately become the most central engineering discipline for human engineers.