The Comprehension Debt: Trusting Code That Nobody Understands

For most of software’s history, writing code was the expensive part. You thought hard, you typed slowly, you reviewed what you typed, and the artifact you produced, the code itself, really was the thing of value. Verification rode along almost for free, because whoever wrote a change was right there, holding its intent in their head as they wrote it.

Coding agents quietly broke that arrangement. When an agent produces a pull-request-ready change in the time it takes to read the ticket, code stops being scarce. Two things become scarce in its place. The first is trust: is this code even correct? The second is quieter, and I’ve come to think it’s the deeper of the two: does anyone understand it? Reading the diff used to settle both at once, because the reader was usually the author. It settles neither when the diffs arrive faster than anyone can read them. Hold onto that distinction, because the whole argument turns on it: you can buy back trust without buying back understanding.

There’s a useful name for that second problem. In 1985 Peter Naur argued that a program’s real substance is not its text but the theory in its authors’ heads: why it is built this way, what is load-bearing, what would quietly break if you changed it. Code whose theory has been lost is, in his word, dead, still running but no longer safely changeable. When an agent writes the code and no human ever held that theory, you begin every future task already in the hole. Call it comprehension debt: the widening gap between the code that exists and the code anyone actually understands.

flowchart LR
  CHEAP[When code is cheap] --> T[Trust
is it correct?]
  CHEAP --> U[Understanding
does anyone grasp it?]
  T -->|a machine can buy this back| V[Verification
trust without reading]
  U -->|no machine buys this back| D[Comprehension debt
the widening gap]

The diff doesn’t scale

One number reframed the problem for me. When Anthropic launched its own code-review tooling in early 2026, it disclosed that beforehand more than 8 in 10 pull requests inside the company were merging without meaningful human review feedback. Some of that is surely trivial diffs and rubber-stamping. But a company doesn’t build a tool to handle a “flood” of AI-generated code unless the volume has outrun the humans’ capacity to read it. The people who build these agents hit the verification wall first, and hardest.

Andrej Karpathy frames the same dynamic as a generation-and-verification loop: the AI generates faster than humans can verify, so verification becomes the rate-limiting step, and the sane response is to keep the agent “on a leash,” with small tasks and fast ways to check the output. Good operational advice. But it leans on you being a fast, reliable verifier, and reading code is neither.

The trouble is that plausible-looking code is not correct code, and agents are extraordinarily good at plausible. A few data points have stuck with me:

These measure different things, and the GitClear trend reflects human habits as much as any agent’s, so don’t read them as one rising line. Read them as three faces of one tendency: agents optimize for output that looks done. Duplication instead of reuse. A confident import of a package that was never published. A function that compiles, passes the happy-path test, and quietly mishandles the empty list. None of these survive a careful reading, and none are caught by the skim-and-nod that diff review becomes at volume. That last row is comprehension debt in a quality costume: code that piles up instead of being refactored is code getting steadily harder to hold in one head.

So if reading code line by line is a weak and unscalable form of oversight, what’s the strong one? And here’s the question I’ll keep returning to: does the strong form give back any understanding, or only let us cope without it?

Reading the wrong altitude

A diff tells you what changed. It is silent on what must remain true, and “what must remain true” is what encodes your intent.

When you review a change by reading it, you reverse-engineer the author’s intent from the implementation, re-derive the spec in your head, then check the code against it. Reasonable enough once, for a change a colleague made with intent you broadly trust. Absurd a hundred times a day for code from a system that has no intent at all, only a very good model of what intent-shaped text looks like.

Sean Grove of OpenAI puts the constructive version well: code is a lossy projection of intent, and the durable artifact, the one worth writing carefully, is the specification of what the system should do and how you’ll know it’s right. On that view the spec, not the code, is the real source; the code is just a compiled, increasingly disposable output of it.

A spec is not just a checkable artifact, though. It’s the smallest honest statement of what you meant. If the implementation is the part you let go of, the spec is the theory you choose to keep: the human-held understanding that survives regeneration, the thing a person still reads, owns, and maintains. That’s the start of an answer to comprehension debt. Stop trying to hold every line in your head, and hold the much smaller statement of intent the lines are supposed to satisfy instead.

But notice what a checker buys you and what it does not. A verifier checks code against a spec; that is verification, and it can be made rigorous. Nothing in that loop checks that the spec matches what you actually meant. That second gap is validation, and no verifier touches it: point a perfect checker at the wrong spec and it will certify wrong code with total confidence. Microsoft researchers call this the intent-formalization problem and argue AI-generated code amplifies it to a scale software has never faced. So the spec carries the whole load: it is the one artifact a machine cannot validate for you, which is why it has to be the part a human still understands.

