Tests or formal verification when AI agents write code

To find out whether a bridge is safe, you have two options. Drive a truck across it: the real bridge gets tested, but only with the trucks that crossed. Or do the calculations on the drawings: every load gets considered, but only on paper, and the builders may not have followed the drawings. Testing is like the first. Formal verification is like the second. This lesson compares the two, then answers how to divide them when agents write most of the code.

The short answer: they catch different bugs, so do not pick one. Choose by risk, and always check whether the check itself can go red.

Try it: same bug, what do three kinds of check see?#

The demo below has one small save flow and six ways to get it wrong, simplified from real bugs. Three kinds of check really run in your browser. Click a cell to see the path to the bug.

Try this order:

1. Switch nothing on. Only "Saves an old copy" gets caught, 3 of 18 cells. Six bugs are sitting there, and nearly every check is green.
2. Switch on Reads or writes can fail. That goes up to 6 of 18. Look at "Second read after a failure": random tests catch it and the model misses it. Tests run the real code, while the model follows the description its author believes, with one read.
3. Switch on The model reads as often as the code. The model catches it at once. The tool did not change, the description just got more accurate.
4. Switch on A rule: unsaved work shows a notice. "Unsaved with no notice" goes to caught in all three columns. Before that no check saw it, because nobody had written the rule.
5. Switch on the other two: 14 of 18. The four cells still missed are all example tests, because nobody wrote a scenario for those bugs.
6. Drop the random runs to 5 and change the seed a few times. Sometimes random testing misses up to three bugs. With 50 runs, all three seeds we tried caught them all. The model does not depend on luck like that, within what it describes.

What does each kind of check prove, and what does it miss?#

Each answers a different question, and none answers both "does the real code work" and "has every case been considered".

One point is easy to mix up: model checking and proof are both formal verification, but they differ in an important way. TLA+ usually checks a description of the system, so the real code is still unchecked. Dafny or Lean can prove things about the code itself, at a much higher cost in effort.

What does evidence from elsewhere say?#

The studies below are much bigger than our experience, and they mostly show formal verification has real value, stopping exactly at its border.

• AWS has used TLA+ since 2011. The 2015 paper describes models finding design bugs in S3, DynamoDB and EBS, some needing a 35-step trace to show. It also says engineers learned it and got results in 2 to 3 weeks. The same paper states two limits: at the time they knew of no tool that could check code against the spec at their scale, and formal specification does not suit sustained performance degradation.
• Proved systems still have bugs, at the border. Fonseca et al. found 16 bugs in three formally verified distributed systems, 11 of them in the shim layer connecting proved code to the operating system. They found none in the protocol parts, while unverified systems had many of that kind. They found those bugs by reading code and testing.
• A proved compiler, the same. When they ran Csmith on CompCert for about six CPU-years, the authors found no middle-end wrong-code bugs, where every other compiler had them. The bugs they did find were in unproved parts.
• Coverage is not a measure of quality. Inozemtseva and Holmes found only a low to moderate correlation between coverage and catching bugs once the number of tests is controlled for.
• Property testing helps, and it is hard to know when it is enough. A study at Jane Street, from 30 interviews, shows developers value the method, yet struggle with writing data generators and with judging whether tests are effective. It is qualitative work at one company.

Why is a green check not enough to trust?#

Because green only means something if the check is able to go red. The test is simple: put the bug back, or remove the guard, and see if the check goes red. Doing this systematically is mutation testing, and Google has run it with more than 24,000 developers, during code review.

This matters more when agents write the tests. A controlled experiment on 24 Java repositories found that LLM-generated tests mostly record what the code does now, rather than what it should do, which makes bugs hard to catch. In the other direction, Meta's ACH system uses simulated faults to steer an LLM's test writing, and engineers accepted 73% of those tests in its trial events.

In our own trial, a test of "opening the app many times makes one backup" could not fail: the launches landed in the same millisecond, so they collapsed into one key. It was green for the wrong reason, and that only came out by asking why it was not red.

What did our small trial show?#

It showed that independent review with a reproducing command still found real bugs after the models and tests were green, but this evidence is weak. It started from a post by Lauren Tan (@poteto) on 3 November 2026, arguing that adversarial reviews are mostly a waste of tokens, better spent on empirical testing combined with formal verification. The author's interrogate skill also keeps only findings a run proves. We tried this on the progress storage of LexiLoop, ChabuLab's vocabulary app. That repository is private, so you cannot check the numbers below yourself.

