AI verification debt: why cheap proofs move the bottleneck to the spec

What verification debt is

Technical debt is code you will have to rework. Verification debt is code nobody has checked against what it was supposed to do. It accrues every time an agent's output merges on a green build that nobody can vouch for, and it compounds, because the next change is built on top of it. The verification bottleneck is no longer writing tests. Agents write those too. It is knowing whether any of it, code or tests, matches what the business meant.

Proofs look like the way out. They move the debt instead.

The strongest answer on offer is formal verification, and it just got dramatically cheaper. Anthropic's Frontier Red Team and Theorem used Claude to prove 239 fuzz entry points across 123 open-source libraries crash-free for every input under 64 MB (Anthropic, 2026-10-22, verified 2026-10-23). Use it for what it proves.

Then read what it took. The team needed a spec, and "The difficulty of obtaining a comprehensive and unambiguous spec is a significant obstacle to verifying software at a larger scale". They converted the libraries' existing tests into one. Their own limit: "a proof checker can’t tell you whether your spec matches reality". Mike Dodds of Galois saw it coming. With cheap proofs, he wrote, “we will quickly verify every compiler and microkernel, then find that we’re stuck.” The reason: “we don’t have a formal specification for Chrome, or a word processor” (Specifications Don't Exist, 2025-06-16, verified 2026-10-23).

A proof pays down the debt between the code and the spec. It moves everything else onto the spec. In business software, that is where the debt was all along. More on what the proofs cover in our guide to AI formal verification, and the news itself in Claude proved 123 libraries crash-free.

Where verification debt hides in business software

In business software the spec is the requirements, the acceptance tests and the business rules. AI now writes all three, so the debt hides in four places:

1. Requirements nobody reviewed. An agent drafts a requirement, a rule or a test's intent, and it merges. Nothing in the build tells you which of them a human ever read.
2. Tests too weak to notice. A suite can run every endpoint and assert almost nothing. When tests become the spec, their strength is the ceiling on every claim built on them. In a companion experiment on a verified interpreter, the same team measured the gap: "we deliberately injected seven bugs … Five survived the random tests, while all seven broke the proof".
3. Greens bought by refusal. A check can turn green because the code started refusing more input or because the assertion was rewritten. The proof team hit the same move from the other side: "Claude could make any theorem provable by rewriting the program into one that trivially never crashes".
4. Meaning that drifted under a green suite. Tests that ask the rules what to expect change when the rules change, and stay green while the answer moves.

Paying it down: a governed spec chain and a review gate

More proofs do not pay down verification debt in business software. A governed spec chain does, with a gate on what nobody has reviewed. Karate Agent does this in one git-native graph your agent drives and a human audits:

• Requirements joined to evidence. The traceability matrix is computed from what actually ran, and every item is graded exercised, partly exercised, incidental or not exercised, so a requirement that looks tested but never ran is named.
• AI claims read as AI claims. When an AI run ticks off a requirement, the report shows it as an AI claim, graded below captured evidence. An agent never quietly marks its own work verified.
• The review ledger. Roadmap Every requirement, rule and test an AI authored stays marked review-pending until a human approves it in a reviewing commit. The report counts what is still unreviewed, and unreviewed high-criticality work blocks the release. AI-written theorem statements join the same ledger.
• Rules as the oracle. The business rules are executable and compute every expected answer, so a test's expectation comes from the rule the business signed, not from what the code happened to return. A violated guarantee blocks the release with the breaking input attached. Business rules testing →
• Tests graded by mutation. Defects are seeded into the rules, the lifecycle model or the live responses; your suite replays; survivors come back naming the requirement nobody defends. Assertions copied from observed output cannot inflate the score. API mutation testing →
• Greens bought by refusal, named. Roadmap A guarantee that turned green by refusing more input, or by rewriting what it asserts, is reported and never credited.
• Drift caught under green. The meaning of every rule is diffed against a baseline a human blessed.
• Proofs carried, not trusted blind. Today TLC results land on the requirement they argue for. Roadmap Rocq, Lean, Verus and Dafny results land bound to the theorem and the code they were about, with the prover's assumptions report verbatim, and stop counting when either moves.

The verdict at the end is computed by versioned code, with no model in the path: READY, CONDITIONAL or NOT READY, blockers named. How the release verdict works → For the wider picture, see testing AI-generated code.

A verification-debt audit you can run this week

1. List your top 20 requirements and, for each, the test evidence that actually exercised it. Count the ones with none.
2. Run mutation testing on your most important suite. Count the survivors.
3. Count the requirements, rules and tests an AI wrote that no human has reviewed.
4. For each business-rule guarantee, ask: was it checked over the whole declared input domain, or over a sample? Write down which.
5. For each proof you hold, write down the theorem statement, who reviewed it, and the commit of the code it was about.

Every blank on that list is verification debt. Karate turns the list into a report that recomputes on every commit.