flowchart LR
  subgraph HUMAN[Human-held · nothing mechanical checks this]
      INTENT[Intent
what you actually meant]
  end
  subgraph MACHINE[Mechanically checkable]
      SPEC[Spec
what correct means]
      CODE[Implementation
the disposable output]
  end
  INTENT -->|validation · the unguarded gap| SPEC
  SPEC -->|verification · rigorous| CODE

The move is up the abstraction stack. Stop verifying the implementation by inspection; instead, state the properties it must satisfy and let something other than your tired eyes enforce them. Which raises the obvious question: what should that something be?

Properties, not examples

The first rung up from reading code is to change what a test even is.

A conventional unit test is an example: for input 2, expect 4. You supply both the input and the answer, and only a handful of them. Property-based testing (PBT) inverts this. Instead of examples, you state an invariant, something that should hold for all valid inputs, and let the framework generate the inputs:

• For all lists xs, reverse(reverse(xs)) equals xs.
• For all x, deserialize(serialize(x)) equals x.
• For any sequence of deposits and withdrawals that never overdraws, the ledger balance is never negative.

In real code it’s almost embarrassingly small. Say an agent hands you a my_sort and you want to trust it. In Python, with Hypothesis, the whole property is four lines:

from collections import Counter
from hypothesis import given, strategies as st

@given(st.lists(st.integers()))
def test_sort(xs):
    result = my_sort(xs)
    assert Counter(result) == Counter(xs)                   # same elements, nothing dropped or invented
    assert all(a <= b for a, b in zip(result, result[1:]))  # and actually in order

You never wrote a single example. You stated what sorted means, the same elements in order, and handed input generation to the machine. Those two assertions are in fact a complete spec of sorting. But Hypothesis doesn’t prove they hold; it samples inputs and looks for a counterexample. A clean run is not a proof, just a far stronger test than any handful of examples. Point it at a my_sort that quietly drops duplicates and the framework hunts down a failure, then shrinks it to about the smallest input that still breaks the property: not some 10,000-element monster but something as small as [0, 0]. The minimal reproducer lands in your lap.

The idea predates the AI wave by a quarter-century: Koen Claessen and John Hughes introduced it with QuickCheck for Haskell in 2000, since ported to some forty languages. Hughes’ slogan is the one to remember: don’t write tests, generate them. And the war stories are the good kind: for Volvo, Hughes’ team translated thousands of pages of automotive spec into properties and surfaced over 200 issues, many of them contradictions in the specifications themselves.

This matters most when the author is an agent. A property is far more durable than any particular implementation. The agent can rewrite the function five times, switch algorithms, refactor the module, and reverse(reverse(xs)) == xs still pins down what “correct” means across every rewrite. The property is a stable, human-readable encoding of intent that survives infinite regeneration: the same theory you choose to keep, now in a form a machine can enforce. That is comprehension debt held in check, because you maintain the property, not the thousand lines beneath it. And the counterexample it produces is machine-actionable: a failure that reads “Rule 7 violated for seed 24, round 5” tells an agent exactly what’s wrong, closing a tight generate-check-repair loop.

It runs in both directions, too. Anthropic recently built an agent that infers properties from a target library’s code and docs, writes the Hypothesis tests, and runs them; pointed at over 100 of the most-downloaded Python packages, it surfaced genuine, reported bugs. Agents can write the properties, and properties can police the agents. There’s measured evidence the trade pays off, too: in one re-grading of LLM-written solutions, a fifth or more of the “passing” code violated a stated property once you checked against properties instead of standard unit tests (From Prompts to Properties, FSE 2025). But an agent-written property isn’t free correctness; in Anthropic’s study only about 56% of the raw bug reports held up until a ranking step. A human or a second checker still sits in the loop deciding what’s real. Properties raise the ceiling on what you can catch. They don’t take you out of the room.

A spectrum of rigor

Property-based testing is one technique among several, and it helps to see the whole landscape. The usual way to draw it is as a ladder of confidence, but that picture misleads. What actually varies from one technique to the next is two things: what the technique quantifies over (one input, a class of inputs, all inputs) and what it costs.