The process: write the rules, write TLA+ models and tests, see them go red with a guard removed, then fix. After each fix, a reviewer on a different model tried to break the code and had to give a reproducing command. Six rounds, in about three hours:

Each round ran after the author's own checks were green: 154 tests passing in round 2, 159 in round 3, 162 in round 4. On 4 November 2026 we reran the final version: 169 tests, 899,377 assertions, and three models passing with 18, 26 and 4,840 states. Removing the guard in the largest model made TLC report a violation after only 23 states.

Two things worth remembering:

• The model shared the author's mistake. Round 3 found a bug where the code read twice and the model had one read. The model was green because it described the code the author thought they had written. The fix was to make the code match the model, and to add a test that fails each storage call.
• Running it changed the priorities. The model said a double press could erase progress, yet in a real run a double-click fired one press. Meanwhile one tap on "Learned" erased ten correct answers, a bug an earlier review had ranked lowest.

Where is this evidence weak?#

Do not use it as a general conclusion, for these reasons:

• A very small sample. One project, one person, one evening, one part of the code. No control group.
• The project owner's objection. Perhaps review found bugs because the formal verification before it was not good enough: the models were new, and failed reads were not in them at first. This trial cannot separate "review catches what formal verification cannot" from "the formal verification here was weak".
• Every fix adds new code. Four of the first five rounds caught a bug from the previous fix, so bug counts do not measure the starting quality.
• A clean round 6 does not prove there are no more bugs. It only says one free model found none. The reviewers did not all use the same model either.
• Token cost was not measured, so we cannot say which approach is cheaper.
• What was not checked. Android, real taps on an iPhone, and real storage failures from the operating system. Storage failures in the tests are all simulated.

What we take from it goes this far: for changes to user data, we keep one independent reviewer, and every finding must come with a reproducing command.

About agents, what is measured and what is only predicted?#

Writing proofs on benchmarks is measured and rising. Agents beating people across the whole job has not been measured by anyone.

What follows is our reasoning, with no measurement behind it. Suppose agents really do write code and proofs better than people:

• The cost changes, the question does not. Kleppmann also points out that when proofs get cheap, the hard part moves to the specification: are the properties you proved the ones you needed?
• The border stays. The bugs in the Fonseca study sat in assumptions about the unproved parts. Real disks, networks and browsers do not prove themselves, so running things still matters.
• Same author, same blind spot. When one agent writes the code, the tests and the model, they easily share a wrong assumption. Being smarter does not remove that by itself. An independent party, or making checks go red, does.
• "Correct" is a choice. Should deleting a marker delete its notes? No tool can answer until someone decides.

If evidence appears against this, this section should be rewritten.

How should you divide the two kinds of check?#

Choose by risk, and do not run everything on every change. This is our recommendation, based on the sources above and one project of ours, not a proven result.

For risky changes, the process we use now is:

What do people keep?#

In our view, the parts where someone answers for the result, even if agents do the rest better. This is an opinion, not a measurement.

• Deciding what counts as correct. On LexiLoop, two tabs saving within the same 1 to 2 milliseconds can lose one answer. We accepted that, because one person does not answer that fast, and locking every save opens a different risk when a tab closes. A reviewer found the bug, but no check could make that decision.
• Choosing how much to invest. Proving a whole vocabulary app is wasteful. Not proving the core of a payment system may not be.
• What needs real experience. Taps on a real phone, reading the words, feeling the pace of the interface.
• Reading results with suspicion. Asking "what does this check not cover?" after every green.

Run a small model checker yourself#

The code below needs Node 22.18 or later and no outside libraries. Save it as lost-update.ts and run node lost-update.ts. It is a complete model checker for two tabs overwriting each other. It puts a sequential test, a random test and a walk of every state side by side.

// lost-update.ts: node lost-update.ts
// Two tabs add to one stored number. Each save reads, then writes.
type State = { disk: number; tabs: { read: number | null; done: number }[] };
type Step = { tab: number; kind: "read" | "write" };

const ANSWERS_PER_TAB = 2;

