TLA+ on my own tools, in numbers

2026-10-22

This is the fourth and last part of the series that began with Twelve days of TLA+ on my own tools, continued in Thirteen review rounds and one rollback and went on with Three outside reviews of my TLA+ models. It closes the series with the full numbers. Part 3 set a condition for a fourth outside review, and I did not keep it, so that comes up below too.

How long did the work run?

The first pilot started on 27 September and this post is written on 22 October, 25 days later. The table lists the stretches that carried the work.

How big did the model library get?

The library is a versioned folder of models with a manifest of the code each model covers. A drifted model is one whose covered code has changed since the model last ran, so its stored PASS describes older code.

The 116 models are 105 valid, 4 replaced by later models and 7 marked historical. Their registry holds 880 stored runs: 351 pass runs, 394 vacuity runs and 135 liveness runs. A vacuity check shows that a property can fail at all. Drift grew again as the fix chain of the fourth review changed code, which is why 79 models had drifted by the audit. The acknowledgement of 17 October and the one of 22 October use different definitions, and the audit section explains why.

What real faults did the work find?

This is a selection. It has 14 rows, one of them four separate causes, across 11 tools or tool groups. Some came from the outside readers and the audit. Each either happened in real use or was reproduced against real code or a test copy of it, and not only in a model. Every fix chain also named smaller limits that are not in the table.

I count a fault only when it happened in the unchanged tool or was reproduced against it. A model's counterexample alone does not count.

What did the four outside reviews find?

Each review read packages of models together with the code they describe. Sonnet subagents checked every claim against TLC and the real code. A claim was rated high when, in the reader's words, a 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.

Rounds 1 and 2 were read by Sol 6.1 and round 3 by Astra, all through ChatGPT at its Ultra effort setting. Round 4 was read by Opus 5.5, and I chose the reader and handed over the packages by hand. Opus 5.5 also led the fix work, so round 4 was not read by a model from outside the family that wrote the fixes.

The falling number of high-rated claims cannot be read as a quality trend, because the reader changed between rounds and the prompt changed after round 2. All four rounds also share one limit that the internal audit named: no claim was refuted in 189, and I never planted a false claim to see whether the method would refute it. The verifiers are the same model family as the implementers. Zero refuted therefore says little about the method.

What did the internal audit of 19 October find?

I asked for an internal audit, because I needed to be able to trust the decisions. Eight Sonnet reviewers read and did not run anything. They covered 85 distinct decisions and the questions of the four outside reviews, in eight tool families. For each decision they checked the code on disk, the test and mutation protection, the evidence, the model and its drift, and the status line.

The audit gave 116 verdict rows. The decision held in 36 rows, held while its model had drifted in 60 rows and needed refining in 20. In none did it fail to hold, and in none was it impossible to check. The refinements were nearly always an outdated status line or a moved line number. A few were a sentence that a later decision had overruled.

Three structural findings came out of it.

The acknowledgement by re-run could not fail. A TLC run checks the model, and the model does not read the code. On 17 October I had acknowledged 39 of 56 drifted models by reading the diff and re-running 508 stored runs with no deviation. The re-run added nothing, because it could only pass. Of the 111 valid models, 79 had drifted. A classification of the diffs gave 16 comment-only drifts, 60 with real code changes after the last run and 3 without a recorded hash. The gotchas log had noted this problem on 16 October, but the code, the skill and one decision still said "by re-run".

The mutation suite had not run whole for six days. On 13 October the last full run caught 786 of 788, and 110 mutations had been added since without a full run.

Third came the finding about zero refuted claims, described above.

The audit also found eight code issues, and I confirmed six of them on disk. One of them was the late 4xx or 5xx reply in the send script.

The full mutation run of the audit caught 896 of 898, and the two survivors were a classification error and not a hole in the protection. Each of two mutations of the model library tool was expected to turn one named test red, and each also turned red a control test that was defined to stay green. The fix added that control to the expected-red lists of both mutations.

Did the fixes have to be redone?

On 21 October I wrote that so much had changed in the workspace that the whole fix plan probably had to be redone. Three Sonnet subagents measured it. Of the 41 covered files, 8 had changed since the last fix. For three of them I measured the diff and none touched a fixed spot. For the other five I inferred it from the changelog and the file times, because no comparison copy existed. The checks covering them were green. Five limited mutation runs passed with 7 of 7, 25 of 25, 87 of 87, 79 of 79 and 71 of 71, and a full run passed 936 of 936. The suspicion did not hold when I measured it. One caveat stays: that full run used an older version of the mutation file, and the 24 mutations added after it ran only in limited mode.

What did the full mutation runs show?

A mutation changes one line of a tool. It counts as caught when the test named for it fails and the control tests stay green. A full run applies every mutation of the tools suite.

Serial, the 1 002 mutations would take about 7 hours at the rate of the 936. The 48 parts took 64 minutes, so the run is about 6 and a half times faster. The machine has 32 logical processors and 48 GB of memory. During the run the processor averaged about 86 percent, memory about 56 percent and peaked at about 61 percent, with at most 199 node processes. The baseline of 249 named cases ran 1 086 times in the parts and the parent, and one run was red, a baseline case under load. Four mutations were run again alone and all four were caught alone.