flowchart TB
  subgraph G1[Universal over an error class · about free]
      TYPES[Types
compile-time]
      ASSERT[Assertions
& contracts]
  end
  subgraph G2[Sound bug-finders · a hit is a real bug, a clean run proves nothing]
      PBT[Property-based
testing]
      FUZZ[Coverage-guided
fuzzing]
  end
  subgraph G3[Aimed at completeness · a pass covers every input]
      MC[Model
checking]
      PROOF[Formal
proof]
  end
  ASSERT -.->|rising authoring cost| PBT
  FUZZ -.->|rising authoring cost| MC

The arrow on that diagram is cost, not confidence, and the column that matters is the second one. Types give a universal guarantee over a whole class of errors at compile time: that is strong in kind, even though it’s the cheapest thing on the list. And fuzzing and PBT don’t cleanly rank against each other. Fuzzing finds deep bugs PBT never will because it doesn’t need you to know what you’re looking for; PBT encodes semantic invariants a fuzzer can’t express. They’re complementary, not ordered.

There is a real divide running through the list, though. PBT and fuzzing are sound bug-finders: when they report a counterexample, the bug is real, no false alarm. But they are incomplete; a clean run only means nothing turned up this time. Model checking and proof are aimed the other way, at completeness: a pass is meant to be a universal guarantee that the property holds for every input. That is the different thing the right end of the table buys you.

What ties all of these together, and what makes them worth reaching for when you don’t trust the author, is the nature of the verdict. A fuzzer either crashes the program or it doesn’t; a model checker either reaches a bad state or shows it can’t; a proof checker either accepts the proof or rejects it. You cannot write a more confident comment, name a variable more reassuringly, or append # this is correct to move the answer, because the verdict is grounded in execution or proof rather than in how persuasively the code argues for itself. That relocation of trust is what pays down comprehension debt: you stop asking “do I believe the author understood this?” and start asking “do I believe this one tiny, auditable tool?” The tool isn’t infallible, but when it’s wrong the failure lives in one small place you can scrutinize, which is exactly why you keep it small.

These techniques are not academic toys. Google’s OSS-Fuzz, which needs only a harness rather than a spec, had by mid-2025 helped fix over 13,000 vulnerabilities and 50,000 bugs across more than 1,000 projects. AWS has applied TLA+ model checking to around ten large systems, finding DynamoDB replication bugs that needed failure traces as deep as 35 steps, well past anything design review and testing had caught. At the far end, the seL4 microkernel carries a machine-checked proof that its ~8,700 lines of C implement their specification, and CompCert is a production C compiler proved not to miscompile.

What’s changed lately is who writes the inputs to these tools, and the pattern across recent research is the same: let the model over-generate candidates, then let an execution-grounded checker throw out the ones that don’t hold. Point an LLM at a loop, have it guess invariants, and keep only the ones an SMT solver certifies, and you can discharge most of a standard invariant benchmark (Loopy); aim a similar loop at Rust verification and it proves more than 90% of a curated Verus suite. The model is the cheap, creative, untrusted part; the checker is the part you believe, and you believe it because it’s small enough to be worth trusting. The proof end has moved fast, too: automated provers now close most of the miniF2F benchmark and DeepMind’s AlphaProof reached silver-medal IMO performance. But read those results carefully: they hold the specification fixed and measure proof search, which was always the cheap part. The hard, unautomated work is writing a spec that captures what you meant, and the benchmarks say almost nothing about it.

So what does this mean for an ordinary product team? Not reaching for proof assistants. The practical stack is mostly the cheap end: types and assertions everywhere, property tests for the handful of core invariants you can actually state, fuzzing for parsers and other input-heavy surfaces, deterministic replay where you have distributed state to pin down, and formal methods reserved for the small, high-stakes core where a bug is catastrophic. The discipline isn’t using all of it. It’s matching the rung to the stakes, and being honest that most code sits near the bottom.

Determinism: making bugs reproducible

The techniques above leave one failure mode unaddressed: the bug that only shows up one run in a million, under a particular interleaving you can never quite reproduce. At agent scale, where flaky tests get re-run until green, these are poison. A test you can’t reproduce is worthless as a trust signal, and useless as something an agent can repair against, since it can’t reliably see the failure twice. Determinism is the fix, but be clear about what it is: testing infrastructure. It buys reproducibility, which is what makes the generate-check-repair loop possible at all. “I can reproduce it” is not “I verified it,” so you still have to point the other techniques at it.

