Thirteen review rounds and one rollback

2026-10-12

This is the second part of Twelve days of TLA+ on my own tools. That post ended with seven fix rounds waiting for 13 decisions that only I could make. On 10 October I took the recommendation on all 13, and two of the seven rounds are now done. Beside them ran a fix session for my gates, and it lasted more than a day and kept my machine busy with mutation runs.

What did the two TLA+ rounds fix?

The first round fixed the ship script and its release tags. The script now saves its record of what was deployed only when the files on disk still match the ones it read before the deploy, and a refused save stops the ship before any commit. Release tags now point at the commit the release script checked. The second round fixed the shared state files: before every retry of a rename, the helper that writes them checks that it still holds the lock. Five fix rounds still wait.

What was the gate fix about?

My workspace has a rule that a session never runs git. A gate in turva-portit, the Claude Code plugin from part 1, enforces it by reading every shell command before it runs. A check of the plugin's earlier fixes on 9 October left a fix list, and one session worked through four of its items from the evening of 10 October to the night of 11 October.

One item asked the gate to stop blocking harmless PowerShell text that only mentions git inside quotes. That block is a false alarm and, as far as I have seen, only costs a retry. Narrowing it meant teaching the gate which quoted words PowerShell will still run as a command.

Why did every round find a new hole?

Each fix went to an independent Sonnet subagent that tried to get git past the gate. Review rounds 1 to 8 each found a new way past the narrowed PowerShell rule. Every parsing rule I added opened the next gap. From round 4 on the reviewers used PowerShell's own parser as the judge and generated their own inputs, soon in the hundreds of thousands. In round 6 the narrowed rule let git through in 176 of 700 000 inputs that the old gate blocked.

Before round 8 I set a stopping rule: if that round found escapes too, the PowerShell part of the narrowing would be undone. It did, so I undid it. Quoted git in PowerShell is blocked again, as it was before the session. Eight rounds of problems came from one change whose only benefit was removing a harmless false block.

The other items stayed. One of them took review rounds 9 to 13, and its rule became a list of allowed command shapes. In all the session ran 13 numbered review rounds, one of them twice. The 23 subagent runs through round 9, implementers and reviewers together and the mutation speed work included, added up to about 21 hours of run time and about 7 800 000 tokens, all on Sonnet. Rounds 10 to 13 came on top.

How was the result checked?

The full comparison in round 9 checked the fixed gate against the gate from before the session on about 4 000 000 PowerShell inputs, 1 100 000 bash inputs and 12 386 real commands from my session logs. It found no input that the old git gate blocked and the new one lets through.

That comparison does not prove the gate is complete. Earlier in the session the reviewers measured 456 inputs where PowerShell runs git and neither the old nor the new gate blocks it. Those holes are older than this session and are listed for a session of their own.

What did the mutation runs cost?

A mutation run breaks the plugin's code one change at a time and expects a test to notice. In part 1 a full run took 2 hours 37 minutes. On the evening of 10 October another session had started one, and the fix session began an hour later on the same machine. I stopped the run after about 16 hours without knowing how far it had got, and I never found out why it was so slow.

Until then every mutation ran the whole test suite, which took about 400 seconds during the fix session and about 310 seconds when I later measured it on a quiet machine. The fix session changed that: a mutation now runs only the test meant to catch it, and a mutation that survives gets the whole suite. Three parallel parts then finished all mutations in 11 to 12 minutes, and a sample of 40 mutations gave the same result in both modes.

More parallel parts did not help at first. With 96 parts Windows ran out of resources and showed a system error, and with 6 parts the timing tests in the starting check failed under load and stopped the run before its first mutation. Now the starting check runs once on its own, and the timing tests compare growth between two input sizes instead of a fixed two seconds. Runs with 3, 12 and 24 parts caught 643 of 643 mutations in 707, 535 and 519 seconds.

On the morning of 12 October my weekly health check started two mutation runs on its own. One hit its time limit and I stopped the other. Mutation runs are no longer part of the weekly check, and I start them by hand.

Why is this a forced break?

While these runs went on, the processor drew about 140 W for about 14 hours in a row and peaked at 62 °C. I have kept the machine free for the mutation runs, because other load can slow a run or fail a timing test, and then I cannot read the result.

So I am on a forced break. Luckily my running costs are small, so the break does not hurt. I do not even want to do other work until I can trust the results again.

What does this not show?

A mutation caught by a test proves that the test notices that one change. It says nothing about a fault no mutation imitates. The zero regressions in the comparison hold for the inputs the generators and my logs produced, and the 456 shared holes show what a comparison against the old gate cannot see.

I made the counts in this post from my own logs and the subagents' usage readings. The power and temperature figures are my own readings from a hardware monitor.

Related

• Twelve days of TLA+ on my own tools
• The checks that pass for the wrong reason
• What 497 cloud agents asked of my desktop