function steps(s: State): Step[] {
  return s.tabs.flatMap((t, tab): Step[] => {
    if (t.read !== null) return [{ tab, kind: "write" }];
    return t.done < ANSWERS_PER_TAB ? [{ tab, kind: "read" }] : [];
  });
}

function apply(s: State, { tab, kind }: Step): State {
  const next: State = structuredClone(s);
  const t = next.tabs[tab]!;
  if (kind === "read") t.read = s.disk;
  else {
    next.disk = t.read! + 1;
    t.read = null;
    t.done += 1;
  }
  return next;
}

// The rule: when no tab is mid-save, every answer is stored.
const holds = (s: State) =>
  s.tabs.some((t) => t.read !== null) || s.disk === s.tabs[0]!.done + s.tabs[1]!.done;

const start: State = { disk: 0, tabs: [{ read: null, done: 0 }, { read: null, done: 0 }] };

// The model checker: every reachable state, breadth first, so the path found is a shortest one.
function check(): { states: number; path: Step[] | null } {
  const seen = new Set([JSON.stringify(start)]);
  let frontier = [{ state: start, path: [] as Step[] }];
  while (frontier.length > 0) {
    const next: typeof frontier = [];
    for (const { state, path } of frontier) {
      for (const step of steps(state)) {
        const after = apply(state, step);
        const key = JSON.stringify(after);
        if (seen.has(key)) continue;
        seen.add(key);
        const trail = [...path, step];
        if (!holds(after)) return { states: seen.size, path: trail };
        next.push({ state: after, path: trail });
      }
    }
    frontier = next;
  }
  return { states: seen.size, path: null };
}

// A test the way it is usually written: one tab saves fully, then the other.
function sequentialTest(): boolean {
  let s = start;
  for (const tab of [0, 1, 0, 1]) {
    s = apply(apply(s, { tab, kind: "read" }), { tab, kind: "write" });
  }
  return holds(s);
}

// A random test: the same steps in a random order, repeated.
function randomTest(runs: number): number {
  let failures = 0;
  for (let run = 0; run < runs; run++) {
    let s = start;
    for (let options = steps(s); options.length > 0; options = steps(s)) {
      s = apply(s, options[Math.floor(Math.random() * options.length)]!);
      if (!holds(s)) {
        failures += 1;
        break;
      }
    }
  }
  return failures;
}

const { states, path } = check();
console.log("sequential test passes:", sequentialTest());
console.log("random test failures in 1000 runs:", randomTest(1000));
console.log("model states visited:", states);
console.log("shortest path:", path?.map((p) => `tab${p.tab} ${p.kind}`).join(", "));

On 4 November 2026, on Node 26.11.1, the result was:

sequential test passes: true
random test failures in 1000 runs: 825
model states visited: 17
shortest path: tab0 read, tab1 read, tab0 write, tab1 write

The sequential test is green despite the bug, because it never lets two tabs overlap. The second line is random, so your number will differ a little. Another run of ours gave 804. Change apply so reading and writing happen in one step, and run it again to see the bug go away.

How do you run real TLA+?#

Follow the six steps below, about ten minutes. The code here is not Java but TLA+, a language for describing a system, and it does not run in any product. The checking tool is called TLC. TLC is written in Java, so you need Java only to run TLC.

Step 1: install Java 11 or later. Run java -version first. If your machine has no such command, or the first number is below 11, open the guide:

winget install EclipseAdoptium.Temurin.21.JDK

brew install --cask temurin@21

sudo apt update
sudo apt install -y default-jre-headless

java -version

Step 2: make an empty folder. These commands are the same on all three systems:

mkdir tla-demo
cd tla-demo

Step 3: save two files in that folder. The names must match exactly. The first is LostUpdate.tla:

---- MODULE LostUpdate ----
\* Two tabs add to one stored number. Each save reads, then writes.
EXTENDS Integers
CONSTANTS Tabs, Answers
VARIABLES disk, read, done

Init == disk = 0 /\ read = [t \in Tabs |-> -1] /\ done = [t \in Tabs |-> 0]

Read(t) ==
  /\ read[t] = -1 /\ done[t] < Answers
  /\ read' = [read EXCEPT ![t] = disk]
  /\ UNCHANGED <<disk, done>>

