2026-06-15T05:30:34Z by Showboat 0.6.1
Who, what, why. Hi Joël — Adam here. Well, sort of Adam. The words below were assembled by a Claude Opus-based agent running on Lathe inside Open WebUI, while the real Adam loaded the dishwasher and supervised from his phone. (He'd like it noted that the forks are now sorted. So are the bytes.)
You mentioned you want to test 9P implementations to a depth beyond what a finite, small test suite can reach. That's a great instinct and it leads somewhere fun: formal verification. This document is a big-picture tour of FV using TLA+ as the working example. Fair warning up front: TLA+ may not be the ideal tool for the 9P job — we'll get into why — but we're going to stumble forward with it anyway, because the stumbling is where the learning lives. I'll make some mistakes on purpose. One of them is going to feel like a win right up until it isn't.
This whole thing is an executable document built with Simon Willison's showboat — you know Simon. Every code block below was actually run; the outputs are captured live, not hand-waved.
(Full disclosure, and it's a fitting one for this particular essay:
showboat verifywon't cleanly re-confirm this doc, because TLC stamps every run with a fresh wall-clock timestamp, so the captured output never byte-matches a re-run. A document about how green checkmarks lie to you cannot get its own green checkmark. I could not have planned this better if I'd tried. Read it as inspiration, not as a notarized affidavit.)
A test suite is a finite list of stories you thought to tell. "When a client opens a file read-only and tries to write, the server should refuse." Great test. You wrote it because you thought of it. The bugs that bite are the stories you didn't think of — the weird interleaving of two clients sharing a fid, the open that half-succeeds, the eleventh-hour clunk. Tests are sampling. You're hoping your samples hit the landmines.
9P — the Plan 9 file protocol, also called
Styx, documented in intro(5) and
described beautifully in the diod protocol notes —
is exactly the kind of thing where the interesting bugs hide in the interleavings. Fids,
qids, the attach → walk → open → read/write → clunk lifecycle. Lots of state. Lots of order.
Model checking flips the sampling around. Instead of you picking the stories, you describe the rules, and a tool called a model checker explores every reachable state up to some bound — every interleaving, every order — looking for one where a rule breaks. Leslie Lamport's TLA+ is the most famous tool for this; its checker is called TLC. Amazon's now-classic paper is the canonical "this actually found real bugs in production systems" story.
The catch — and Joël, please tattoo this somewhere visible — model checking explores every state of your model, not your code. The model is a story you wrote about the code. If the story is wrong, the green checkmark is a lie. We are going to walk straight into that lie on purpose later, because it's the single most important thing to understand about this whole game.
TLA+ ships as a Java jar (tla2tools.jar) containing the parser, the TLC model checker, and
more. We grabbed it from the official tlaplus release
and we've got a JRE. Nothing exotic. Let's confirm the tools are alive before we trust a word
they say later.
java -version 2>&1 | head -1; echo "---"; java -cp tla2tools.jar tlc2.TLC 2>&1 | head -2openjdk version "21.0.11" 2026-04-21
---
TLC2 Version 2.19 of 08 August 2024 (rev: 5a47802)
Error: Error: Missing input TLA+ module.
Here's our trusted model — the ruler we measure implementations against. It's deliberately
tiny. It does not model the wire format, byte counts, tags, or auth. It models where the
bugs live: the fid lifecycle and the qid (the server's stable identity for a file —
intro(5): "two files are the same
if and only if their qids are the same").
A fid starts unallocated; attach/walk bind it to a file; open arms it for I/O in a
mode; read/write use it; clunk forgets it. The rules we encode: can't open something
unbound, can't read something opened write-only, a bound fid keeps its qid until clunk.
Read it like prose — /\ is "and", \E is "there exists", var' is "var in the next state":
cat NinePTrustedV1.tla--------------------------- MODULE NinePTrustedV1 ---------------------------
(***************************************************************************)
(* TOY trusted model of a 9P-like file protocol. *)
(* *)
(* It models the fid lifecycle -- attach, walk, open, read/write, clunk -- *)
(* and the rules that make 9P "9P": you cannot open an unbound fid, you *)
(* cannot read a fid you opened write-only, a bound fid keeps its qid. *)
(* *)
(* This is the spec we TRUST and measure implementations against. *)
(***************************************************************************)
EXTENDS Naturals, FiniteSets
CONSTANTS Fids, Files, NoFile
Qid(f) == f
CanRead(f) == TRUE
CanWrite(f) == TRUE
Modes == {"read", "write"}
VARIABLES bound, open, omode, qid
vars == <<bound, open, omode, qid>>
Init ==
/\ bound = [f \in Fids |-> NoFile]
/\ open = [f \in Fids |-> FALSE]
/\ omode = [f \in Fids |-> "read"]
/\ qid = [f \in Fids |-> NoFile]
Attach(fid, f) ==
/\ bound[fid] = NoFile
/\ bound' = [bound EXCEPT ![fid] = f]
/\ qid' = [qid EXCEPT ![fid] = Qid(f)]
/\ UNCHANGED <<open, omode>>
Walk(fid, f) ==
/\ bound[fid] # NoFile
/\ ~open[fid]
/\ bound' = [bound EXCEPT ![fid] = f]
/\ qid' = [qid EXCEPT ![fid] = Qid(f)]
/\ UNCHANGED <<open, omode>>
Open(fid, m) ==
/\ bound[fid] # NoFile
/\ ~open[fid]
/\ \/ (m = "read" /\ CanRead(bound[fid]))
\/ (m = "write" /\ CanWrite(bound[fid]))
/\ open' = [open EXCEPT ![fid] = TRUE]
/\ omode' = [omode EXCEPT ![fid] = m]
/\ UNCHANGED <<bound, qid>>
\* Tread: only legal when fid is open and was opened in read mode.
Read(fid) ==
/\ open[fid]
/\ omode[fid] = "read"
/\ UNCHANGED vars
\* Twrite: only legal when fid is open and was opened in write mode.
Write(fid) ==
/\ open[fid]
/\ omode[fid] = "write"
/\ UNCHANGED vars
Clunk(fid) ==
/\ bound[fid] # NoFile
/\ bound' = [bound EXCEPT ![fid] = NoFile]
/\ open' = [open EXCEPT ![fid] = FALSE]
/\ omode' = [omode EXCEPT ![fid] = "read"]
/\ qid' = [qid EXCEPT ![fid] = NoFile]
Next ==
\/ \E fid \in Fids, f \in Files : Attach(fid, f)
\/ \E fid \in Fids, f \in Files : Walk(fid, f)
\/ \E fid \in Fids, m \in Modes : Open(fid, m)
\/ \E fid \in Fids : Read(fid)
\/ \E fid \in Fids : Write(fid)
\/ \E fid \in Fids : Clunk(fid)
Spec == Init /\ [][Next]_vars
TypeOK ==
/\ bound \in [Fids -> Files \cup {NoFile}]
/\ open \in [Fids -> BOOLEAN]
/\ omode \in [Fids -> Modes]
/\ qid \in [Fids -> Files \cup {NoFile}]
OpenImpliesBound == \A fid \in Fids : open[fid] => bound[fid] # NoFile
QidConsistent ==
\A fid \in Fids : bound[fid] # NoFile => qid[fid] = Qid(bound[fid])
Safety == TypeOK /\ OpenImpliesBound /\ QidConsistent
=============================================================================
TLC needs a tiny config file saying how big to make the universe (model checking is finite — we bound the fids and files) and which invariants to enforce:
SPECIFICATION Spec
CONSTANTS
Fids = {1, 2}
Files = {f1, f2}
NoFile = NoFile
INVARIANT TypeOK
INVARIANT OpenImpliesBound
INVARIANT QidConsistent
Two fids, two files. That's enough to exercise every interesting interleaving of the lifecycle. Let's check that our trusted spec is at least internally consistent — that it never violates its own invariants in any reachable state:
java -cp tla2tools.jar tlc2.TLC -config NinePTrustedV1.cfg NinePTrustedV1.tla 2>&1 | grep -vE "^Warning|UseParallelGC|nowarning|^$" | tail -12Semantic processing of module NinePTrustedV1
Starting... (2026-06-15 05:33:03)
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2026-06-15 05:33:03.
Model checking completed. No error has been found.
Estimates of the probability that TLC did not check all reachable states
because two distinct states had the same fingerprint:
calculated (optimistic): val = 6.2E-16
281 states generated, 49 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 5.
The average outdegree of the complete state graph is 1 (minimum is 0, the maximum 4 and the 95th percentile is 4).
Finished in 00s at (2026-06-15 05:33:04)
49 distinct states, no errors. The trusted spec doesn't contradict itself. Good. Now — this is the part Joël actually cares about — let's test an implementation against it.
You have a 9P server written by someone else, in C or Go or whatever. The dream is: turn it into a TLA+ model (this is called lifting — and yes, you can now point an LLM at a codebase and have it draft the model; Azure reportedly found a real production bug this way), then ask TLC whether that model refines our trusted spec.
Refinement is the magic word. Model Impl refines Spec if every behavior Impl allows
is also allowed by Spec. If true, the implementation can't do anything the spec forbids —
that's conformance. In TLA+ you check it by asking: is the trusted Spec a property of the
implementation? (Lamport's Specifying Systems
covers refinement mappings properly; this is the cocktail-napkin version.)
Here's our candidate. Pretend the LLM lifted it from a real server. It's almost identical to
the trusted spec, but it has a planted bug — a Read that forgot to check the open mode, so
a write-only fid can be read. (This is a real class of 9P bug; the mode check is exactly the
kind of thing that gets botched.)
sed -n "47,56p" NinePImplV1.tla\* *** THE BUG *** No omode check: reads any open fid, even write-only.
ReadBuggy(fid) ==
/\ open[fid]
/\ UNCHANGED vars
Write(fid) ==
/\ open[fid]
/\ omode[fid] = "write"
/\ UNCHANGED vars
There's the bug, plain as day: ReadBuggy only requires open[fid]. No omode = "read"
check. A fid you opened write-only sails right through.
We wire the impl to instantiate the trusted spec over the same variables and ask TLC to check
that the trusted Spec holds as a property:
SPECIFICATION Spec
CONSTANTS Fids = {1,2} Files = {f1,f2} NoFile = NoFile
PROPERTY TrustedSpec
If the implementation truly conformed, TLC would find no violation. Our impl has a glaring bug. So we should get a counterexample, right? Drumroll:
java -cp tla2tools.jar tlc2.TLC -config NinePImplV1.cfg NinePImplV1.tla 2>&1 | grep -vE "^Warning|UseParallelGC|nowarning|^$" | tail -10Computing initial states...
Finished computing initial states: 1 distinct state generated at 2026-06-15 05:33:25.
Model checking completed. No error has been found.
Estimates of the probability that TLC did not check all reachable states
because two distinct states had the same fingerprint:
calculated (optimistic): val = 6.9E-16
309 states generated, 49 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 5.
The average outdegree of the complete state graph is 1 (minimum is 0, the maximum 4 and the 95th percentile is 4).
Finished in 00s at (2026-06-15 05:33:26)
Stop and feel that for a second, Joël, because this is the most important moment in the whole document. We have a model checker — a mathematically exhaustive tool — looking at an implementation with an obvious, planted, staring-you-in-the-face bug, and it just told us everything's fine. Ship it!
This is exactly the failure mode the Specula team documented when they had LLMs model real systems: the model follows a plausible template that doesn't actually match the system's behavior, and "admits transitions that produce states the real system would never produce" — or, as here, fails to distinguish states it should. The green checkmark certifies the model, and the model is wrong.
So why did it pass? Look back at both Read actions — trusted and buggy — they both end in
UNCHANGED vars. A read changes nothing in our state. It has no observable effect. So when
the buggy impl does its illegal read, the resulting state is byte-for-byte identical to the
state before. TLA+ calls a step that changes nothing a stutter, and the spec
[][Next]_vars explicitly permits stuttering (that's what the _vars subscript means — see
Lamport on stuttering). The illegal
read disguised itself as "nothing happened," and "nothing happened" is always allowed.
The bug wasn't in the implementation's logic. The bug was in what our model could see. We abstracted away the one thing — the act of reading — that distinguishes a legal read from an illegal one. We built a smoke detector and forgot to give it a nose.
The lesson generalizes way past 9P: a model checker can only catch a divergence it can see. If the thing that distinguishes good from bad behavior isn't represented in your state, no amount of exhaustive search will find it. The checker explored all 49 states perfectly. The states just didn't contain the evidence.
For 9P, the natural observable is the thing a client actually witnesses: the I/O event —
the Rread/Rwrite response on the wire. (Conveniently, 9P's whole interface is a clean
little stream of T-messages and R-messages — see the diod protocol notes
— which is exactly the boundary you'd instrument on a real server.)
So we add an io variable recording the last I/O event, and make Read/Write emit it
instead of stuttering. Now an illegal read produces a genuinely distinct, visible state. Same
spec, same lifecycle, one new pair of eyes. Here are the changed actions in the fixed trusted
spec:
sed -n "62,79p" NinePTrusted.tla
\* Tread: only legal when fid is OPEN and was opened in read mode.
Read(fid) ==
/\ open[fid]
/\ omode[fid] = "read"
/\ io' = [op |-> "read", fid |-> fid, mode |-> "read"]
/\ UNCHANGED <<bound, open, omode, qid>>
\* Twrite: only legal when fid is OPEN and was opened in write mode.
Write(fid) ==
/\ open[fid]
/\ omode[fid] = "write"
/\ io' = [op |-> "write", fid |-> fid, mode |-> "write"]
/\ UNCHANGED <<bound, open, omode, qid>>
Clunk(fid) ==
/\ bound[fid] # NoFile
/\ bound' = [bound EXCEPT ![fid] = NoFile]
The buggy implementation gets the same treatment — its ReadBuggy now emits a read I/O
event (still without checking the mode). Everything else is unchanged; the bug is still the
missing omode check. Now we re-run the exact same refinement check. Same checker, same bug,
same tiny universe — the only difference is that our model finally has eyes:
java -cp tla2tools.jar tlc2.TLC -config NinePImpl.cfg NinePImpl.tla 2>&1 | grep -vE "^Warning|UseParallelGC|nowarning|fingerprint|optimistic|two distinct|^$" | sed -n "/Computing initial/,/Finished in/p"Computing initial states...
Finished computing initial states: 1 distinct state generated at 2026-06-15 05:33:59.
Error: Action property line 93, col 17 to line 93, col 29 of module NinePTrusted is violated.
Error: The behavior up to this point is:
State 1: <Initial predicate>
/\ qid = <<NoFile, NoFile>>
/\ omode = <<"read", "read">>
/\ open = <<FALSE, FALSE>>
/\ bound = <<NoFile, NoFile>>
/\ io = [op |-> "none", fid |-> 0, mode |-> "read"]
State 2: <Attach line 31, col 5 to line 35, col 32 of module NinePImpl>
/\ qid = <<f1, NoFile>>
/\ omode = <<"read", "read">>
/\ open = <<FALSE, FALSE>>
/\ bound = <<f1, NoFile>>
/\ io = [op |-> "none", fid |-> 0, mode |-> "read"]
State 3: <Open line 46, col 5 to line 51, col 31 of module NinePImpl>
/\ qid = <<f1, NoFile>>
/\ omode = <<"write", "read">>
/\ open = <<TRUE, FALSE>>
/\ bound = <<f1, NoFile>>
/\ io = [op |-> "none", fid |-> 0, mode |-> "read"]
State 4: <ReadBuggy line 56, col 5 to line 58, col 44 of module NinePImpl>
/\ qid = <<f1, NoFile>>
/\ omode = <<"write", "read">>
/\ open = <<TRUE, FALSE>>
/\ bound = <<f1, NoFile>>
/\ io = [op |-> "read", fid |-> 1, mode |-> "read"]
60 states generated, 27 distinct states found, 17 states left on queue.
The depth of the complete state graph search is 4.
The average outdegree of the complete state graph is 3 (minimum is 1, the maximum 4 and the 95th percentile is 4).
Finished in 00s at (2026-06-15 05:33:59)
Now we're cooking. TLC didn't just say "nope" — it handed us the shortest sequence of steps that breaks the rule:
- State 1 — fresh. Nothing bound, nothing open.
- State 2 —
Attachfid 1 to filef1. - State 3 —
Openfid 1 in"write"mode. (omode = <<"write", "read">>.) - State 4 —
ReadBuggyfid 1. Look atio:[op |-> "read", fid |-> 1, ...]. A read on a write-only fid. The trusted spec has no transition that produces this state from State 3 — itsReadrequiresomode = "read"— so the property is violated.
This four-step trace is the whole point. It's not a vague "something's wrong somewhere." It's a concrete, minimal, replayable script: attach, open-for-write, read. Hand that to a human and they immediately see the bug. And TLC found it by exhaustively checking every interleaving in the bounded universe — which is precisely the "depth beyond a finite test suite" you were after. You didn't have to think of this test. The checker enumerated it.
(Notice it explored only 27 distinct states and bailed at depth 4 the moment it found the violation — model checkers give you the shortest path to the bug, which is a lovely property when you're debugging.)
Here's the honest architecture for "test a 9P implementation deeper than a test suite can," stitched together from what we just did:
- Author a trusted model by hand. Small enough to read and believe. This is your ruler. (We just wrote one. The fact that it took two tries — that the v1 was blind — is the whole reason you keep it small and reviewable.)
- Lift the target implementation into a model. An LLM can draft this from the real source. It will be imperfect, possibly mis-specified. That's expected.
- Check refinement with TLC: does the lifted model do anything the trusted model forbids?
- If TLC finds a counterexample, you have a hypothesis, not yet a bug. It might be a real
divergence — or an artifact of a sloppy lift. So you unlift: translate that abstract
trace (attach → open-write → read) back into actual 9P wire messages —
Tattach,Topen,Tread— and replay them against the real server.- If the real server serves bytes on that read → confirmed bug. Ship the report.
- If it correctly refuses → the lift was wrong, not the server. Feed that back, refine the model, loop. (This is CEGAR — counterexample-guided abstraction refinement — in spirit.)
The crucial discipline: the concrete replay is the oracle, not the model. The LLM and the abstraction never have to be trusted — they only have to be good enough to generate hypotheses that a real replay can confirm or reject. That keeps the AI out of the trust path, which, given the stuttering fiasco above, is where you want it. The trace-validation work by Merz et al. (Oracle-funded, TLA+) is the rigorous version of this "check real executions against a trusted spec" idea.
I promised we'd stumble forward and be honest about it, so: TLA+ is fantastic for the thing we did — concurrency, interleavings, "does this state machine ever reach a bad state." That's its home turf, and it's a great fit for the protocol-level concerns of 9P (fid lifecycles, ordering, two clients racing on a shared fid).
But notice what we kept not modeling: bytes, offsets, partial reads, the actual file
contents, iounit negotiation, the wire encoding. TLA+ can express those, but it gets
clumsy, and the state space explodes. If your bugs live in the data plane rather than the
control plane, you might be happier with:
- Stateful property-based testing (Hypothesis, PropEr, QuickCheck) — generate random valid 9P command sequences, run them against the real server and a simple reference model, assert the responses agree. This is "lift/check/unlift" minus the TLA+, often with less ceremony, and it runs against the actual binary.
- A process calculus / labeled-transition tool (mCRL2, CADP) if you genuinely want bisimulation — which, recall, is a stronger relation than the refinement we checked. 9P's ancestor Styx has roots in this world, so it's philosophically apt.
- Fuzzing the parser for the wire-format bugs that are about bytes, not protocol logic.
None of that makes today wasted. The concept — trusted model, exhaustive check, concrete replayable counterexample, AI-in-the-loop-but-not-in-the-trust-path — transfers directly. TLA+ was just the clearest blackboard to learn it on.
If you want one concrete next step that's closest to your "deeper than a test suite" goal and least likely to drown you in TLA+ ceremony: stateful property-based testing against a reference model. Write the tiny trusted model (you basically have it above — it's ~90 lines), have Hypothesis/PropEr generate thousands of random valid 9P command sequences, run each against both your reference and the real server, and assert the observable responses agree. That's the whole lift→check→unlift→replay loop, collapsed into one harness, pointed at the actual binary — no abstraction gap to get bitten by.
Keep TLA+ in your back pocket for the genuinely concurrent questions — two clients racing on a shared fid, flush-vs-response ordering — where exhaustive interleaving search earns its keep and random testing gets unlucky.
And whatever you reach for, carry the one lesson that cost us a whole fake victory above:
A verifier can only catch a divergence it can see. Spend your modeling effort on the observables, not the machinery.
Go forth and break some file servers. Tell me what you find — and if you build the Hypothesis harness, send it over, I want to watch it turn red.
— Adam (via a Claude Opus agent on Lathe, who would like the record to show that the dishwasher is now running and the bytes remain sorted)