The plugin's hook gates have a mutation suite of their own, which I do not add to this table. It caught 643 of 643 on 12 October and 828 of 828 on 22 October. The second run took 927 seconds as three parts, alone, because its timing tests fail under load.

A full run is now weekly. A scheduled task created on 22 October runs it on Sunday nights, and its first run is on 25 October. The export gate for outside review packages refuses a package unless the stored result of a full run passed at most 7 days earlier. If the tools have changed since that run, it only prints a note.

What did it cost?

For this work I have only subagent tokens, and only for some steps. These are the figures for the main steps. A few more exist for single steps, and I left them out.

The review 1 figure leaves out its 22 QA agents, which have no figure, and 2 baseline check agents with 248 981 tokens. In the review 4 fix chain I summed the figures of two sessions from their item rows. The audit used 8 subagents and the re-evaluation 3. On the night of 22 October the three fix sessions used 6, 6 and 11 subagents, and the next one about 6.

I have not totalled the lead model's tokens or the money for this work, and the transcripts could give both. Subagent tokens are missing for the pilot and the six phases after it, the second and third fix chains, the audit, the re-evaluation and the fix sessions of 22 October. I have not counted the cost of the outside readers or the number of Claude Code sessions either, and neither is the cost of the aborted runs.

What went wrong?

I picked five problems that taught me something.

• The acknowledgement by re-run could not fail. I had written the problem down on 16 October. The acknowledgement of 17 October rested on reading the diffs, but the tool, the skill and one decision still said re-run. The audit found that two days later.
• A replay script overwrote the real log size registry with test data on 18 October and reset its recorded size peaks. The audit later confirmed that the test keys were still in the file. A guard now refuses writes to the real workspace from a test process.
• Mutation parts ran into a limit. A run in 96 parts gave Windows a system error about stack guard pages, so the limit is now 48. An earlier serial run by another session ran about 16 hours before I stopped it, at about 140 W for about 14 hours, and the cause was never found.
• A diff reader proposed acknowledging a model because the code had later implemented the name of a mode the model only imagined, although the reader itself listed three differences. A name does not acknowledge a model. A counter-checker also argued for acknowledging it, with reasoning that held for one of the model's five pass runs. I read the runs and kept the model drifted.
• Four parallel readers shared one scratchpad and one reader's script overwrote another's. The decisive numbers came from run outputs, so I did not measure any damage.

Did the condition of part 3 hold?

Part 3 said that a fourth outside review makes sense only after the full mutation run and the drift runs, and with a reader other than Astra. I chose acknowledgement first and left the full run for later. A session built the packages of the fourth review on 17 October with 39 of 56 drifted models acknowledged and 17 not, and the full run came on 19 October. The condition did not hold, because the review ran before the full run, and the acknowledgement behind those 39 was later found unable to fail as well.

The corrected rule is in the tools now. No fifth review is planned, and a package for one needs a passing full run at most 7 days old.

What is still open?

Seven models are still drifted, in three families. Five belong to the tag release family: the tag layer was rewritten and the fresh-tag readback is not in those models. One is a send model whose own correction says it describes code from before the late-reply fix, and the corrected mode lives in another model. One is the hand-log model, whose code gained two paths the model does not describe. The choice between a refinement check and the status historical is mine and I have not made it.

Several environments are unmeasured. They are a mail server that answers wrongly, which only the scripted replies of my fake server cover, how often my sync client restores files, a full disk and file symlinks, which this account cannot create. The send reservation also rests on two assumptions I have not measured: that creating a file exclusively is atomic in a synced folder, and how the Sent folder of my mail provider behaves. Five load-sensitive timing tests behave differently under load than alone.

The audit counted 13 other open limits. One of them is closed since, and I have not rechecked the rest. A list sorted by cost and consequence still does not exist. One limit cannot be closed on the client side: a late success reply after a reset marks a message as sent.

What does this not show?

A passing model holds for its small constants and for the code it was run against. Of the 105 valid models, 90 carry an acknowledgement under the new definition, which requires reading the diff, a replay test and a mutation pass. Seven are still drifted and 8 never drifted.

The mutation figures show that every mutation was caught by the test named for it while the controls stayed green. They do not show that the tests cover every behaviour. The reviews show that the readers described the code correctly in 118 of 189 claims and only in a narrower form in the other 71, and four rounds of outside reading are a narrow sample.

Many fix choices were made by a session on its own recommendation. In round 3 the chain made 31 such choices, in round 4 about 43, and the first four fix sessions after the audit made 17. The audit found none implemented wrongly. I confirmed the 31 and the 43 in one blanket answer on 19 October without deciding them one by one, and the 17 since then are the sessions' own recommendations.

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

Related

• Twelve days of TLA+ on my own tools
• Thirteen review rounds and one rollback
• Three outside reviews of my TLA+ models