Write(t) ==
  /\ read[t] # -1
  /\ disk' = read[t] + 1
  /\ read' = [read EXCEPT ![t] = -1]
  /\ done' = [done EXCEPT ![t] = @ + 1]

Next == \E t \in Tabs : Read(t) \/ Write(t)

\* The rule: when no tab is mid-save, every answer is stored.
RECURSIVE Sum(_)
Sum(S) == IF S = {} THEN 0 ELSE LET t == CHOOSE x \in S : TRUE IN done[t] + Sum(S \ {t})
NothingLost == (\E t \in Tabs : read[t] # -1) \/ disk = Sum(Tabs)
====

The second is LostUpdate.cfg. It tells TLC how many tabs and answers to use, and which rule to check:

CONSTANTS
  Tabs = {t1, t2}
  Answers = 2
INIT Init
NEXT Next
INVARIANT NothingLost

Step 4: download TLC. It is one file of about 2.3 MB. On Windows, in PowerShell, type curl.exe instead of curl.

curl -LO https://github.com/tlaplus/tlaplus/releases/download/v1.7.4/tla2tools.jar

Step 5: run it.

java -cp tla2tools.jar tlc2.TLC -deadlock LostUpdate

TLC reports the broken rule and prints the path to it. With TLC 2.19 the main part looks like this, with the states in the middle left out:

Error: Invariant NothingLost is violated.
Error: The behavior up to this point is:
State 1: <Initial predicate>
/\ done = (t1 :> 0 @@ t2 :> 0)
/\ read = (t1 :> -1 @@ t2 :> -1)
/\ disk = 0
State 2: <Read line 10, col 3 to line 12, col 29 of module LostUpdate>
...
State 5: <Write line 15, col 3 to line 18, col 39 of module LostUpdate>
/\ done = (t1 :> 1 @@ t2 :> 1)
/\ read = (t1 :> -1 @@ t2 :> -1)
/\ disk = 1

Read from the top: both tabs read disk = 0, then each writes 1. The last lines show done at one answer per tab, two in total, yet disk holds 1. That is the lost answer. TLC also creates a states folder, which you can delete.

Step 6: fix the bug and run again. In LostUpdate.tla, replace the Next line with the block below, so reading and writing happen in one step. Then run the command from step 5 again.

Save(t) ==
  /\ done[t] < Answers
  /\ disk' = disk + 1
  /\ done' = [done EXCEPT ![t] = @ + 1]
  /\ UNCHANGED read

Next == \E t \in Tabs : Save(t)

TLC visits 9 states and reports:

Model checking completed. No error has been found.

Now remember what this lesson said: this green is only about this description. Whether your real code reads and writes in one step is something TLC cannot know.

If you get an error:

We ran these steps on 4 November 2026 with TLC 2.19, on a clean Ubuntu 24.04 with Java 21 and on macOS with OpenJDK 25.

Common mistakes#

• Treating green as done. Add one line: what this green does not cover.
• Letting one agent write code, tests and model, then trusting all three. Make each check go red once, and use an independent party for the risky parts.
• One read in the model, two in the code. Each model step must point at real code, with the same reads and writes.
• Believing a model's bug path right away. Replay it with real input before ranking how serious it is.
• Chasing 100% coverage. Coverage shows what is untested, not whether the tests are good.
• Review with no command to run. A finding nobody can reproduce should be marked unproven.
• Using formal verification for everything. It does nothing for performance or look and feel, and costs effort on low-risk parts.

How do you hand this to an AI?#

Copy the text below, fill in the blanks and give it to an agent:

Change: [describe the change]
Risk: [user data, money, concurrency, interface, ...]

Before or while coding:
1. Write down the rules this change must keep, in plain words. Stop for my approval on any rule that needs my decision.
2. For each rule, pick a check that fits: property or exhaustive tests for pure logic; model checking for retries, races, saves and undo; E2E for user flows.
3. If you use a model: each step must point at real code, with the same number of reads and writes.

Before reporting done:
4. For each check, put the bug back or remove the guard, show me it going red, then restore it.
5. Replay every bug path from a model with real input. If it does not reproduce, say so.
6. Start the report with the commands run and their output, then the summary.
7. Add one line: what these checks do NOT cover.
8. List any limits you propose accepting and why, so I can decide.

A finding with no reproducing command is marked unproven, and starts no fix.