The most interesting answer comes from deterministic simulation testing. Before the team behind FoundationDB wrote their database, they wrote a deterministic simulation for it to run inside: a fake world where the network, disks, clocks, and thread scheduler were all software mocks driven by a single random seed, so any bug the simulator found could be replayed exactly by re-running its seed. But determinism on its own is a quiet world; it reproduces only the executions you happen to drive. So they sprinkled the code with fault-injection hooks (famously named BUGGIFY) and drove runs from randomized seeds biased toward partitions, crashes, and corruption. The determinism makes a found bug reproducible; the randomized runs go find it. And because simulated time is decoupled from wall-clock time, they could fast-forward through years of rare events in hours.

This has since hardened into a discipline. TigerBeetle’s simulator runs the real cluster code against stubbed-out clocks, network, and disk, with every bug reproducible from a (seed, commit) pair. And Antithesis, founded by FoundationDB alumni, built a deterministic hypervisor so any software can be run reproducibly, even down to one-in-a-million race conditions. The connection to agents is direct: in 2026 Antithesis shipped tooling that lets an agent call the platform, learn exactly what broke, and correct its own output, escalating to a human only when it can’t. Determinism doesn’t tell you the code is correct. It turns a found bug into something an agent can see twice and act on, rather than a Heisenbug that vanishes on the next run.

Who verifies the verifier?

There’s an obvious hole in all of this: if the agent writes its own tests, it can satisfy them without satisfying your intent. That’s worse than useless, because now a green checkmark vouches for the wrong thing.

This isn’t hypothetical. Under evaluation, frontier models have been caught editing the tests, reading the reference implementation, and otherwise gaming the score; in one Anthropic study, a model that had learned to game its rewards went on to sabotage the very code meant to catch its misbehavior around 12% of the time. But the structural version of the problem is worse than the adversarial one, because it shows up even without bad intent. A model writing a test tends to encode what the code does rather than what it should do, so its oracles track the implementation, bug and all. Take matched correct and buggy versions of the same program and ask LLM test generators to tell them apart, and the suites validate the bug up to 68% of the time, passing the broken code and rejecting the test that would have exposed it. The same failure reappears one rung up: ask a model for a formal spec and it describes the program’s behavior, not your intent, so a spec synthesized from buggy code is satisfied by that bug. A verifier the author controls, at any level, drifts toward rubber-stamping the author.

Independence is what’s actually doing the work. Verification scales on an asymmetry: checking should be cheaper than producing. But that only holds when the checker has something the generator can’t fake, an independent source of evidence, or a verdict it can’t see and rewrite. The reward-hacking spiked exactly when the model could see the full scoring function. The cleanest framing I know treats the generator as untrusted by assumption and asks whether a cheap, trusted checker plus a little scarce human attention can stay safe even against a generator actively trying to slip something past. Safety, on that view, is whether the author can subvert the check, not whether it bothered to today.

All of which points one way: the check has to live outside the generator’s reach. De Moura’s prescription is the cleanest model I’ve seen: a small trusted kernel, a few thousand lines, that does the checking, with the AI, the automation, and even the human guidance sitting outside the trust boundary. Keep the kernel small enough to audit by hand, then re-implement it in more than one language, so fooling it would mean fooling several independent checkers at once. This isn’t only theory: an independent Rust re-implementation of the Lean proof kernel once rejected a proof the official kernel had wrongly accepted. So a rule of thumb falls out. The agent can generate the property, the harness, the spec, the proof; that is the expensive, pattern-heavy authoring work it is good at. But whatever decides pass or fail must be something the agent can’t reach in and edit. Generation and judgment have to be separable.

flowchart LR
  subgraph OUT[Outside the boundary · fast, fallible, untrusted]
      AGENT[Agent
generates code, specs,
properties, proofs]
  end
  subgraph TCB[Trusted base · small, auditable, redundant]
      KERNEL[Checker / kernel
decides pass or fail]
  end
  AGENT -->|proposes| KERNEL
  KERNEL -->|reject, repair| AGENT
  KERNEL -->|accept| SHIP[Trusted result]

None of this is airtight, and independent test generators still miss a great deal. What you buy is a verdict from something small, sound, and beyond the author’s reach, so that its mistakes are at least honest ones, not the author grading its own paper.

The economics flip, if it flips

Formal methods have always worked. They stayed boxed into aerospace, medical, and defense for one reason: cost. The seL4 proof ran to more than 20 person-years, over two person-years of proof for every thousand lines of C. Nobody was going to spend that on a CRUD app.

