Twelve days of TLA+ on my own tools

2026-10-09

On 22 September Boris Cherny, who created Claude Code, wrote on X that he had used Opus 5.5 to formally verify the Claude Agent SDK with Lean. Further down his post he added, "TLA+ also works well. I sometimes combine Lean and TLA+". Five days later I pointed TLA+ at my own tools, and this post counts what has happened since.

Why TLA+ and not Lean?

My tools are scripts that send outreach email, ship this site, keep shared logs and clean up after file sync. Several Claude Code sessions run them at the same time, and a sync service writes to the same folder. The faults I worry about depend on the order in which those writers happen to run. TLA+ describes a system as states and the steps between them, and its model checker TLC tries every order of steps the model allows. My question was about order, so I left Lean out.

One rule came before the first model. A finding counts only when it reproduces against the unchanged code or has already happened on disk, and an independent Sonnet subagent compares the model with the code. A day after his first post Boris described the same sequence of work in a follow-up: build a model, find counterexamples in it, reproduce them and fix them.

What did the first model find?

The pilot on 27 September modelled the script that deletes the conflict copies file sync leaves behind. TLC found a run in which the script deleted the newest version of a file, because sync had restored an old version under the original name and the newer text sat in the copy. The same run reproduced against the unchanged script.

I fixed it, and the model of the fixed script found a hole in the fix. The fix was safe only if sync kept the old file's modification time, and I had never measured whether it does. The script now handles only copies whose content is identical to the original, and since 28 September it moves them to a quarantine folder instead of deleting them.

How far did it go?

On 28 September six more phases ran in one day. Here is one finding each from five of the tools:

By 1 October I had 23 distinct models in 27 files. The largest state space TLC explored held 20 849 212 distinct states.

Who checked the work?

Outside models read the work several times. The last two reads came from ChatGPT, and Sonnet subagents checked every claim against the code before anything was fixed. A refined claim held only in a narrower form or at a lower severity than the reviewer gave it.

On 8 October I also checked the 70 fixes from the first review with 497 Sonnet subagents. That run has its own post.

How many fix rounds so far?

I count a round as one logged batch of fixes that went into code together. Before 7 October a batch was a wave of decisions after the models, and after that it was a fix group or one session from a fix list.

Two more sessions from that check are open. The 8 October review set seven more rounds, and they wait for 13 decisions that only I can make. Since the pilot my decision log has gained 81 numbered entries, not all of them about TLA+.

How many gates and hooks?

The gates live in turva-portit, a Claude Code plugin I wrote for this workspace. It hooks into Claude Code at six points: session start, each prompt, before a tool call, after a tool call, before the context is compacted and when a session stops. Seven hook scripts sit behind those points. A gate is one check inside them that blocks or asks before a session does something my rules forbid.

The 9 October column is the plugin's source. The installed plugin is still 0.44.1 until I install 0.45.0.

Outside the plugin, 21 scripts in my tools folder carry portti, the Finnish word for gate, in their names, and the docs check runs 35 checks before every ship. The full mutation run breaks the tools' code one change at a time and expects a test to notice. Its last full run, on 9 October, caught 577 of 577 mutations in 2 hours 37 minutes.

What does this not show?

A model covers only what I put in it. A green TLC run says nothing about a step the model leaves out, so a model has to be read against the code again whenever the code changes. TLC also checks only within the bounds each model sets, such as a fixed number of sessions and files, and a fault that needs more than that stays out of its reach.

I made the counts in this post from my own logs. The rounds before 7 October are my grouping of logged sessions.

Why keep going?

Seven rounds wait for my decisions, and every round so far has left something for the next one. I will not stop until the last stone is turned. Luckily Claude does not get tired.

Related

• What 497 cloud agents asked of my desktop
• The checks that pass for the wrong reason
• My gate could not see a sixth