# Three outside reviews of my TLA+ models

2026-10-17

This is the third part of the series that began with [Twelve days of TLA+ on my own tools](/blog/twelve-days-of-tla-plus) and continued in [Thirteen review rounds and one rollback](/blog/thirteen-review-rounds-and-one-rollback). Part 2 ended with five fix rounds of the first outside review still waiting. Since then all of them are done, two more outside reviews have read the models, and each review got its own fix sessions.

## What did the three reviews find?

Each review read packages of my TLA+ models together with the code they describe and the reports of earlier runs. Sonnet subagents then checked every claim against TLC and the real code before anything was fixed. A claim rated high was one where, in the reader's words, a TLC verdict or a fix might not hold for the real code. After the check I kept the high rating only for a silent loss that contradicts a general statement in one of my reports.

| Review | Claims | Confirmed | Refined | Refuted | Rated high before and after the check |
|---|---|---|---|---|---|
| 8 October, four packages | 68 | 39 | 29 | 0 | 33 before, 2 after |
| 15 October, six packages, 35 models | 49 | 35 | 14 | 0 | 20 before, 2 after |
| 16 October, six packages, 55 models | 37 | 24 | 13 | 0 | 10 before, 0 after |

The third review is the first with no claim left at the high rating. The two high claims of the second review were one mechanism that two readers found in different models. My log size check registered entries from one scan and checked the caller's own entry with a separate read, so two sync restores in that window could leave the entry unregistered while the check still printed PASS. The fix session made the check read the caller's entry from the same scan.

## Can the three rounds be compared?

Not as a quality trend. ChatGPT read the packages in all three rounds at its Ultra effort setting, but the model changed: Sol 6.1 read rounds 1 and 2, and Astra read round 3. The prompt for round 3 also asked the reader not to report a point from an earlier round again unless it could show that the fix fails or that the stated limit understates the problem. Fewer claims in round 3 can come from the different reader or from better code, and the narrower prompt may have cut repeats as well. The numbers do not tell which.

The steadier signal is that no review claim about the models was refuted in any round. Many claims held only in a narrower form or at a lower rating, but none was wrong outright.

## What changed between the reviews?

The last five fix sessions of the first review ran on 12 October. Three of them changed real behaviour. The send script now refuses a rescan package whose target already has send evidence in another rescan batch. When the log rotation tool loses its lock after writing its size approval, it now prints the dropped entries and exits with an error instead of saying that nothing was approved. The restore path of the archive tool checks its lock again before it writes, so it no longer overwrites another writer's change.

From 12 to 15 October I worked through a plan of 12 items before the second review. The first one found that some of my test scripts passed for the wrong reason. In the send test, 12 of 120 checks stayed green when the tool exited at once with an error, and 8 of 120 when it exited at once with a clean exit code. The test scripts now require proof that the tool actually ran. The last full mutation run so far, on the night of 12 to 13 October, caught 786 of 788 mutations in about 3 hours 45 minutes, and both survivors were faults in the mutations themselves: one was equivalent to the original code, and the other matched two places in its target file.

Models moved into a versioned library with a manifest of the code each one covers, and a drift check names every model whose covered code has changed since the model last ran. It started with 32 models and had 41 before the second review. A runner reruns every stored configuration and compares the verdict and the state count with the recorded ones.

## Did the new techniques find anything?

I tried three techniques that go beyond checking a model on its own. A liveness check asks whether something good eventually happens, not only whether something bad never does. It confirmed two known stuck states that only a human step clears: the pipeline lock after a hard crash, and the in-progress marker of a send after a crash or an uncertain send. I left both for a human to resolve.

State graph replay walked the lock model's state graph edge by edge against the real code. Across 5 502 edges it found no contradiction. In 465 edges the model allowed a write that the code refused, because the model is older than the code's later ownership check.

Trace validation went the other way. Real tools ran freely in parallel and wrote an event log, and TLC checked that each log was a behaviour of the model. Of 300 traces, 298 were accepted, one failed because of the test setup and one exposed a model step that was coarser than the code. The data stayed correct, so the fix went into a finer model and not into the code.

Two real bugs came from the same stretch. Parallel subagents share their parent session's id, so my plugin's hooks wrote the same state file at the same time. A replay against the real hook code showed one gate silently skipping its check in 20 of 300 rounds, and after the fix in 0 of 300. Batch import never finished an interrupted run: after three retries it stayed at 4 of 5 records, and now it resumes.

## How did the second and third fix rounds run?

The second review got seven fix sessions from 15 to 16 October, each in a fresh Claude Code session with Opus leading and Sonnet subagents doing the work, and the third got six on 17 October. In the third review the worst finding was in the send script. After the final dot that ends an SMTP message it treated a late 354 reply as a certain refusal, so a server that had already accepted the message and then sent that 354 made a retry send it a second time. A local fake server reproduced the double delivery. It now treats only 4xx and 5xx replies as a certain refusal and leaves anything else for me to resolve.

The chain of fix sessions also ran differently the third time. The app does not let a session start another session on a turn that a session report woke up, so in the second round each later session waited for my click. In the third round the coordinating session started the last four sessions at once on a turn of my own. The first began right away. Each of the other three waited in a background loop until the previous session had marked its row done in the shared plan, and only then read or wrote anything. After one stop of mine that a message from the coordinating session undid, the chain ran through without me, and a choice that only I could make no longer stopped it: the session took its own recommendation and listed it in a morning report for me to change.

Checking the 37 claims of the third review took 16 Sonnet subagents and about 3 100 000 tokens, against about 3 900 000 for the 49 claims of the second, counting subagent tokens only.

## What is still open?

The library now holds 88 models and 770 stored runs, and 56 of those models have drifted from the code they cover. A drifted model's PASS holds only for the version of the code it was run against, so each needs a fresh run before I rely on it.

The fix sessions of the second and third rounds ran only limited mutation runs. A full run has about 880 mutations now and takes roughly 3 to 4 hours, and it has not run since 13 October.

Each fix session also named limits it chose not to close. Before I close any of them I want a list sorted by cost and consequence. Some environments are unmeasured: a mail server that answers wrongly, how often my sync client restores files, a full disk and file symlinks, which this account cannot create. A fourth outside review makes sense only after the full mutation run and the drift runs, and with a reader other than Astra.

## What does this not show?

A confirmed claim shows that the reviewer described the code correctly. It does not show that the reviewers found everything, and three rounds by two models of one product family are a narrow sample. A model that passes holds for its small constants and for the code it was run against.

I made the counts in this post from my decision log, the review reports and the subagents' usage readings.

## Frequently asked

**Why did the number of high-rated claims fall to zero?**

I cannot say it was only better code. The third round had a different reader model and a prompt that asked it not to repeat earlier points without new evidence, so the three rounds are not a clean comparison.

**What is trace validation?**

The real tools run freely and log what they do, and TLC checks that every log is a behaviour the model allows. A rejected log means the model and the code disagree or the test setup is wrong, and in this project the one real rejection pointed to a model step that was coarser than the code.

**What is a drifted model?**

A model whose covered code has changed since its last run. Its stored PASS still describes the old code, so it needs a fresh run before it says anything about the code that runs today.

## Related

- [Twelve days of TLA+ on my own tools](/blog/twelve-days-of-tla-plus)
- [Thirteen review rounds and one rollback](/blog/thirteen-review-rounds-and-one-rollback)
- [The checks that pass for the wrong reason](/blog/checks-that-pass-for-the-wrong-reason)