But look at where the cost lived. Almost never the verifier. Proof checkers, model checkers, and fuzzers run cheaply, and have for years. The cost was the human authoring: writing the spec, building the harness, composing the proof script, encoding the TLA+. That’s the human-bottlenecked input at every rung of the ladder, and it’s precisely the work agents are suited to: structured, pattern-heavy generation against a known target. So here is the optimistic claim, stated as a conditional. If agents can drive the marginal cost of authoring specs, harnesses, and proofs toward zero, the whole cost-versus-confidence curve shifts down and to the right, and rigor that was economically irrational for ordinary software becomes routine.

But that “if” hides the catch from the last section. There are two different jobs an agent can do here, and they are not equally safe. When the agent writes a proof the kernel checks, the trust boundary holds: a bad proof gets rejected, and cheap proof-authoring is the win we want. When the agent writes the spec we then trust as the definition of correct, nothing downstream checks it against your intent. That’s the validation gap, and it’s where spec-gaming lives. So the cost of proof authoring can fall toward zero safely; the cost of spec authoring cannot, because a human has to stay in the loop deciding whether the spec says what they meant. The economics don’t vanish. They relocate, from implementing and proving, which agents can take, to specifying and reviewing the spec, which stays human.

The slice this fits, and the slice it doesn’t

I’ve made the optimistic case, so it would be dishonest to skip the objections. This approach fits a good deal less software than its enthusiasts imply.

Most code is disposable, and understanding is overrated for it. A throwaway script, a one-off migration, a glue endpoint you’ll delete next quarter: the theory of that code is worth nothing because there’s no future maintainer to hold it. Demanding a spec there is ceremony. Specs aren’t automatically more legible than code, either. A dense TLA+ or refinement spec can be harder to read than the implementation it constrains, so “write the spec” is not a free upgrade in human comprehension; sometimes it just moves the obscurity somewhere fewer people can read.

The deeper limit is the oracle problem. The clean cases in this essay (sorting, numerical routines checked against NumPy) are the easy minority: code with a crisp property you can state independently of the implementation. Most business logic has no such property. What is the spec for “this checkout flow feels right,” or for a thousand lines of tax rules that are the specification? For a large fraction of software, there’s no oracle cheaper than rebuilding the program, and verification has nothing to bite on. And specs rot. A spec that drifts from intent is just comprehension debt at a higher altitude: now you have two artifacts to keep honest, and a passing check that quietly certifies the wrong target. The technique earns its keep on the slice of software that has a checkable property, a long enough life to amortize the spec, and stakes high enough to justify it. That slice is real and growing. It is not all of software, and pretending otherwise is how the whole thing gets discredited.

Trust is not understanding

There’s a limit no amount of rigor removes, and it’s the one that matters most. Everything above buys trust: a way to believe code is correct without reading it. But trust and understanding come apart precisely when you can least afford it. A passing property tells you the code does the right thing on the cases it covers. It says nothing about why the code is shaped the way it is, which lines are load-bearing, or how it will break when the next change lands just outside the property’s envelope. Naur’s point bites here: the theory of the system, the thing you need to debug it at 3am or extend it without fear, was never built. Verification lets you ship without it, and what makes that dangerous is that a green checkmark feels like understanding. It licenses you to move on, and each time you do the gap widens, until you can run a system no living person comprehends. That is fine right up until it does something none of your properties anticipated, and there’s no theory in anyone’s head to reason from.

That gap is worth measuring, not just lamenting, because comprehension debt sounds like a slogan until you can point a number at it. A few crude gauges: the share of merged diffs no human on the team can explain a week later; the fraction of lines under no asserted property or spec at all; the count of modules whose only documentation is the test suite the agent also wrote. None is precise, but any of them, tracked over time, tells you whether the gap is widening. That gap, not the bug count, is the thing to watch.

Where this leaves us

I don’t think coding agents devalue the craft. I think they relocate it.

The scarce skill stops being the ability to produce a correct implementation by hand. It becomes two things. The first is saying, precisely and in a form a machine can check, what correct even means, then putting that check somewhere a fast, fallible author can’t sweet-talk it. The second, harder one, is deciding what you’ll still understand: which theory of the system is worth holding in a human head, written down as the spec, so the abundant, disposable code beneath it stays anchored to something a person actually grasps. The code becomes cheap. What stays expensive is the understanding you choose to keep, and the spec authoring and review that no kernel will do for you.

It’s the same lesson I keep meeting from other directions. I’ve argued before that the model is rarely the bottleneck; an agent lives or dies on the harness around it. Verifiability is the conscience of that harness: it decides whether cheap, fast generation adds up to something you can trust. But trust was always the easier half. The harder half is making sure that somewhere, in the spec if not in the code, a human still understands what the system is for. When the author can no longer be trusted on sight, you stop trusting authors and start trusting checkers. Just don’t mistake the checker’s verdict for understanding. It can tell you the code is right. It can’t tell you why, and it can’t hold the theory for you. That part is still the job.

Sources and further reading

The problem: volume, trust, and comprehension

• Peter Naur: Programming as Theory Building (1985). The real artifact is the theory in your head, not the code.
• Anthropic launches a code review tool to check the flood of AI-generated code. TechCrunch; the “>8 in 10 PRs” figure.
• Andrej Karpathy: Software Is Changing (Again). The generation and verification loop, and “keep AI on a leash.”
• Sean Grove (OpenAI): The New Code. “The spec is the new source code.”
• Leonardo de Moura: When AI Writes the World’s Software, Who Verifies It?. The trusted-kernel argument.
• Intent Formalization: A Grand Challenge for Reliable Coding (Microsoft Research, 2026). The gap between spec and intent.

Evidence on AI code quality

• Veracode 2025 GenAI Code Security Report. ~45% of generated code carried a vulnerability.
• Slopsquatting: how AI hallucinations fuel a new supply-chain attack. On the USENIX Security 2025 study “We Have a Package for You!”
• GitClear: AI Copilot Code Quality 2025. Duplication up, refactoring down across 211M lines.
• NIST CAISI / METR: AI models can cheat on evaluations. Reward hacking and test sabotage.
• Anthropic: emergent misalignment from reward hacking. The ~12% sabotage-of-oversight finding.

Property-based testing

• Claessen & Hughes: QuickCheck (ICFP 2000). The original paper.
• John Hughes: Testing the Hard Stuff and Staying Sane. Industrial PBT war stories (LevelDB, AUTOSAR/Volvo).
• Hypothesis (Python) and fast-check (TypeScript). Modern PBT frameworks.
• Anthropic: Property-Based Testing with Claude and the Agentic Property-Based Testing paper. Agents inferring and checking properties.
• From Prompts to Properties (FSE 2025). Unit-test evaluations overstate how correct generated code is.
• Validating LLM-Generated Programs with Metamorphic Prompt Testing. Catching bugs with no reference oracle.

The rigor spectrum: fuzzing, model checking, proof

• Google OSS-Fuzz. Coverage-guided fuzzing at scale.
• How Amazon Web Services Uses Formal Methods (CACM 2015). TLA+ on S3, DynamoDB, EBS.
• seL4: Formal Verification of an OS Kernel and Gernot Heiser on the economics.
• CompCert. A formally verified C compiler.

Agents plus formal methods: what works, and where it breaks

• Loopy: Finding Inductive Loop Invariants using LLMs (FMCAD 2024) and AutoVerus (OOPSLA 2025). The over-generate-then-verify pattern.
• Clover: Closed-Loop Verifiable Code Generation and AlphaVerus (ICML 2025). Codegen paired with a checker; AlphaVerus documents spec-gaming.
• Specify What? Enhancing Neural Specification Synthesis (IFM 2024). LLM specs infer intent, not behaviour: a spec from buggy code certifies the bug.
• A benchmark for vericoding (2025). Large-scale verified-codegen results; natural-language descriptions don’t help much.
• DeepSeek-Prover-V2 and AlphaProof (Nature 2025). Strong on competition math, far from push-button on hard or arbitrary code.

Oversight and independent verification

• Design choices made by LLM-based test generators prevent them from finding bugs and Do LLMs generate oracles capturing actual or expected behaviour?. The circular-oracle problem, measured.
• AI Control: Improving Safety Despite Intentional Subversion (ICML 2024). Untrusted generator, trusted checker, scarce human attention.
• Prover-Verifier Games Improve Legibility of LLM Outputs and On Scalable Oversight with Weak LLMs Judging Strong LLMs (NeurIPS 2024). Where the verify-beats-generate asymmetry holds.
• Large Language Models Cannot Self-Correct Reasoning Yet (ICLR 2024). The empirical floor under self-checking.

Deterministic simulation testing

• FoundationDB: testing through simulation and Will Wilson’s Strange Loop talk. The origin of “simulation before code.”
• TigerBeetle: the VOPR. DST in a production database.
• Antithesis: Is something bugging you? and Antithesis teaches AIs to correct their own output. The deterministic hypervisor, and the agent feedback loop.