Move design docs and specs next to the code that cites them

- Move the long-turn memory benchmark guide to
  `benchmarks/long-turn-memory.md`, next to its script, so the repository no
  longer has a top-level `docs/` folder.
- Add the session manager design record and its TLA+ models and trace
  checkers under `src/core/session_manager/`, where the session code already
  cites them.
- Add the indexer refresh model under `src/core/indexer/tla/`.
- Point spec citations in code comments at the new paths, and remove
  references to design notes that are not in the repository.

src/acp/server.zig

@@ -877,7 +877,7 @@ fn resolveSubagentAuthority(
 }
 
 /// Joins the child threads before the session they append to can close
-/// (`tla/Wiring.tla` ParentOutlivesChildren).
+/// (`src/core/session_manager/tla/Wiring.tla` ParentOutlivesChildren).
 pub fn disableSubagentHost(state: *ServerState) void {
     if (state.subagent_host) |host| {
         host.deinit();

src/core/app/app_session_runtime.zig

@@ -3824,7 +3824,7 @@ pub fn Runtime(comptime App: type) type {
         }
 
         /// Stops the subagent host, joining its child threads, before the
-        /// session they append to can close (`tla/Wiring.tla`
+        /// session they append to can close (`src/core/session_manager/tla/Wiring.tla`
         /// ParentOutlivesChildren).
         pub fn disableSubagentHost(app: *App) void {
             if (app.session_persistence.subagent_host) |host| {

src/core/indexer/git_index.zig

@@ -9,7 +9,7 @@ const io_mod = @import("../shared/io.zig");
 
 const Allocator = std.mem.Allocator;
 
-/// D7: the index is never read beyond this size.
+/// The index is never read beyond this size.
 const max_index_bytes: usize = 128 * 1024 * 1024;
 
 const mode_type_mask: u32 = 0o170000;

src/core/indexer/ignore.zig

@@ -8,7 +8,7 @@ const wildmatch = @import("wildmatch.zig");
 
 const Allocator = std.mem.Allocator;
 
-/// Largest pattern file read, per source (D7).
+/// Largest pattern file read, per source.
 pub const max_pattern_file_bytes: usize = 1024 * 1024;
 
 const Pattern = struct {

src/core/indexer/scan.zig

@@ -29,12 +29,12 @@ pub const Kind = tree_mod.Kind;
 pub const Entry = tree_mod.Entry;
 
 pub const Options = struct {
-    /// D7: at most this many files are returned. Folder rows do not count;
+    /// At most this many files are returned. Folder rows do not count;
     /// the collection limit (`collect_factor`) bounds them.
     candidate_cap: usize = 100_000,
     max_path_bytes: usize = 2048,
     /// Folder and file names skipped outside repositories and below an
-    /// ignored root (D4, U3). Never applied inside a repository.
+    /// ignored root. Never applied inside a repository.
     skipped_names: []const []const u8 = &default_skipped_names,
     max_workers: usize = 8,
 };
@@ -634,7 +634,7 @@ fn entryLessThan(_: void, a: Entry, b: Entry) bool {
 }
 
 /// Length of the sorted prefix that holds the first `cap` files, or null when
-/// `entries` has no more than `cap` files. Folder rows do not count (D7).
+/// `entries` has no more than `cap` files. Folder rows do not count.
 fn capCut(entries: []const Entry, cap: usize) ?usize {
     var files: usize = 0;
     for (entries, 0..) |entry, index| {

src/core/indexer/tla/Refresh.tla

@@ -0,0 +1,74 @@
+-------------------------------- MODULE Refresh --------------------------------
+EXTENDS Naturals, Sequences
+CONSTANTS MaxSteps, Guarded
+Files == {"a.txt", "b.txt"}
+VARIABLES fs, tick, stamp, ignoreB, ignoreEpoch, knownStamp, knownIgnore,
+          reusable, snapshot, phase, beforeStamp, beforeIgnore, beforeTick,
+          listed, published, history
+vars == <<fs, tick, stamp, ignoreB, ignoreEpoch, knownStamp, knownIgnore,
+          reusable, snapshot, phase, beforeStamp, beforeIgnore, beforeTick,
+          listed, published, history>>
+Visible == IF ignoreB THEN fs \ {"b.txt"} ELSE fs
+Init == /\ fs = {} /\ tick = 0 /\ stamp = 0
+        /\ ignoreB = FALSE /\ ignoreEpoch = 0
+        /\ knownStamp = 0 /\ knownIgnore = 0 /\ reusable = FALSE
+        /\ snapshot = {} /\ phase = "idle" /\ beforeStamp = 0
+        /\ beforeIgnore = 0 /\ beforeTick = 0 /\ listed = {}
+        /\ published = FALSE /\ history = <<>>
+Edit(p) == /\ fs' = IF p \in fs THEN fs \ {p} ELSE fs \cup {p}
+           /\ stamp' = tick /\ published' = FALSE
+           /\ history' = Append(history, "Edit:" \o p)
+           /\ UNCHANGED <<tick, ignoreB, ignoreEpoch, knownStamp, knownIgnore,
+                           reusable, snapshot, phase, beforeStamp,
+                           beforeIgnore, beforeTick, listed>>
+Tick == /\ tick < 2 /\ tick' = tick + 1 /\ published' = FALSE
+        /\ history' = Append(history, "Tick")
+        /\ UNCHANGED <<fs, stamp, ignoreB, ignoreEpoch, knownStamp, knownIgnore,
+                        reusable, snapshot, phase, beforeStamp, beforeIgnore,
+                        beforeTick, listed>>
+ChangeIgnore == /\ ignoreB' = ~ignoreB /\ ignoreEpoch' = ignoreEpoch + 1
+                /\ published' = FALSE
+                /\ history' = Append(history, "ChangeIgnore")
+                /\ UNCHANGED <<fs, tick, stamp, knownStamp, knownIgnore,
+                                reusable, snapshot, phase, beforeStamp,
+                                beforeIgnore, beforeTick, listed>>
+Reuse == /\ phase = "idle" /\ stamp = knownStamp
+         /\ (~Guarded \/ (reusable /\ stamp < tick /\
+                          ignoreEpoch = knownIgnore))
+         /\ published' = TRUE /\ history' = Append(history, "Reuse")
+         /\ UNCHANGED <<fs, tick, stamp, ignoreB, ignoreEpoch, knownStamp,
+                         knownIgnore, reusable, snapshot, phase, beforeStamp,
+                         beforeIgnore, beforeTick, listed>>
+Begin == /\ phase = "idle" /\ phase' = "listing"
+         /\ beforeStamp' = stamp /\ beforeIgnore' = ignoreEpoch
+         /\ beforeTick' = tick /\ published' = FALSE
+         /\ history' = Append(history, "Begin")
+         /\ UNCHANGED <<fs, tick, stamp, ignoreB, ignoreEpoch, knownStamp,
+                         knownIgnore, reusable, snapshot, listed>>
+List == /\ phase = "listing" /\ phase' = "validate" /\ listed' = Visible
+        /\ published' = FALSE /\ history' = Append(history, "List")
+        /\ UNCHANGED <<fs, tick, stamp, ignoreB, ignoreEpoch, knownStamp,
+                        knownIgnore, reusable, snapshot, beforeStamp,
+                        beforeIgnore, beforeTick>>
+Commit == LET valid == ~Guarded \/ (stamp = beforeStamp /\
+                                   ignoreEpoch = beforeIgnore /\
+                                   stamp < beforeTick)
+          IN /\ phase = "validate" /\ phase' = "idle"
+             /\ snapshot' = IF valid THEN listed ELSE snapshot
+             /\ knownStamp' = IF valid THEN stamp ELSE knownStamp
+             /\ knownIgnore' = IF valid THEN ignoreEpoch ELSE knownIgnore
+             /\ reusable' = IF valid THEN TRUE ELSE reusable
+             /\ published' = valid /\ history' = Append(history, "Commit")
+             /\ UNCHANGED <<fs, tick, stamp, ignoreB, ignoreEpoch, beforeStamp,
+                             beforeIgnore, beforeTick, listed>>
+Next == /\ Len(history) < MaxSteps
+        /\ ((\E p \in Files : Edit(p)) \/ Tick \/ ChangeIgnore \/
+             Reuse \/ Begin \/ List \/ Commit)
+Spec == Init /\ [][Next]_vars
+TypeOK == /\ fs \subseteq Files /\ snapshot \subseteq Files
+          /\ listed \subseteq Files /\ tick \in 0..2 /\ stamp \in 0..2
+          /\ ignoreB \in BOOLEAN /\ published \in BOOLEAN
+          /\ reusable \in BOOLEAN /\ phase \in {"idle", "listing", "validate"}
+          /\ ignoreEpoch \in 0..MaxSteps /\ Len(history) <= MaxSteps
+NoStalePublication == published => snapshot = Visible
+=============================================================================

src/core/indexer/tla/RefreshWitness.tla

@@ -0,0 +1,21 @@
+---------------------------- MODULE RefreshWitness ----------------------------
+\* Each invariant claims a reuse path cannot happen. TLC's counterexample is
+\* then the shortest trace that exercises it, which the real replay runs.
+EXTENDS Refresh
+Before(a, b) == \E i, j \in 1..Len(history) : i < j /\ history[i] \in a /\ history[j] = b
+NoReuse == ~Before({"Begin"}, "Reuse")
+NoReuseAfterEdit == ~Before({"Edit:a.txt", "Edit:b.txt"}, "Reuse")
+\* Real files have only times, so an ignore change counts once a Tick passes;
+\* b.txt exists first so the reused snapshot must reflect the new rule.
+NoReuseAfterIgnore == ~\E i, k, m, j \in 1..Len(history) :
+    /\ i < k /\ k < m /\ m < j
+    /\ history[i] = "Edit:b.txt" /\ history[k] = "ChangeIgnore"
+    /\ history[m] = "Tick" /\ history[j] = "Reuse"
+\* A change after a reuse: the real code must notice it at the next check.
+NoEditAfterReuse == ~\E i, j \in 1..Len(history) :
+    i < j /\ history[i] = "Reuse" /\ history[j] \in {"Edit:a.txt", "Edit:b.txt"}
+NoIgnoreChangeAfterReuse == ~\E i, k, j \in 1..Len(history) :
+    /\ i < k /\ k < j
+    /\ history[i] = "Edit:b.txt" /\ history[k] = "Reuse"
+    /\ history[j] = "ChangeIgnore"
+=============================================================================

src/core/indexer/tla/refresh-mutation.cfg

@@ -0,0 +1,4 @@
+SPECIFICATION Spec
+CONSTANTS MaxSteps = 6
+          Guarded = FALSE
+INVARIANTS TypeOK NoStalePublication

src/core/indexer/tla/refresh-simulation.cfg

@@ -0,0 +1,3 @@
+SPECIFICATION Spec
+CONSTANTS MaxSteps = 10 Guarded = TRUE
+INVARIANTS TypeOK NoStalePublication

src/core/indexer/tla/refresh-witness-NoEditAfterReuse.cfg

@@ -0,0 +1,3 @@
+SPECIFICATION Spec
+CONSTANTS MaxSteps = 10 Guarded = TRUE
+INVARIANTS TypeOK NoStalePublication NoEditAfterReuse

src/core/indexer/tla/refresh-witness-NoIgnoreChangeAfterReuse.cfg

@@ -0,0 +1,3 @@
+SPECIFICATION Spec
+CONSTANTS MaxSteps = 10 Guarded = TRUE
+INVARIANTS TypeOK NoStalePublication NoIgnoreChangeAfterReuse

src/core/indexer/tla/refresh-witness-NoReuse.cfg

@@ -0,0 +1,3 @@
+SPECIFICATION Spec
+CONSTANTS MaxSteps = 10 Guarded = TRUE
+INVARIANTS TypeOK NoStalePublication NoReuse

src/core/indexer/tla/refresh-witness-NoReuseAfterEdit.cfg

@@ -0,0 +1,3 @@
+SPECIFICATION Spec
+CONSTANTS MaxSteps = 10 Guarded = TRUE
+INVARIANTS TypeOK NoStalePublication NoReuseAfterEdit

src/core/indexer/tla/refresh-witness-NoReuseAfterIgnore.cfg

@@ -0,0 +1,3 @@
+SPECIFICATION Spec
+CONSTANTS MaxSteps = 10 Guarded = TRUE
+INVARIANTS TypeOK NoStalePublication NoReuseAfterIgnore

src/core/indexer/tla/refresh.cfg

@@ -0,0 +1,4 @@
+SPECIFICATION Spec
+CONSTANTS MaxSteps = 6
+          Guarded = TRUE
+INVARIANTS TypeOK NoStalePublication

src/core/indexer/tree.zig

@@ -4,7 +4,7 @@
 //! its times are older than the scan's start by the granularity margin, so a
 //! change in the same clock tick as the scan, which a later stamp comparison
 //! could not see, always forces a new scan. This is the reuse certificate the
-//! refresh model (Refresh.tla) requires.
+//! refresh model (`tla/Refresh.tla`) requires.
 
 const std = @import("std");
 const io_mod = @import("../shared/io.zig");

src/core/mcp_host/runtime.zig

@@ -1160,7 +1160,7 @@ pub const Runtime = struct {
     }
 
     /// Permission is fx's tool admission, before the call reaches the
-    /// runtime, and only the runtime calls the engine (D6).
+    /// runtime, and only the runtime calls the engine.
     fn allow(_: *anyopaque, _: []const u8, _: []const u8, _: ?[]const u8) bool {
         return true;
     }

src/core/session/session_adapter.zig

@@ -18,7 +18,7 @@
 //!   ACP client's prompt and tool identities are settings (D46); hosted
 //!   terminal state lives in `~/.fx/terminal/{id}/` (D45). An older session
 //!   with a `~/.fx/session-files/{id}/` side folder moves on its first
-//!   writable open (D47, `tla/MoveSideFiles.tla`).
+//!   writable open (D47, `src/core/session_manager/tla/MoveSideFiles.tla`).
 
 const std = @import("std");
 const testing_allocator = @import("../shared/testing_allocator.zig");
@@ -1123,7 +1123,7 @@ pub const Session = struct {
     }
 
     /// Closes the session and frees the adapter. Every child thread of this
-    /// session must have joined (`tla/Wiring.tla` ParentOutlivesChildren).
+    /// session must have joined (`src/core/session_manager/tla/Wiring.tla` ParentOutlivesChildren).
     /// A copy of its capability that a background reader still holds keeps
     /// reading, and stores nothing more (D44).
     pub fn close(self: *Session) void {
@@ -1782,11 +1782,12 @@ pub const Session = struct {
 
     // -- the move off the side folder (D47) -----------------------------------
 
-    /// Makes an older session one manager folder (D47, `tla/MoveSideFiles.tla`)
-    /// on its first writable open, then loads the map its old handles resolve
-    /// through. Every body in the side folder becomes a blob, the map from
-    /// each old name to its blob is one more blob, and one batch records the
-    /// map, every moved blob, and the client's settings from the old files.
+    /// Makes an older session one manager folder (D47,
+    /// `src/core/session_manager/tla/MoveSideFiles.tla`) on its first writable
+    /// open, then loads the map its old handles resolve through. Every body
+    /// in the side folder becomes a blob, the map from each old name to its
+    /// blob is one more blob, and one batch records the map, every moved
+    /// blob, and the client's settings from the old files.
     /// Then the terminal folder moves to `~/.fx/terminal/{id}` and the side
     /// folder goes. Each step can be repeated, so a crash at any point
     /// redoes the move on the next open.
@@ -1813,7 +1814,7 @@ pub const Session = struct {
     }
 
     /// Every step of the move but the side folder's removal, in the order
-    /// `tla/MoveSideFiles.tla` checks; returns how many bodies moved.
+    /// `src/core/session_manager/tla/MoveSideFiles.tla` checks; returns how many bodies moved.
     fn moveOut(self: *Session, side: *io_mod.VerifiedDir) !usize {
         var scratch = std.heap.ArenaAllocator.init(self.alloc);
         defer scratch.deinit();

src/core/session_manager/api.zig

@@ -3,7 +3,7 @@
 //!
 //! This file (L4) is the only public root; fx imports it and nothing else.
 //! A process creates one `Manager` with `init`, which does no disk I/O.
-//! Thirteen operations cover every host (docs/session-manager/system-design.md
+//! Thirteen operations cover every host (`system-design.md`
 //! "API"), plus `verify` and `rebuild` for doctor:
 //!
 //!   openNew  openResume  openFork  openImport        -> Session

src/core/session_manager/tla/Catalog.cfg

@@ -0,0 +1,9 @@
+SPECIFICATION Spec
+CONSTANT Ids = {s1, s2, s3}
+INVARIANTS
+    TypeOK
+    ListedAreLive
+    NoResurrection
+    IndexNamesPublished
+PROPERTIES
+    RebuildIsExact

src/core/session_manager/tla/Catalog.tla

@@ -0,0 +1,156 @@
+----------------------------- MODULE Catalog -----------------------------
+(***************************************************************************)
+(* Step: L3 catalog (index.jsonl).                                        *)
+(*                                                                         *)
+(* The index is derived. Publishing a folder happens before its index    *)
+(* put; delete renames the folder to .trash before its tombstone, then   *)
+(* purges it. A crash can land between any two steps and forgets owed    *)
+(* index writes. list() filters out entries whose folder is missing and *)
+(* appends a tombstone for them (Heal). rebuild() re-derives the index   *)
+(* from live folders and purges .trash, atomically under index.lock.     *)
+(*                                                                         *)
+(* Design: system-design.md "Concurrency And Ordering" (index) and       *)
+(* "Reliability And Recovery".                                           *)
+(***************************************************************************)
+EXTENDS Naturals, Sequences, FiniteSets
+
+CONSTANT Ids
+
+VARIABLES
+    dir,          \* [Ids -> {"none", "live", "trash", "gone"}]
+    index,        \* a sequence of [id, op], op \in {"put", "del"}
+    pending,      \* [Ids -> {"none", "put", "del"}]: index write still owed
+    everDeleted   \* ghost: ids that were ever deleted
+
+vars == <<dir, index, pending, everDeleted>>
+
+LastOp(s) ==
+    LET is == {i \in 1..Len(index) : index[i].id = s} IN
+    IF is = {} THEN "none"
+    ELSE index[CHOOSE i \in is : \A j \in is : j <= i].op
+
+Indexed == {s \in Ids : LastOp(s) = "put"}
+Live == {s \in Ids : dir[s] = "live"}
+
+\* What list() returns: indexed entries whose folder exists.
+Listed == {s \in Indexed : dir[s] = "live"}
+
+TypeOK ==
+    /\ dir \in [Ids -> {"none", "live", "trash", "gone"}]
+    /\ pending \in [Ids -> {"none", "put", "del"}]
+    /\ everDeleted \subseteq Ids
+
+Init ==
+    /\ dir = [s \in Ids |-> "none"]
+    /\ index = <<>>
+    /\ pending = [s \in Ids |-> "none"]
+    /\ everDeleted = {}
+
+\* First save: rename .tmp/{id} to {id}; the index put is owed next.
+Publish(s) ==
+    /\ dir[s] = "none"
+    /\ dir' = [dir EXCEPT ![s] = "live"]
+    /\ pending' = [pending EXCEPT ![s] = "put"]
+    /\ UNCHANGED <<index, everDeleted>>
+
+IndexPut(s) ==
+    /\ pending[s] = "put"
+    /\ index' = Append(index, [id |-> s, op |-> "put"])
+    /\ pending' = [pending EXCEPT ![s] = "none"]
+    /\ UNCHANGED <<dir, everDeleted>>
+
+\* delete(): rename {id} to .trash/{id}; the tombstone is owed next.
+Trash(s) ==
+    /\ dir[s] = "live"
+    /\ pending[s] = "none"
+    /\ dir' = [dir EXCEPT ![s] = "trash"]
+    /\ pending' = [pending EXCEPT ![s] = "del"]
+    /\ everDeleted' = everDeleted \cup {s}
+    /\ UNCHANGED index
+
+IndexDel(s) ==
+    /\ pending[s] = "del"
+    /\ index' = Append(index, [id |-> s, op |-> "del"])
+    /\ pending' = [pending EXCEPT ![s] = "none"]
+    /\ UNCHANGED <<dir, everDeleted>>
+
+Purge(s) ==
+    /\ dir[s] = "trash"
+    /\ pending[s] = "none"
+    /\ dir' = [dir EXCEPT ![s] = "gone"]
+    /\ UNCHANGED <<index, pending, everDeleted>>
+
+\* A resume, or a title, workspace or language change, rewrites the entry of
+\* a live session (D42). The session holds its writer lock throughout, and
+\* delete needs that lock (Busy), so no Trash lands inside it. Over an entry
+\* already put, a refresh changes no last op, so the spec leaves that case
+\* out; over a missing one, such as a publish put a crash forgot, it heals.
+Refresh(s) ==
+    /\ dir[s] = "live"
+    /\ LastOp(s) # "put"
+    /\ index' = Append(index, [id |-> s, op |-> "put"])
+    /\ UNCHANGED <<dir, pending, everDeleted>>
+
+\* A crash forgets every owed index write.
+Crash ==
+    /\ \E s \in Ids : pending[s] # "none"
+    /\ pending' = [s \in Ids |-> "none"]
+    /\ UNCHANGED <<dir, index, everDeleted>>
+
+\* list() self-heal: tombstone an indexed id whose folder is missing.
+Heal(s) ==
+    /\ s \in Indexed
+    /\ dir[s] # "live"
+    /\ index' = Append(index, [id |-> s, op |-> "del"])
+    /\ UNCHANGED <<dir, pending, everDeleted>>
+
+\* rebuild(): a fresh index with one put per live folder, then one del per
+\* tombstoned id, each group in any order; .trash is purged. Tombstones
+\* survive so a deleted id can never be re-imported or listed again. Owed
+\* writes are dropped because the fresh index already reflects the folders.
+Tombstoned == {s \in Ids : LastOp(s) = "del"}
+
+Rebuild ==
+    /\ LET n == Cardinality(Live)
+           m == Cardinality(Tombstoned)
+       IN \E order \in [1..n -> Live], gone \in [1..m -> Tombstoned] :
+          /\ \A i, j \in 1..n : i # j => order[i] # order[j]
+          /\ \A i, j \in 1..m : i # j => gone[i] # gone[j]
+          /\ index' = [i \in 1..n |-> [id |-> order[i], op |-> "put"]]
+                      \o [i \in 1..m |-> [id |-> gone[i], op |-> "del"]]
+    /\ dir' = [s \in Ids |-> IF dir[s] = "trash" THEN "gone" ELSE dir[s]]
+    /\ pending' = [s \in Ids |-> "none"]
+    /\ UNCHANGED everDeleted
+
+Next ==
+    \/ \E s \in Ids :
+          \/ Publish(s)
+          \/ IndexPut(s)
+          \/ Refresh(s)
+          \/ Trash(s)
+          \/ IndexDel(s)
+          \/ Purge(s)
+          \/ Heal(s)
+    \/ Crash
+    \/ Rebuild
+
+Spec == Init /\ [][Next]_vars
+
+-----------------------------------------------------------------------------
+(* Invariants *)
+
+\* list() never returns a session whose folder is gone.
+ListedAreLive == Listed \subseteq Live
+
+\* A deleted id never comes back, in the list or on disk.
+NoResurrection ==
+    \A s \in everDeleted : s \notin Listed /\ dir[s] # "live"
+
+\* The index only ever names ids that were published.
+IndexNamesPublished ==
+    \A i \in 1..Len(index) : dir[index[i].id] # "none"
+
+(* Action property: right after rebuild(), the index lists exactly the *)
+(* live folders.                                                        *)
+RebuildIsExact == [][Rebuild => (Indexed' = Live')]_vars
+=============================================================================

src/core/session_manager/tla/Fork.cfg

@@ -0,0 +1,12 @@
+SPECIFICATION Spec
+CONSTANTS
+    Ids = {s1, s2, s3}
+    Blobs = {b1, b2}
+    MaxLen = 4
+    NoBlob = NoBlob
+INVARIANTS
+    TypeOK
+    RefsExist
+    ForkKeepsPrefix
+    ForkAtBoundary
+    FirstLine

src/core/session_manager/tla/Fork.tla

@@ -0,0 +1,159 @@
+------------------------------- MODULE Fork -------------------------------
+(***************************************************************************)
+(* Step: L2 fork and blobs.                                               *)
+(*                                                                         *)
+(* A blob file lands before any line can reference it. A fork copies     *)
+(* lines 2..S of its source at a turn boundary and hard-links the        *)
+(* source's blobs. Deleting a session removes its folder, log and links. *)
+(* Invariants: every blob a live log references exists in that session,  *)
+(* unless the disk lost it there, and a fork keeps its copied prefix     *)
+(* whatever later happens to its source. A lost blob damages only its   *)
+(* session: a fork never copies a line that names one (D39).            *)
+(*                                                                         *)
+(* Design: system-design.md D5, D6 and D39.                               *)
+(***************************************************************************)
+EXTENDS Naturals, Sequences, FiniteSets
+
+CONSTANTS Ids, Blobs, MaxLen, NoBlob
+
+VARIABLES
+    st,     \* [Ids -> {"none", "live", "deleted"}]
+    lg,     \* [Ids -> Seq(entry)]: each session's log
+    links,  \* [Ids -> SUBSET Blobs]: files present in {id}/blobs/
+    base,   \* [Ids -> Seq(entry)]: prefix copied at fork time (<<>> for roots)
+    lost    \* [Ids -> SUBSET Blobs]: blob files the disk lost in that session
+
+vars == <<st, lg, links, base, lost>>
+
+E(k, b) == [k |-> k, b |-> b]
+
+Count(l, k) == Cardinality({i \in 1..Len(l) : l[i].k = k})
+IsOpen(l) == Count(l, "start") > Count(l, "commit")
+
+TypeOK ==
+    /\ st \in [Ids -> {"none", "live", "deleted"}]
+    /\ links \in [Ids -> SUBSET Blobs]
+    /\ lost \in [Ids -> SUBSET Blobs]
+
+Init ==
+    /\ st = [s \in Ids |-> "none"]
+    /\ lg = [s \in Ids |-> <<>>]
+    /\ links = [s \in Ids |-> {}]
+    /\ base = [s \in Ids |-> <<>>]
+    /\ lost = [s \in Ids |-> {}]
+
+Create(s) ==
+    /\ st[s] = "none"
+    /\ st' = [st EXCEPT ![s] = "live"]
+    /\ lg' = [lg EXCEPT ![s] = <<E("created", NoBlob)>>]
+    /\ UNCHANGED <<links, base, lost>>
+
+Start(s) ==
+    /\ st[s] = "live"
+    /\ Len(lg[s]) < MaxLen
+    /\ ~IsOpen(lg[s])
+    /\ lg' = [lg EXCEPT ![s] = Append(@, E("start", NoBlob))]
+    /\ UNCHANGED <<st, links, base, lost>>
+
+Commit(s) ==
+    /\ st[s] = "live"
+    /\ Len(lg[s]) < MaxLen
+    /\ IsOpen(lg[s])
+    /\ lg' = [lg EXCEPT ![s] = Append(@, E("commit", NoBlob))]
+    /\ UNCHANGED <<st, links, base, lost>>
+
+\* put_blob(): the file is installed before any line can reference it.
+PutBlob(s, b) ==
+    /\ st[s] = "live"
+    /\ b \notin links[s]
+    /\ links' = [links EXCEPT ![s] = @ \cup {b}]
+    /\ UNCHANGED <<st, lg, base, lost>>
+
+\* append(item{blob}): the manager checks the blob exists in this session.
+Item(s, b) ==
+    /\ st[s] = "live"
+    /\ Len(lg[s]) < MaxLen
+    /\ IsOpen(lg[s])
+    /\ b \in links[s]
+    /\ lg' = [lg EXCEPT ![s] = Append(@, E("item", b))]
+    /\ UNCHANGED <<st, links, base, lost>>
+
+\* append(set{blobs}): a setting may list blobs, inside a turn or outside it,
+\* under the item's rule: the manager checks the blob exists in this
+\* session. fx writes such lines when it moves a session off its side folder
+\* (D47) and when its compactor keeps records (D50). One per session bounds
+\* the states; more such lines behave as more items do.
+SetBlob(s, b) ==
+    /\ st[s] = "live"
+    /\ Len(lg[s]) < MaxLen
+    /\ Count(lg[s], "set") = 0
+    /\ b \in links[s]
+    /\ lg' = [lg EXCEPT ![s] = Append(@, E("set", b))]
+    /\ UNCHANGED <<st, links, base, lost>>
+
+\* open(.fork{src, at}): only at a turn boundary, and only over lines
+\* whose blobs the source still has (`.last_good` ends before the first
+\* that names a lost one, D39). Line 1 is new; lines 2..at are copied
+\* unchanged; every source blob is hard-linked.
+Fork(src, f, at) ==
+    /\ st[src] = "live"
+    /\ st[f] = "none"
+    /\ at \in 1..Len(lg[src])
+    /\ ~IsOpen(SubSeq(lg[src], 1, at))
+    /\ \A i \in 2..at : lg[src][i].b # NoBlob => lg[src][i].b \in links[src]
+    /\ LET copied == SubSeq(lg[src], 2, at) IN
+          /\ lg' = [lg EXCEPT ![f] = <<E("created", NoBlob)>> \o copied]
+          /\ base' = [base EXCEPT ![f] = copied]
+    /\ links' = [links EXCEPT ![f] = links[src]]
+    /\ st' = [st EXCEPT ![f] = "live"]
+    /\ UNCHANGED lost
+
+\* delete(): the folder, its log and its blob links go away.
+Delete(s) ==
+    /\ st[s] = "live"
+    /\ st' = [st EXCEPT ![s] = "deleted"]
+    /\ lg' = [lg EXCEPT ![s] = <<>>]
+    /\ links' = [links EXCEPT ![s] = {}]
+    /\ lost' = [lost EXCEPT ![s] = {}]
+    /\ UNCHANGED base
+
+\* The disk loses one blob file of a live session (D39).
+Lose(s, b) ==
+    /\ st[s] = "live"
+    /\ b \in links[s]
+    /\ links' = [links EXCEPT ![s] = @ \ {b}]
+    /\ lost' = [lost EXCEPT ![s] = @ \cup {b}]
+    /\ UNCHANGED <<st, lg, base>>
+
+Next ==
+    \E s \in Ids :
+        \/ Create(s)
+        \/ Start(s)
+        \/ Commit(s)
+        \/ Delete(s)
+        \/ \E b \in Blobs : PutBlob(s, b) \/ Item(s, b) \/ SetBlob(s, b) \/ Lose(s, b)
+        \/ \E f \in Ids, at \in 1..MaxLen : Fork(s, f, at)
+
+Spec == Init /\ [][Next]_vars
+
+-----------------------------------------------------------------------------
+(* Invariants *)
+
+\* Every blob a live log references is present in that session, unless the
+\* disk lost it there: a fork never inherits a missing reference.
+RefsExist ==
+    \A s \in Ids : st[s] = "live" =>
+        \A i \in 1..Len(lg[s]) :
+            lg[s][i].b # NoBlob => lg[s][i].b \in links[s] \cup lost[s]
+
+\* A fork's copied prefix is intact, whatever happened to its source.
+ForkKeepsPrefix ==
+    \A f \in Ids : st[f] = "live" =>
+        SubSeq(lg[f], 2, Len(base[f]) + 1) = base[f]
+
+\* A fork never starts inside an open turn.
+ForkAtBoundary == \A f \in Ids : ~IsOpen(base[f])
+
+\* Line 1 of every live log is `created`.
+FirstLine == \A s \in Ids : st[s] = "live" => lg[s][1].k = "created"
+=============================================================================

src/core/session_manager/tla/Lifecycle.cfg

@@ -0,0 +1,7 @@
+SPECIFICATION Spec
+CONSTANT Ids = {s1, s2}
+INVARIANTS
+    TypeOK
+    VisibleHasLine1
+    AckedIsVisible
+    NothingBeforeFirstTurn

src/core/session_manager/tla/Lifecycle.tla

@@ -0,0 +1,135 @@
+---------------------------- MODULE Lifecycle ----------------------------
+(***************************************************************************)
+(* Step: L2 lazy creation and publish.                                    *)
+(*                                                                         *)
+(* open(.new) touches nothing on disk. The first turn builds .tmp/{id}:  *)
+(* mkdir, write line 1, fsync the log, rename to {id}, fsync the parent  *)
+(* directory, and only then returns to the caller. An fx crash stops    *)
+(* the sequence anywhere. A machine crash can also undo an unsynced rename,*)
+(* drop an unsynced mkdir, and drop line 1 if it was not fsynced.       *)
+(* Rebuild sweeps leftovers in .tmp.                                     *)
+(*                                                                         *)
+(* Design: system-design.md D2 and "Durable State And Schema" (publish).  *)
+(***************************************************************************)
+EXTENDS Naturals
+
+CONSTANT Ids
+
+Steps == {"idle", "mem", "tmpdir", "written", "synced", "renamed", "done", "dead"}
+
+VARIABLES
+    step,    \* [Ids -> Steps]: how far the first-turn publish has got
+    where,   \* [Ids -> {"none", "tmp", "visible"}]: the folder on disk
+    line1,   \* [Ids -> {"none", "cached", "durable"}]: line 1 on disk
+    acked    \* [Ids -> BOOLEAN]: the caller was told the save succeeded
+
+vars == <<step, where, line1, acked>>
+
+TypeOK ==
+    /\ step \in [Ids -> Steps]
+    /\ where \in [Ids -> {"none", "tmp", "visible"}]
+    /\ line1 \in [Ids -> {"none", "cached", "durable"}]
+    /\ acked \in [Ids -> BOOLEAN]
+
+Init ==
+    /\ step = [s \in Ids |-> "idle"]
+    /\ where = [s \in Ids |-> "none"]
+    /\ line1 = [s \in Ids |-> "none"]
+    /\ acked = [s \in Ids |-> FALSE]
+
+Advance(s, from, to) ==
+    /\ step[s] = from
+    /\ step' = [step EXCEPT ![s] = to]
+
+OpenNew(s) ==
+    /\ Advance(s, "idle", "mem")
+    /\ UNCHANGED <<where, line1, acked>>
+
+MkTmp(s) ==
+    /\ Advance(s, "mem", "tmpdir")
+    /\ where' = [where EXCEPT ![s] = "tmp"]
+    /\ UNCHANGED <<line1, acked>>
+
+WriteLine1(s) ==
+    /\ Advance(s, "tmpdir", "written")
+    /\ line1' = [line1 EXCEPT ![s] = "cached"]
+    /\ UNCHANGED <<where, acked>>
+
+FsyncLog(s) ==
+    /\ Advance(s, "written", "synced")
+    /\ line1' = [line1 EXCEPT ![s] = "durable"]
+    /\ UNCHANGED <<where, acked>>
+
+Rename(s) ==
+    /\ Advance(s, "synced", "renamed")
+    /\ where' = [where EXCEPT ![s] = "visible"]
+    /\ UNCHANGED <<line1, acked>>
+
+\* fsync of sessions/v2/ makes the rename durable; then append() returns.
+FsyncDirAndAck(s) ==
+    /\ Advance(s, "renamed", "done")
+    /\ acked' = [acked EXCEPT ![s] = TRUE]
+    /\ UNCHANGED <<where, line1>>
+
+\* fx dies: every unfinished first-turn publish stops; the disk keeps what it has.
+ProcessCrash ==
+    /\ \E s \in Ids : step[s] \notin {"idle", "done", "dead"}
+    /\ step' = [s \in Ids |-> IF step[s] \in {"idle", "done"} THEN step[s] ELSE "dead"]
+    /\ UNCHANGED <<where, line1, acked>>
+
+\* Machine crash (the PowerLoss action): like an fx crash, and unsynced directory changes and unsynced
+\* line 1 bytes may also be lost. An unsynced rename may be undone, and when
+\* the mkdir of .tmp/{id} was never synced either, the folder may be gone
+\* from both places. Unsynced line 1 bytes may vanish or survive; after the
+\* reboot, whatever survived is durable.
+PowerLoss ==
+    \E lose \in [Ids -> BOOLEAN], gone \in [Ids -> BOOLEAN], keep \in [Ids -> BOOLEAN] :
+        LET w == [s \in Ids |->
+                    CASE step[s] = "renamed" /\ lose[s] -> IF gone[s] THEN "none" ELSE "tmp"
+                      [] where[s] = "tmp" /\ step[s] # "done" /\ lose[s] -> "none"
+                      [] OTHER -> where[s]]
+        IN /\ where' = w
+           /\ line1' = [s \in Ids |->
+                          CASE w[s] = "none"                  -> "none"
+                            [] line1[s] = "cached" /\ keep[s] -> "durable"
+                            [] line1[s] = "cached"            -> "none"
+                            [] OTHER                          -> line1[s]]
+           /\ step' = [s \in Ids |->
+                          IF step[s] \in {"idle", "done"} THEN step[s] ELSE "dead"]
+           /\ UNCHANGED acked
+
+\* rebuild(): remove a leftover .tmp folder of a first-turn publish that died.
+Sweep(s) ==
+    /\ step[s] = "dead"
+    /\ where[s] = "tmp"
+    /\ where' = [where EXCEPT ![s] = "none"]
+    /\ line1' = [line1 EXCEPT ![s] = "none"]
+    /\ UNCHANGED <<step, acked>>
+
+Next ==
+    \/ \E s \in Ids :
+          \/ OpenNew(s)
+          \/ MkTmp(s)
+          \/ WriteLine1(s)
+          \/ FsyncLog(s)
+          \/ Rename(s)
+          \/ FsyncDirAndAck(s)
+          \/ Sweep(s)
+    \/ ProcessCrash
+    \/ PowerLoss
+
+Spec == Init /\ [][Next]_vars
+
+-----------------------------------------------------------------------------
+(* Invariants *)
+
+\* A visible session always has a durable first line.
+VisibleHasLine1 == \A s \in Ids : where[s] = "visible" => line1[s] = "durable"
+
+\* An acknowledged first turn stays visible, even after a machine crash.
+AckedIsVisible == \A s \in Ids : acked[s] => where[s] = "visible"
+
+\* open(.new) and settings held before the first turn never create anything on disk.
+NothingBeforeFirstTurn ==
+    \A s \in Ids : step[s] \in {"idle", "mem"} => where[s] = "none"
+=============================================================================

src/core/session_manager/tla/MoveSideFiles.cfg

@@ -0,0 +1,9 @@
+SPECIFICATION FairSpec
+CONSTANT Handles = {h1, h2, h3}
+INVARIANTS
+    TypeOK
+    Resolvable
+    TerminalKept
+    MapComplete
+PROPERTIES
+    EventuallyDone

src/core/session_manager/tla/MoveSideFiles.tla

@@ -0,0 +1,126 @@
+--------------------------- MODULE MoveSideFiles ---------------------------
+(***************************************************************************)
+(* Step: fx wiring, moving an older v2 session off its side folder (D47).  *)
+(*                                                                         *)
+(* An older v2 session keeps large bodies and its terminal state in       *)
+(* ~/.fx/session-files/{id}/. On its first writable open fx puts each     *)
+(* body as a blob, writes one batch holding the map from old handles to   *)
+(* blobs and the two settings, renames the terminal folder to             *)
+(* ~/.fx/terminal/{id}/, and removes the side folder. One writer at a     *)
+(* time holds the session (WriterLock), and a crash can stop it between   *)
+(* any two steps; the next open starts again from what the disk holds.    *)
+(* A reader may resolve any old handle at any moment: through the map     *)
+(* once it is written, through the side folder before.                    *)
+(*                                                                         *)
+(* Design: system-design.md D44 to D48.                                    *)
+(***************************************************************************)
+EXTENDS Naturals, FiniteSets
+
+CONSTANTS Handles
+
+VARIABLES
+    side,      \* SUBSET Handles: bodies still in the side folder
+    folder,    \* "present" | "removed": the side folder itself
+    blobs,     \* SUBSET Handles: bodies put as blobs of the session
+    mapped,    \* TRUE once the batch with the map and settings is durable
+    terminal,  \* "side" | "moved": where the terminal state lives
+    open       \* TRUE while a writer is running the move
+
+vars == <<side, folder, blobs, mapped, terminal, open>>
+
+TypeOK ==
+    /\ side \subseteq Handles
+    /\ folder \in {"present", "removed"}
+    /\ blobs \subseteq Handles
+    /\ mapped \in BOOLEAN
+    /\ terminal \in {"side", "moved"}
+    /\ open \in BOOLEAN
+
+Init ==
+    /\ side = Handles
+    /\ folder = "present"
+    /\ blobs = {}
+    /\ mapped = FALSE
+    /\ terminal = "side"
+    /\ open = FALSE
+
+\* A writable open takes the session; the move runs inside it.
+Open ==
+    /\ ~open
+    /\ open' = TRUE
+    /\ UNCHANGED <<side, folder, blobs, mapped, terminal>>
+
+\* put_blob() of one side body; repeating it is harmless (content addressed).
+PutBlob(h) ==
+    /\ open
+    /\ ~mapped
+    /\ h \in side
+    /\ blobs' = blobs \cup {h}
+    /\ UNCHANGED <<side, folder, mapped, terminal, open>>
+
+\* One durable batch: `set moved_files` listing every blob, and the settings.
+WriteMap ==
+    /\ open
+    /\ ~mapped
+    /\ blobs = Handles
+    /\ mapped' = TRUE
+    /\ UNCHANGED <<side, folder, blobs, terminal, open>>
+
+\* Rename session-files/{id}/terminal to terminal/{id}.
+MoveTerminal ==
+    /\ open
+    /\ mapped
+    /\ terminal = "side"
+    /\ terminal' = "moved"
+    /\ UNCHANGED <<side, folder, blobs, mapped, open>>
+
+\* Remove the side folder and everything left in it.
+RemoveSide ==
+    /\ open
+    /\ mapped
+    /\ terminal = "moved"
+    /\ folder = "present"
+    /\ folder' = "removed"
+    /\ side' = {}
+    /\ UNCHANGED <<blobs, mapped, terminal, open>>
+
+\* The writer stops: a clean close or a crash between any two steps.
+Stop ==
+    /\ open
+    /\ open' = FALSE
+    /\ UNCHANGED <<side, folder, blobs, mapped, terminal>>
+
+Done == folder = "removed"
+
+Next ==
+    \/ Open
+    \/ \E h \in Handles : PutBlob(h)
+    \/ WriteMap
+    \/ MoveTerminal
+    \/ RemoveSide
+    \/ Stop
+
+Spec == Init /\ [][Next]_vars
+
+\* Writers keep coming back, and a step enabled again and again eventually
+\* runs (a crash can stop any one open, not every open).
+FairSpec == Spec /\ WF_vars(Open) /\ SF_vars(WriteMap) /\ SF_vars(MoveTerminal)
+    /\ SF_vars(RemoveSide) /\ \A h \in Handles : SF_vars(PutBlob(h))
+
+-----------------------------------------------------------------------------
+(* Invariants *)
+
+\* Every old handle resolves at every moment: through the map once it is
+\* written, through the side folder before.
+Resolvable ==
+    \A h \in Handles : (mapped /\ h \in blobs) \/ (~mapped /\ h \in side)
+
+\* The terminal state is never lost: the side folder goes only after it moved.
+TerminalKept == folder = "removed" => terminal = "moved"
+
+\* The map names only bodies that exist as blobs.
+MapComplete == mapped => blobs = Handles
+
+\* Liveness under FairSpec: the move eventually finishes and stays finished.
+EventuallyDone == <>[]Done
+=============================================================================

src/core/session_manager/tla/README.md

@@ -0,0 +1,148 @@
+# TLA+ models
+
+One model per step of the design. Each one checks the protocol described in
+`../system-design.md`, not the Zig code. The bridge to the code is that every
+invariant below also becomes a test assertion for the step it models.
+
+**Status: all eight specs parse (SANY) and pass TLC. Each one also catches
+its planted bugs (`./mutants.py`).** Last run: 2026-09-27, TLC2 2.19 (rev
+5a47802), OpenJDK 27 on macOS arm64.
+
+| Spec | States generated | Distinct states | Search depth | Result |
+|---|---|---|---|---|
+| `SessionLog` | 686 | 110 | 15 | No error |
+| `TurnLifecycle` | 21,684 | 19,352 | 14 | No error |
+| `WriterLock` | 3,257 | 1,016 | 24 | No error |
+| `ResumeSnapshot` | 5,461 | 5,461 | 7 | No error |
+| `Fork` | 375,727 | 51,776 | 16 | No error |
+| `Subagents` | 204,097 | 120,297 | 23 | No error |
+| `Catalog` | 645,269 | 94,482 | 19 | No error |
+| `Lifecycle` | 9,553 | 144 | 13 | No error |
+
+Every run explored the whole bounded state space (0 states left on the queue).
+
+`Lifecycle`'s `PowerLoss` was widened on 2026-09-27, when trace validation
+compared it with real disk behavior. A renamed but unsynced publish may also
+vanish from both folders (when the `mkdir` of `.tmp/{id}` was never synced
+either), and unsynced line 1 bytes may survive as well as vanish. The spec
+still passes, and both of its mutants are still caught.
+
+`Catalog`'s `Rebuild` was widened the same day to keep a `del` for every
+tombstoned id after its fresh `put` lines, as the code does, so a deleted id
+stays deleted through a rebuild and cannot be re-imported. The spec still
+passes, and its mutant is still caught.
+
+`Subagents` was widened on 2026-09-27 for D22 (the pre-wiring API check):
+work numbers per child, at most one unfinished work item per child, `failed`
+finishes and a parent `cancelled`. `LostMeansNoLog` became an action
+property, checked on the step that writes the line, because a persistent
+child marked lost for one work item may create its log with a later one.
+
+`./mutants.py` plants 14 realistic bugs, one to three per spec, and requires
+TLC to report the matching invariant or action property as violated. All 14
+are caught:
+
+- fsync acknowledging a half-written line
+- open() keeping a torn tail
+- reopen skipping `turn_interrupted`
+- accepting an item outside a turn
+- open ignoring the flock
+- a snapshot with the wrong state
+- a fork forgetting blob links
+- a fork inside an open turn
+- repair marking every child lost
+- a spawn while the child's work is open
+- reopen skipping child repair
+- list skipping the folder check
+- rename before the line 1 fsync
+- ack before the directory fsync
+
+## The specs
+
+| Spec | Step (level) | What it proves | Invariants |
+|---|---|---|---|
+| `SessionLog.tla` | Log append, fsync, fx crash, machine crash, torn tail (L1) | Acknowledged lines survive a machine crash; only the final line can be torn; open() leaves no torn line | `SeqContiguous`, `OnlyTailTorn`, `AckedSurvive`, `OpenIsClean` |
+| `TurnLifecycle.tla` | Turn rules, close, crash, reopen (L2) | The manager only writes valid turn transitions; close and reopen never leave a stale open turn; the log is only ever extended | `StartsWithCreated`, `AtMostOneOpenTurn`, `ItemsInsideTurns`, `EndsCloseATurn`, `ClosedOnlyBetweenTurns`, `NoStaleTurnAfterReopen`, property `AppendOnly` |
+| `WriterLock.tla` | flock across processes, Session mutex across threads (L0, L2) | One writing process; file order equals seq order across threads and after takeover | `OneWriter`, `OnlyHolderOpen`, `MutexInsideOpenSession`, `SeqIsPosition` |
+| `ResumeSnapshot.tla` | Fold and resume from a snapshot (L2) | Resuming from the newest snapshot equals a full replay; snapshots can be dropped | `ResumeEqualsFullReplay`, `SnapshotsAreIgnorable` |
+| `Lifecycle.tla` | Lazy creation and publish (L2) | Nothing on disk before the first turn; a visible session has a durable line 1; an acknowledged first turn survives a machine crash | `VisibleHasLine1`, `AckedIsVisible`, `NothingBeforeFirstTurn` |
+| `Fork.tla` | Fork and blobs (L2) | Every referenced blob exists; a fork keeps its prefix after the source changes or is deleted; forks start at turn boundaries | `RefsExist`, `ForkKeepsPrefix`, `ForkAtBoundary`, `FirstLine` |
+| `Subagents.tla` | Children, persistent work, cancel, parent crash and repair (L2) | Every work item ends in a known state; one unfinished work item per child; `lost` only without a log; no orphan child logs | `OneOpenWork`, `FinishClosesOpenWork`, `NoOrphanChild`, `NoIndeterminate`, property `LostMeansNoLog` |
+| `Catalog.tla` | index.jsonl, list self-heal, delete, rebuild (L3) | list never returns a missing session; a deleted id never comes back; rebuild is exact | `ListedAreLive`, `NoResurrection`, `IndexNamesPublished`, property `RebuildIsExact` |
+
+Every spec also checks `TypeOK` where one is defined.
+
+**What the `PowerLoss` action means.** It models a machine crash: the OS
+goes down without flushing the page cache, and only synced bytes survive.
+With D3's plain `fsync`, that covers:
+
+- an OS crash (kernel panic or freeze) on every platform;
+- a power cut on Linux.
+
+A power cut on macOS can also lose recently synced data from the drive's own
+cache. D3 accepts that, and it is outside these models. The action keeps its
+name so the trace event contract and the mutants stay stable.
+
+## Running
+
+```sh
+./check.sh                  # all specs
+./check.sh SessionLog Fork  # some specs
+./mutants.py                # every planted bug must still be caught
+```
+
+Requirements:
+
+- OpenJDK: `brew install openjdk`. It is keg-only, so it is not on PATH;
+  both scripts find it at `/opt/homebrew/opt/openjdk/bin/java`.
+- `tla2tools.jar`: `~/.local/share/tla/tla2tools.jar`. Override the location
+  with `TLA2TOOLS_JAR`.
+
+`check.sh` runs TLC with `-deadlock`, because every model is bounded and stops
+at its bound, and it keeps TLC's state files outside this folder. When you add
+an invariant, add a mutant to `mutants.py` that breaks it.
+
+## Checking the code, not just the design
+
+The models above check the design. To check that the Zig code actually
+behaves like them, the code writes a trace of its steps in test builds, and
+TLC validates that trace against the same specs. See
+[trace/README.md](trace/README.md).
+
+```sh
+./trace/validate.sh SessionLog run.ndjson  # ACCEPTED, or REJECTED at step N
+./trace/selftest.sh                        # the validator must accept and reject
+```
+
+## What the models do not cover
+
+- Byte encoding, JSON parsing and line size caps. Those are covered by unit
+  tests.
+- Byte offsets. `Fork.tla` copies lines as values, so it cannot see that a
+  snapshot's `compaction_offset` moves when the fork's line 1 is longer; the
+  driver found that, and the fork now encodes each copied snapshot again
+  (`session.zig` test "a fork after a compaction and snapshots").
+- Which bytes open reads. `SessionLog.tla` recovers a whole log; the manager
+  reads only line 1, the newest snapshot and what follows, so older damage
+  is found by `read` and `verify` (`system-design.md` Reliability And
+  Recovery; the driver's bit-flip cells cover every region).
+- Code paths that no test runs. Trace validation (above) covers only the
+  runs we execute.
+- Performance. That is the benchmark in `../system-design.md` Performance
+  And Capacity.
+- The fx adapter and host policy, such as when to offer "continue". Those are
+  covered by fx E2E tests.
+- Liveness (for example "every child eventually finishes"). The models check
+  safety only. Liveness would need fairness assumptions about the model
+  provider, which the manager does not control.
+- Model bounds. Small bounds (2 or 3 ids, logs of 4 to 7 lines) find ordering
+  and crash-window bugs, but they do not prove behavior at every size. Raise
+  a bound in a spec's `.cfg` when a bug is suspected past it.
+
+## Keeping the models honest
+
+When a decision in `../system-design.md` changes, update the spec that models
+it in the same change. If TLC finds a counterexample:
+
+1. If the spec is wrong, fix the spec.
+2. If the design is wrong, fix `system-design.md` first, then the spec.

src/core/session_manager/tla/ResumeSnapshot.cfg

@@ -0,0 +1,8 @@
+SPECIFICATION Spec
+CONSTANTS
+    Vals = {v1, v2}
+    MaxLen = 6
+    NoVal = NoVal
+INVARIANTS
+    ResumeEqualsFullReplay
+    SnapshotsAreIgnorable

src/core/session_manager/tla/ResumeSnapshot.tla

@@ -0,0 +1,91 @@
+-------------------------- MODULE ResumeSnapshot --------------------------
+(***************************************************************************)
+(* Step: L2 fold and resume.                                              *)
+(*                                                                         *)
+(* open(.resume) folds from the newest snapshot instead of line 1. This  *)
+(* spec states the contract that makes that safe: resuming from the      *)
+(* newest snapshot gives exactly the state of a full replay, and the     *)
+(* snapshot lines themselves can be dropped without changing any state.  *)
+(* The Zig implementation must pass the same two checks as property      *)
+(* tests.                                                                 *)
+(*                                                                         *)
+(* Design: system-design.md "Fold".                                       *)
+(***************************************************************************)
+EXTENDS Naturals, Sequences
+
+CONSTANTS Vals, MaxLen, NoVal
+
+Empty == [pref |-> NoVal, turns |-> 0, open |-> FALSE]
+
+\* Every line has the same record shape; `st` is used only by snapshots.
+Entry(k, v, s) == [k |-> k, v |-> v, st |-> s]
+
+Step(s, e) ==
+    CASE e.k = "set"    -> [s EXCEPT !.pref = e.v]
+      [] e.k = "start"  -> [s EXCEPT !.open = TRUE]
+      [] e.k = "commit" -> [s EXCEPT !.open = FALSE, !.turns = @ + 1]
+      [] OTHER          -> s    \* snapshot lines change nothing
+
+RECURSIVE FoldFrom(_, _, _)
+FoldFrom(l, i, s) ==
+    IF i > Len(l) THEN s ELSE FoldFrom(l, i + 1, Step(s, l[i]))
+
+Full(l) == FoldFrom(l, 1, Empty)
+
+SnapIdx(l) == {i \in 1..Len(l) : l[i].k = "snap"}
+
+LastSnap(l) ==
+    IF SnapIdx(l) = {} THEN 0
+    ELSE CHOOSE i \in SnapIdx(l) : \A j \in SnapIdx(l) : j <= i
+
+\* What open(.resume) computes: the newest snapshot, then fold the tail.
+Resume(l) ==
+    LET j == LastSnap(l) IN
+    IF j = 0 THEN Full(l) ELSE FoldFrom(l, j + 1, l[j].st)
+
+RECURSIVE Strip(_)
+Strip(l) ==
+    IF l = <<>> THEN <<>>
+    ELSE IF Head(l).k = "snap" THEN Strip(Tail(l))
+         ELSE <<Head(l)>> \o Strip(Tail(l))
+
+VARIABLES log
+vars == <<log>>
+
+Init == log = <<>>
+
+Set(v) ==
+    /\ Len(log) < MaxLen
+    /\ log' = Append(log, Entry("set", v, Empty))
+
+Start ==
+    /\ Len(log) < MaxLen
+    /\ ~Full(log).open
+    /\ log' = Append(log, Entry("start", NoVal, Empty))
+
+Commit ==
+    /\ Len(log) < MaxLen
+    /\ Full(log).open
+    /\ log' = Append(log, Entry("commit", NoVal, Empty))
+
+\* The manager writes a snapshot of the state folded so far. Snapshots
+\* may land anywhere, including inside an open turn.
+Snapshot ==
+    /\ Len(log) < MaxLen
+    /\ log' = Append(log, Entry("snap", NoVal, Full(log)))
+
+Next ==
+    \/ \E v \in Vals : Set(v)
+    \/ Start
+    \/ Commit
+    \/ Snapshot
+
+Spec == Init /\ [][Next]_vars
+
+-----------------------------------------------------------------------------
+(* Invariants *)
+
+ResumeEqualsFullReplay == Resume(log) = Full(log)
+
+SnapshotsAreIgnorable == Full(Strip(log)) = Full(log)
+=============================================================================

src/core/session_manager/tla/SessionLog.cfg

@@ -0,0 +1,8 @@
+SPECIFICATION Spec
+CONSTANT MaxLines = 4
+INVARIANTS
+    TypeOK
+    SeqContiguous
+    OnlyTailTorn
+    AckedSurvive
+    OpenIsClean

src/core/session_manager/tla/SessionLog.tla

@@ -0,0 +1,122 @@
+---------------------------- MODULE SessionLog ----------------------------
+(***************************************************************************)
+(* Step: L1 log. One append-only log file.                                *)
+(*                                                                         *)
+(* Models write() into the page cache, fsync at a durability point, an fx *)
+(* crash (the kernel keeps every written byte), a machine crash (only the *)
+(* fsynced prefix is guaranteed; the rest may be lost and the new last    *)
+(* line may be torn) and the torn-tail cut plus fsync done by open().     *)
+(*                                                                         *)
+(* Design: system-design.md "Line format" and "Durable State And Schema". *)
+(***************************************************************************)
+EXTENDS Naturals, Sequences
+
+CONSTANT MaxLines
+
+VARIABLES
+    log,      \* file contents: a sequence of lines [seq, done]
+    durable,  \* length of the prefix that is on stable storage
+    acked,    \* number of lines a caller was told are durable
+    status    \* "open", "writing" or "down"
+
+vars == <<log, durable, acked, status>>
+
+Line(n, d) == [seq |-> n, done |-> d]
+
+LastDone == Len(log) = 0 \/ log[Len(log)].done
+
+TypeOK ==
+    /\ log \in Seq([seq : 1..MaxLines, done : BOOLEAN])
+    /\ Len(log) <= MaxLines
+    /\ durable \in 0..MaxLines
+    /\ acked \in 0..MaxLines
+    /\ status \in {"open", "writing", "down"}
+
+Init ==
+    /\ log = <<>>
+    /\ durable = 0
+    /\ acked = 0
+    /\ status = "open"
+
+(* write() starts: bytes are in the page cache, the newline is not yet. *)
+BeginWrite ==
+    /\ status = "open"
+    /\ Len(log) < MaxLines
+    /\ log' = Append(log, Line(Len(log) + 1, FALSE))
+    /\ status' = "writing"
+    /\ UNCHANGED <<durable, acked>>
+
+(* write() returns: the whole line, including its newline, is written. *)
+FinishWrite ==
+    /\ status = "writing"
+    /\ log' = [log EXCEPT ![Len(log)].done = TRUE]
+    /\ status' = "open"
+    /\ UNCHANGED <<durable, acked>>
+
+(* Durability point: fsync, then acknowledge to the caller. *)
+Fsync ==
+    /\ status = "open"
+    /\ durable' = Len(log)
+    /\ acked' = Len(log)
+    /\ UNCHANGED <<log, status>>
+
+(* fx dies. The kernel keeps every byte already written. *)
+ProcessCrash ==
+    /\ status \in {"open", "writing"}
+    /\ status' = "down"
+    /\ UNCHANGED <<log, durable, acked>>
+
+(* Machine crash (OS crash, or a power cut on Linux; D3 leaves a macOS   *)
+(* power cut outside the model): bytes after the durable prefix may be   *)
+(* lost, and the new                                                      *)
+(* last line may be torn.                                                *)
+PowerLoss ==
+    /\ \E k \in durable..Len(log), torn \in BOOLEAN :
+          LET kept == SubSeq(log, 1, k) IN
+          log' = IF torn /\ k > durable
+                    THEN [kept EXCEPT ![k].done = FALSE]
+                    ELSE kept
+    /\ status' = "down"
+    /\ UNCHANGED <<durable, acked>>
+
+(* open(.resume): cut a torn last line, fsync, accept writes again. *)
+Recover ==
+    /\ status = "down"
+    /\ LET repaired == IF LastDone THEN log ELSE SubSeq(log, 1, Len(log) - 1)
+       IN /\ log' = repaired
+          /\ durable' = Len(repaired)
+    /\ status' = "open"
+    /\ UNCHANGED acked
+
+Next ==
+    \/ BeginWrite
+    \/ FinishWrite
+    \/ Fsync
+    \/ ProcessCrash
+    \/ PowerLoss
+    \/ Recover
+
+Spec == Init /\ [][Next]_vars
+
+-----------------------------------------------------------------------------
+(* Invariants *)
+
+\* seq equals the line's position: no gaps and no duplicates.
+SeqContiguous == \A i \in 1..Len(log) : log[i].seq = i
+
+\* Only the final line can be incomplete.
+OnlyTailTorn == \A i \in 1..(Len(log) - 1) : log[i].done
+
+\* A line the caller was told is durable is never lost or torn.
+AckedSurvive ==
+    /\ acked <= durable
+    /\ durable <= Len(log)
+    /\ \A i \in 1..acked : log[i].done
+
+\* An open log never ends in a torn line.
+OpenIsClean == status = "open" => LastDone
+
+(* Note: after a machine crash, a line past `acked` can vanish and its seq *)
+(* is handed out again. Hosts must treat only acknowledged seqs as       *)
+(* stable (system-design.md "Acknowledged seq").                         *)
+=============================================================================

src/core/session_manager/tla/Subagents.cfg

@@ -0,0 +1,11 @@
+SPECIFICATION Spec
+CONSTANT Children = {c1, c2}
+CONSTANT MaxWork = 2
+INVARIANTS
+    TypeOK
+    OneOpenWork
+    FinishClosesOpenWork
+    NoOrphanChild
+    NoIndeterminate
+PROPERTY
+    LostMeansNoLog

src/core/session_manager/tla/Subagents.tla

@@ -0,0 +1,170 @@
+---------------------------- MODULE Subagents ----------------------------
+(***************************************************************************)
+(* Step: L2 children.                                                      *)
+(*                                                                         *)
+(* The parent log records child_spawned (durable) before the child's work *)
+(* starts. A child's first turn creates its own log; a persistent child's *)
+(* later work runs in that same log. The child thread appends             *)
+(* child_finished (ok or failed), or the parent cancels the work          *)
+(* (cancelled). A crash can land between any two steps. On parent reopen, *)
+(* the manager closes every unfinished work item: `lost` if the child has *)
+(* no log, `interrupted` if it has one.                                    *)
+(*                                                                         *)
+(* A child has at most one unfinished work item (D22); its later work     *)
+(* items are new spawn/finish pairs with the next work number. fx's       *)
+(* `data` on these lines is opaque to the manager and not modeled.        *)
+(*                                                                         *)
+(* Design: system-design.md kinds table, "Reliability And Recovery" and   *)
+(* D22.                                                                    *)
+(***************************************************************************)
+EXTENDS Naturals, Sequences, FiniteSets
+
+CONSTANTS Children, MaxWork
+
+VARIABLES
+    plog,       \* parent log: a sequence of [k, c, w, o]
+    childLog,   \* [Children -> BOOLEAN]: {c}/log.jsonl exists
+    thread,     \* [Children -> {"none", "starting", "running"}], in memory
+    up,         \* the fx process is running
+    repairing   \* reopen repair is in progress
+
+vars == <<plog, childLog, thread, up, repairing>>
+
+Outcomes == {"ok", "failed", "cancelled", "interrupted", "lost"}
+
+Count(s, k, c) == Cardinality({i \in 1..Len(s) : s[i].k = k /\ s[i].c = c})
+Works(c) == Count(plog, "spawned", c)
+Unfinished(c) == Works(c) > Count(plog, "finished", c)
+Spawned(c) == Works(c) > 0
+
+TypeOK ==
+    /\ \A i \in 1..Len(plog) :
+          /\ plog[i].k \in {"spawned", "finished"}
+          /\ plog[i].c \in Children
+          /\ plog[i].w \in 1..MaxWork
+          /\ plog[i].o \in Outcomes \cup {"none"}
+    /\ childLog \in [Children -> BOOLEAN]
+    /\ thread \in [Children -> {"none", "starting", "running"}]
+    /\ up \in BOOLEAN
+    /\ repairing \in BOOLEAN
+
+Init ==
+    /\ plog = <<>>
+    /\ childLog = [c \in Children |-> FALSE]
+    /\ thread = [c \in Children |-> "none"]
+    /\ up = TRUE
+    /\ repairing = FALSE
+
+Normal == up /\ ~repairing
+
+\* 1. The parent appends child_spawned (fsynced), then starts the thread.
+\*    Refused while the child still has unfinished work.
+Spawn(c) ==
+    /\ Normal
+    /\ ~Unfinished(c)
+    /\ Works(c) < MaxWork
+    /\ plog' = Append(plog, [k |-> "spawned", c |-> c, w |-> Works(c) + 1, o |-> "none"])
+    /\ thread' = [thread EXCEPT ![c] = "starting"]
+    /\ UNCHANGED <<childLog, up, repairing>>
+
+\* 2. The child's work starts a turn; the first one publishes its log.
+ChildStart(c) ==
+    /\ Normal
+    /\ thread[c] = "starting"
+    /\ childLog' = [childLog EXCEPT ![c] = TRUE]
+    /\ thread' = [thread EXCEPT ![c] = "running"]
+    /\ UNCHANGED <<plog, up, repairing>>
+
+\* 3. The child finishes and appends child_finished to the parent.
+ChildFinish(c) ==
+    /\ Normal
+    /\ thread[c] = "running"
+    /\ \E o \in {"ok", "failed"} :
+          plog' = Append(plog, [k |-> "finished", c |-> c, w |-> Works(c), o |-> o])
+    /\ thread' = [thread EXCEPT ![c] = "none"]
+    /\ UNCHANGED <<childLog, up, repairing>>
+
+\* 3'. The parent cancels the child's unfinished work and stops its thread.
+Cancel(c) ==
+    /\ Normal
+    /\ thread[c] \in {"starting", "running"}
+    /\ plog' = Append(plog, [k |-> "finished", c |-> c, w |-> Works(c), o |-> "cancelled"])
+    /\ thread' = [thread EXCEPT ![c] = "none"]
+    /\ UNCHANGED <<childLog, up, repairing>>
+
+\* The process dies anywhere. Durable lines stay; threads are gone.
+Crash ==
+    /\ up
+    /\ up' = FALSE
+    /\ thread' = [c \in Children |-> "none"]
+    /\ repairing' = FALSE
+    /\ UNCHANGED <<plog, childLog>>
+
+\* Parent reopen: repair runs before any normal work.
+Reopen ==
+    /\ ~up
+    /\ up' = TRUE
+    /\ repairing' = TRUE
+    /\ UNCHANGED <<plog, childLog, thread>>
+
+RepairChild(c) ==
+    /\ up
+    /\ repairing
+    /\ Unfinished(c)
+    /\ plog' = Append(plog, [k |-> "finished", c |-> c, w |-> Works(c),
+                             o |-> IF childLog[c] THEN "interrupted" ELSE "lost"])
+    /\ UNCHANGED <<childLog, thread, up, repairing>>
+
+RepairDone ==
+    /\ up
+    /\ repairing
+    /\ \A c \in Children : ~Unfinished(c)
+    /\ repairing' = FALSE
+    /\ UNCHANGED <<plog, childLog, thread, up>>
+
+Next ==
+    \/ \E c \in Children :
+          \/ Spawn(c)
+          \/ ChildStart(c)
+          \/ ChildFinish(c)
+          \/ Cancel(c)
+          \/ RepairChild(c)
+    \/ Crash
+    \/ Reopen
+    \/ RepairDone
+
+Spec == Init /\ [][Next]_vars
+
+-----------------------------------------------------------------------------
+(* Invariants *)
+
+\* A child has at most one unfinished work item.
+OneOpenWork ==
+    \A c \in Children :
+        Count(plog, "finished", c) <= Works(c) /\ Works(c) <= Count(plog, "finished", c) + 1
+
+\* Every child_finished closes that child's newest work item, which was
+\* unfinished until then: no finish before its spawn, none twice.
+FinishClosesOpenWork ==
+    \A i \in 1..Len(plog) :
+        plog[i].k = "finished" =>
+            LET p == SubSeq(plog, 1, i - 1) IN
+                /\ Count(p, "spawned", plog[i].c) = Count(p, "finished", plog[i].c) + 1
+                /\ plog[i].w = Count(p, "spawned", plog[i].c)
+
+\* A child log never exists without a spawn line in the parent.
+NoOrphanChild == \A c \in Children : childLog[c] => Spawned(c)
+
+\* `lost` is recorded only when the child really has no log at that moment.
+\* An action property: a persistent child marked lost for one work item may
+\* create its log with a later one.
+LostMeansNoLog ==
+    [][\A i \in (Len(plog) + 1)..Len(plog') :
+          (plog'[i].k = "finished" /\ plog'[i].o = "lost") => ~childLog[plog'[i].c]]_vars
+
+\* Outside repair, every unfinished work item has a live thread: no child
+\* is ever left in an unknown state.
+NoIndeterminate ==
+    Normal => \A c \in Children :
+        Unfinished(c) => thread[c] \in {"starting", "running"}
+=============================================================================

src/core/session_manager/tla/TurnLifecycle.cfg

@@ -0,0 +1,12 @@
+SPECIFICATION Spec
+CONSTANT MaxLen = 7
+INVARIANTS
+    TypeOK
+    StartsWithCreated
+    AtMostOneOpenTurn
+    ItemsInsideTurns
+    EndsCloseATurn
+    ClosedOnlyBetweenTurns
+    NoStaleTurnAfterReopen
+PROPERTIES
+    AppendOnly

src/core/session_manager/tla/TurnLifecycle.tla

@@ -0,0 +1,127 @@
+--------------------------- MODULE TurnLifecycle ---------------------------
+(***************************************************************************)
+(* Step: L2 turn rules, close, crash and reopen repair.                   *)
+(*                                                                         *)
+(* A host may ask for any kind in any order. The manager appends only     *)
+(* valid transitions and rejects the rest (InvalidTransition). close()   *)
+(* interrupts an open turn before `closed`. open(.resume) interrupts a    *)
+(* turn left open by a crash. Byte-level durability is SessionLog.tla's   *)
+(* job; here a crash keeps the log exactly as written. Every interrupt    *)
+(* reason (host: cancel, failed; manager: closed, crash) is one           *)
+(* "interrupt": the turn rules do not depend on it (D21).                 *)
+(*                                                                         *)
+(* Design: system-design.md kinds table and "Fold".                       *)
+(***************************************************************************)
+EXTENDS Naturals, Sequences, FiniteSets
+
+CONSTANT MaxLen
+
+HostKinds == {"start", "item", "compacted", "commit", "interrupt", "set"}
+Kinds == HostKinds \cup {"created", "closed"}
+
+VARIABLES
+    log,     \* the session log as a sequence of kinds
+    status,  \* "new", "open", "closed" or "down"
+    fresh    \* TRUE right after open(.resume), until the next turn starts
+
+vars == <<log, status, fresh>>
+
+Count(l, k) == Cardinality({i \in 1..Len(l) : l[i] = k})
+Ends(l) == Count(l, "commit") + Count(l, "interrupt")
+IsOpen(l) == Count(l, "start") > Ends(l)
+
+Prefix(a, b) == Len(a) <= Len(b) /\ SubSeq(b, 1, Len(a)) = a
+
+\* What the manager accepts from a host.
+Valid(l, k) ==
+    CASE k = "start"     -> ~IsOpen(l)
+      [] k = "item"      -> IsOpen(l)
+      [] k = "commit"    -> IsOpen(l)
+      [] k = "interrupt" -> IsOpen(l)
+      [] k = "compacted" -> TRUE
+      [] k = "set"       -> TRUE
+
+TypeOK ==
+    /\ log \in Seq(Kinds)
+    /\ status \in {"new", "open", "closed", "down"}
+    /\ fresh \in BOOLEAN
+
+Init ==
+    /\ log = <<>>
+    /\ status = "new"
+    /\ fresh = FALSE
+
+\* The first turn publishes the session with line 1 (D2).
+Create ==
+    /\ status = "new"
+    /\ log' = <<"created">>
+    /\ status' = "open"
+    /\ UNCHANGED fresh
+
+\* A host asks to append k; only valid kinds are written.
+Write(k) ==
+    /\ status = "open"
+    /\ Len(log) < MaxLen
+    /\ Valid(log, k)
+    /\ log' = Append(log, k)
+    /\ fresh' = (fresh /\ k # "start")
+    /\ UNCHANGED status
+
+\* close(): an open turn is interrupted, then `closed` is appended.
+Close ==
+    /\ status = "open"
+    /\ Len(log) + 2 <= MaxLen
+    /\ log' = IF IsOpen(log)
+                 THEN log \o <<"interrupt", "closed">>
+                 ELSE Append(log, "closed")
+    /\ status' = "closed"
+    /\ fresh' = FALSE
+
+\* fx dies with the session open.
+Crash ==
+    /\ status = "open"
+    /\ status' = "down"
+    /\ UNCHANGED <<log, fresh>>
+
+\* open(.resume): a turn left open by a crash gets turn_interrupted.
+Reopen ==
+    /\ status \in {"closed", "down"}
+    /\ Len(log) < MaxLen
+    /\ log' = IF IsOpen(log) THEN Append(log, "interrupt") ELSE log
+    /\ status' = "open"
+    /\ fresh' = TRUE
+
+Next ==
+    \/ Create
+    \/ \E k \in HostKinds : Write(k)
+    \/ Close
+    \/ Crash
+    \/ Reopen
+
+Spec == Init /\ [][Next]_vars
+
+-----------------------------------------------------------------------------
+(* Invariants *)
+
+StartsWithCreated == Len(log) > 0 => log[1] = "created"
+
+AtMostOneOpenTurn == Count(log, "start") - Ends(log) \in {0, 1}
+
+ItemsInsideTurns ==
+    \A i \in 1..Len(log) :
+        log[i] = "item" => IsOpen(SubSeq(log, 1, i - 1))
+
+EndsCloseATurn ==
+    \A i \in 1..Len(log) :
+        log[i] \in {"commit", "interrupt"} => IsOpen(SubSeq(log, 1, i - 1))
+
+ClosedOnlyBetweenTurns ==
+    \A i \in 1..Len(log) :
+        log[i] = "closed" => ~IsOpen(SubSeq(log, 1, i - 1))
+
+\* After open(.resume), no turn from the previous owner is still open.
+NoStaleTurnAfterReopen == fresh => ~IsOpen(log)
+
+(* Action property: the log is only ever extended, never rewritten. *)
+AppendOnly == [][Prefix(log, log')]_vars
+=============================================================================

src/core/session_manager/tla/V1Conversion.cfg

@@ -0,0 +1,36 @@
+SPECIFICATION FairSpec
+CONSTANTS
+    Procs = {p1, p2}
+    RootId = RootId
+    ChildId = ChildId
+    NewIds = {n}
+    None = None
+    Torn = Torn
+    MaxV = 2
+    MaxLocks = 2
+    MaxExtra = 1
+    MaxCrash = 2
+    MaxReq = 3
+    AvoidV1Ids = TRUE
+INVARIANTS
+    TypeOK
+    LockHeld
+    NoStaleConvLock
+    CopyIsCurrent
+    NoTornImport
+    NoShadow
+    ChildrenLanded
+    OrphansKeepV1
+    UsageKept
+    NoDanglingMark
+PROPERTIES
+    AnsweredWhole
+    NoFalseNotFound
+    NothingHalfConverted
+    NoLossOnDelete
+    LeftoversGone
+    ConverterOnlyDeletes
+    ConvertsOnlyOnRequest
+    RootsStick
+    ChildrenStick
+    RequestsAnswered

src/core/session_manager/tla/V1Conversion.mutants.cfg

@@ -0,0 +1,36 @@
+SPECIFICATION FairSpec
+CONSTANTS
+    Procs = {p1, p2}
+    RootId = RootId
+    ChildId = ChildId
+    NewIds = {n}
+    None = None
+    Torn = Torn
+    MaxV = 2
+    MaxLocks = 1
+    MaxExtra = 1
+    MaxCrash = 1
+    MaxReq = 2
+    AvoidV1Ids = TRUE
+INVARIANTS
+    TypeOK
+    LockHeld
+    NoStaleConvLock
+    CopyIsCurrent
+    NoTornImport
+    NoShadow
+    ChildrenLanded
+    OrphansKeepV1
+    UsageKept
+    NoDanglingMark
+PROPERTIES
+    AnsweredWhole
+    NoFalseNotFound
+    NothingHalfConverted
+    NoLossOnDelete
+    LeftoversGone
+    ConverterOnlyDeletes
+    ConvertsOnlyOnRequest
+    RootsStick
+    ChildrenStick
+    RequestsAnswered

src/core/session_manager/tla/V1Conversion.tla

@@ -0,0 +1,612 @@
+---------------------------- MODULE V1Conversion ----------------------------
+(***************************************************************************)
+(* Step: v1 sessions convert to v2 when they are opened (D55, D56, D59,   *)
+(* D60, D61).                                                              *)
+(*                                                                         *)
+(* Processes of the new build (Procs) each ask to open a root id, or the  *)
+(* convert-all command asks for it. If v2 holds the id, the request is    *)
+(* answered at once, after deleting any v1 folder of the family a crash   *)
+(* left behind that is unchanged since it was copied. If only v1 holds   *)
+(* it, the process converts the family, the root and the child sessions  *)
+(* in its registry, before it answers: it takes the v1 lock of every     *)
+(* member (a held one answers "busy"), and only then clears the family's *)
+(* crash leftovers in .tmp and stages a copy of each member (an          *)
+(* unreadable member answers "unreadable" and drops the staging). A      *)
+(* child an earlier, crashed conversion already published is reused as  *)
+(* it is. It publishes the children and then the root, deletes each      *)
+(* member's v1 folder under its lock while that folder is the version   *)
+(* its copy holds (D60), and releases the locks. A delete the file      *)
+(* system refuses leaves the folder and still answers. Nothing converts *)
+(* without a request, and the converter writes no v1 file: it only      *)
+(* deletes a folder whose copy is published.                             *)
+(*                                                                         *)
+(* Older builds keep writing v1 sessions throughout: a writer holds a     *)
+(* session's lock while it has the session open, and a write in progress *)
+(* leaves the files torn. The new build creates fresh v2 sessions and    *)
+(* appends to any v2 root. Any process can crash at any step: a crash    *)
+(* drops every lock it held and leaves staging, published children and  *)
+(* undeleted v1 folders behind.                                           *)
+(*                                                                         *)
+(* Rule R1 (AvoidV1Ids): a fresh v2 session never takes the id of a live  *)
+(* v1 session. Assumption A1: an older build never creates a v1 session   *)
+(* under an id v2 holds (ids are 72 random bits).                         *)
+(*                                                                         *)
+(* Converted once per id (D55): a v1 folder an older build changed after  *)
+(* its copy was made is never converted again or deleted, so v1ver may   *)
+(* run ahead of base.                                                      *)
+(*                                                                         *)
+(* Design: system-design.md D53 to D57 and D59 to D61.                     *)
+(***************************************************************************)
+EXTENDS Naturals, FiniteSets
+
+CONSTANTS
+    Procs,      \* processes of the new build
+    RootId,     \* a v1 root session
+    ChildId,    \* a child session in that root's registry
+    NewIds,     \* ids only fresh v2 sessions can take
+    None,
+    Torn,       \* the copy of a member read while a writer was mid-write
+    MaxV,       \* versions a v1 session reaches
+    MaxLocks,   \* times a writer opens one session
+    MaxExtra,   \* v2 turns appended to one session
+    MaxCrash,   \* crashes and refused deletes in one behavior
+    MaxReq,     \* open and convert-all requests in one behavior
+    AvoidV1Ids  \* rule R1
+
+Ids == {RootId, ChildId}
+Parent == [i \in Ids |-> IF i = ChildId THEN RootId ELSE None]
+ASSUME RootId # ChildId /\ Ids \cap NewIds = {} /\ Procs \cap {"free", "writer"} = {}
+
+AllIds == Ids \cup NewIds
+Roots == {i \in Ids : Parent[i] = None}
+Children(r) == {c \in Ids : Parent[c] = r}
+Fam(r) == {r} \cup Children(r)
+
+Kinds == {"none", "open", "all"}
+Answers == {"none", "opened", "converted", "busy", "unreadable", "notfound"}
+Status == {"none", "import", "fresh"}
+
+VARIABLES
+    v1ver,      \* [Ids -> 0..MaxV]: 0 absent, else the version of its files
+    v1lock,     \* [Ids -> {"free", "writer"} \cup Procs]
+    writing,    \* [Ids -> BOOLEAN]: a writer is mid-write; the files are torn
+    locks,      \* [Ids -> 0..MaxLocks]: times a writer took the lock
+    bad,        \* [Ids -> BOOLEAN]: the member's v1 files cannot be read
+    pub,        \* [AllIds -> Status]: the id in v2
+    base,       \* [AllIds -> 0..MaxV \cup {Torn}]: the version a conversion
+                \* copied, which the v2 copy records as its fingerprint
+    staged,     \* [Ids -> BOOLEAN]: a copy in .tmp
+    stagedBase, \* [Ids -> 0..MaxV \cup {Torn}]
+    extra,      \* [AllIds -> 0..MaxExtra]: v2 turns appended since publish
+    conv,       \* [Procs -> the converter: pc, the family root, its locked
+                \* members, and those it copied in this run]
+    req,        \* [Procs -> the request being answered: kind and root]
+    out,        \* [Procs -> the answer to the latest request: ans and root]
+    refused,    \* [Procs -> SUBSET Ids]: deletes refused in the current request
+    reqs,       \* requests made
+    crashes,
+    famOf,      \* [Roots -> SUBSET Ids]: the members a root's conversion covered
+    mark1,      \* [Ids -> BOOLEAN]: v1's usage marker, ~/.fx/usage-recovery/{id}
+    mark2,      \* [Ids -> BOOLEAN]: v2's usage marker, ~/.fx/usage-recovery-v2/{id}
+    owed        \* [Ids -> BOOLEAN]: ghost: the member has usage still to settle
+
+vars == <<v1ver, v1lock, writing, locks, bad, pub, base, staged, stagedBase,
+          extra, conv, req, out, refused, reqs, crashes, famOf, mark1, mark2, owed>>
+
+marks == <<mark1, mark2, owed>>
+
+Idle == [pc |-> "idle", root |-> None, members |-> {}, copied |-> {}]
+NoReq == [kind |-> "none", root |-> None]
+
+TypeOK ==
+    /\ v1ver \in [Ids -> 0..MaxV]
+    /\ v1lock \in [Ids -> {"free", "writer"} \cup Procs]
+    /\ writing \in [Ids -> BOOLEAN]
+    /\ locks \in [Ids -> 0..MaxLocks]
+    /\ bad \in [Ids -> BOOLEAN]
+    /\ pub \in [AllIds -> Status]
+    /\ base \in [AllIds -> (0..MaxV) \cup {Torn}]
+    /\ staged \in [Ids -> BOOLEAN]
+    /\ stagedBase \in [Ids -> (0..MaxV) \cup {Torn}]
+    /\ extra \in [AllIds -> 0..MaxExtra]
+    /\ \A p \in Procs :
+         /\ conv[p].pc \in {"idle", "locked", "staged", "published"}
+         /\ conv[p].root \in Roots \cup {None}
+         /\ conv[p].members \subseteq Ids /\ conv[p].copied \subseteq conv[p].members
+         /\ req[p].kind \in Kinds /\ req[p].root \in Roots \cup {None}
+         /\ out[p].ans \in Answers /\ out[p].root \in Roots \cup {None}
+         /\ refused[p] \subseteq Ids
+    /\ reqs \in 0..MaxReq
+    /\ crashes \in 0..MaxCrash
+    /\ famOf \in [Roots -> SUBSET Ids]
+    /\ mark1 \in [Ids -> BOOLEAN] /\ mark2 \in [Ids -> BOOLEAN] /\ owed \in [Ids -> BOOLEAN]
+
+Live(i) == pub[i] \in {"import", "fresh"}
+
+\* A published child whose root is not published: a crash's leftover, which
+\* the next conversion of its family reuses as it is.
+Orphan(i) == Parent[i] # None /\ pub[i] = "import" /\ pub[Parent[i]] = "none"
+Dirty == \E i \in Ids : staged[i]
+
+\* A v1 folder a crash or a refused delete left behind, unchanged since its
+\* copy (damage changes its fingerprint too), free, and not refused in p's
+\* current request: p's open deletes it.
+Leftover(p, i) ==
+    /\ pub[i] = "import" /\ v1ver[i] > 0 /\ v1ver[i] = base[i] /\ ~bad[i]
+    /\ v1lock[i] = "free" /\ i \notin refused[p]
+
+\* What the picker and `fx sessions` list: v2 roots, and v1 roots v2 does not
+\* hold; children are internal.
+Listed ==
+    {r \in Roots : Live(r) \/ (pub[r] = "none" /\ v1ver[r] > 0)}
+        \cup {n \in NewIds : Live(n)}
+
+Init ==
+    /\ v1ver = [i \in Ids |-> 0]
+    /\ v1lock = [i \in Ids |-> "free"]
+    /\ writing = [i \in Ids |-> FALSE]
+    /\ locks = [i \in Ids |-> 0]
+    /\ bad = [i \in Ids |-> FALSE]
+    /\ pub = [i \in AllIds |-> "none"]
+    /\ base = [i \in AllIds |-> 0]
+    /\ staged = [i \in Ids |-> FALSE]
+    /\ stagedBase = [i \in Ids |-> 0]
+    /\ extra = [i \in AllIds |-> 0]
+    /\ conv = [p \in Procs |-> Idle]
+    /\ req = [p \in Procs |-> NoReq]
+    /\ out = [p \in Procs |-> [ans |-> "none", root |-> None]]
+    /\ refused = [p \in Procs |-> {}]
+    /\ reqs = 0
+    /\ crashes = 0
+    /\ famOf = [r \in Roots |-> {}]
+    /\ mark1 = [i \in Ids |-> FALSE]
+    /\ mark2 = [i \in Ids |-> FALSE]
+    /\ owed = [i \in Ids |-> FALSE]
+
+(* -- v1 writers: older builds *)
+
+WCreate(i) ==
+    /\ v1ver[i] = 0
+    /\ Parent[i] # None => v1ver[Parent[i]] > 0
+    /\ pub[i] = "none"                                   \* A1
+    /\ v1ver' = [v1ver EXCEPT ![i] = 1]
+    /\ UNCHANGED <<v1lock, writing, locks, bad, pub, base, staged, stagedBase,
+                   extra, conv, req, out, refused, reqs, crashes, famOf>>
+    /\ UNCHANGED marks
+
+WLock(i) ==
+    /\ v1ver[i] > 0
+    /\ v1lock[i] = "free"
+    /\ locks[i] < MaxLocks
+    /\ v1lock' = [v1lock EXCEPT ![i] = "writer"]
+    /\ locks' = [locks EXCEPT ![i] = @ + 1]
+    /\ UNCHANGED <<v1ver, writing, bad, pub, base, staged, stagedBase, extra,
+                   conv, req, out, refused, reqs, crashes, famOf>>
+    /\ UNCHANGED marks
+
+WBegin(i) ==
+    /\ v1lock[i] = "writer"
+    /\ ~writing[i]
+    /\ v1ver[i] < MaxV
+    /\ writing' = [writing EXCEPT ![i] = TRUE]
+    /\ UNCHANGED <<v1ver, v1lock, locks, bad, pub, base, staged, stagedBase,
+                   extra, conv, req, out, refused, reqs, crashes, famOf>>
+    /\ UNCHANGED marks
+
+WEnd(i) ==
+    /\ writing[i]
+    /\ writing' = [writing EXCEPT ![i] = FALSE]
+    /\ v1ver' = [v1ver EXCEPT ![i] = @ + 1]
+    /\ UNCHANGED <<v1lock, locks, bad, pub, base, staged, stagedBase, extra,
+                   conv, req, out, refused, reqs, crashes, famOf>>
+    /\ UNCHANGED marks
+
+WUnlock(i) ==
+    /\ v1lock[i] = "writer"
+    /\ ~writing[i]
+    /\ v1lock' = [v1lock EXCEPT ![i] = "free"]
+    /\ UNCHANGED <<v1ver, writing, locks, bad, pub, base, staged, stagedBase,
+                   extra, conv, req, out, refused, reqs, crashes, famOf>>
+    /\ UNCHANGED marks
+
+\* A writer dies: the kernel drops its lock, and v1's own open repairs a torn
+\* write back to the last whole version.
+WCrash(i) ==
+    /\ v1lock[i] = "writer"
+    /\ crashes < MaxCrash
+    /\ v1lock' = [v1lock EXCEPT ![i] = "free"]
+    /\ writing' = [writing EXCEPT ![i] = FALSE]
+    /\ crashes' = crashes + 1
+    /\ UNCHANGED <<v1ver, locks, bad, pub, base, staged, stagedBase, extra,
+                   conv, req, out, refused, reqs, famOf>>
+    /\ UNCHANGED marks
+
+\* An older build ends a turn whose usage is not settled yet: it keeps v1's
+\* usage marker, under its lock.
+WMark(i) ==
+    /\ v1lock[i] = "writer"
+    /\ ~mark1[i]
+    /\ mark1' = [mark1 EXCEPT ![i] = TRUE]
+    /\ owed' = [owed EXCEPT ![i] = TRUE]
+    /\ UNCHANGED <<v1ver, v1lock, writing, locks, bad, pub, base, staged, stagedBase,
+                   extra, conv, req, out, refused, reqs, crashes, famOf, mark2>>
+
+\* A member's v1 files become unreadable: damage from outside fx.
+Damage(i) ==
+    /\ v1ver[i] > 0
+    /\ ~bad[i]
+    /\ bad' = [bad EXCEPT ![i] = TRUE]
+    /\ UNCHANGED <<v1ver, v1lock, writing, locks, pub, base, staged,
+                   stagedBase, extra, conv, req, out, refused, reqs, crashes, famOf>>
+    /\ UNCHANGED marks
+
+(* -- the new build's own v2 sessions *)
+
+FCreate(i) ==
+    /\ i \in NewIds \/ (i \in Roots /\ (AvoidV1Ids => v1ver[i] = 0))
+    /\ pub[i] = "none"
+    /\ i \in Ids => ~staged[i]
+    /\ pub' = [pub EXCEPT ![i] = "fresh"]
+    /\ UNCHANGED <<v1ver, v1lock, writing, locks, bad, base, staged,
+                   stagedBase, extra, conv, req, out, refused, reqs, crashes, famOf>>
+    /\ UNCHANGED marks
+
+FAppend(i) ==
+    /\ Live(i)
+    /\ i \in NewIds \/ i \in Roots
+    /\ extra[i] < MaxExtra
+    /\ extra' = [extra EXCEPT ![i] = @ + 1]
+    /\ UNCHANGED <<v1ver, v1lock, writing, locks, bad, pub, base, staged,
+                   stagedBase, conv, req, out, refused, reqs, crashes, famOf>>
+    /\ UNCHANGED marks
+
+(* -- requests and the converter, in each requesting process *)
+
+Request(p, k, r) ==
+    /\ k \in {"open", "all"}
+    /\ req[p] = NoReq
+    /\ conv[p] = Idle
+    /\ reqs < MaxReq
+    /\ req' = [req EXCEPT ![p] = [kind |-> k, root |-> r]]
+    /\ out' = [out EXCEPT ![p] = [ans |-> "none", root |-> r]]
+    /\ refused' = [refused EXCEPT ![p] = {}]
+    /\ reqs' = reqs + 1
+    /\ UNCHANGED <<v1ver, v1lock, writing, locks, bad, pub, base, staged,
+                   stagedBase, extra, conv, crashes, famOf>>
+    /\ UNCHANGED marks
+
+Answer(p, a) ==
+    /\ req' = [req EXCEPT ![p] = NoReq]
+    /\ out' = [out EXCEPT ![p] = [ans |-> a, root |-> req[p].root]]
+
+Done(p) == IF req[p].kind = "open" THEN "opened" ELSE "converted"
+
+Waiting(p) == req[p] # NoReq /\ conv[p] = Idle
+
+\* v2 already holds the id: any leftover of its family is cleaned first.
+AHeld(p) ==
+    /\ Waiting(p)
+    /\ Live(req[p].root)
+    /\ ~\E i \in Fam(req[p].root) : Leftover(p, i)
+    /\ Answer(p, Done(p))
+    /\ UNCHANGED <<v1ver, v1lock, writing, locks, bad, pub, base, staged,
+                   stagedBase, extra, conv, refused, reqs, crashes, famOf>>
+    /\ UNCHANGED marks
+
+\* A leftover v1 folder, unchanged since its copy, is deleted under its lock.
+CClean(p, i) ==
+    /\ Waiting(p)
+    /\ Live(req[p].root)
+    /\ i \in Fam(req[p].root)
+    /\ Leftover(p, i) /\ ~mark1[i]
+    /\ v1ver' = [v1ver EXCEPT ![i] = 0]
+    /\ UNCHANGED <<v1lock, writing, locks, bad, pub, base, staged,
+                   stagedBase, extra, conv, req, out, refused, reqs, crashes, famOf>>
+    /\ UNCHANGED marks
+
+\* The file system refuses that delete: the folder stays, the open goes on.
+CCleanRefused(p, i) ==
+    /\ Waiting(p)
+    /\ Live(req[p].root)
+    /\ i \in Fam(req[p].root)
+    /\ Leftover(p, i)
+    /\ crashes < MaxCrash
+    /\ refused' = [refused EXCEPT ![p] = @ \cup {i}]
+    /\ crashes' = crashes + 1
+    /\ UNCHANGED <<v1ver, v1lock, writing, locks, bad, pub, base, staged,
+                   stagedBase, extra, conv, req, out, reqs, famOf>>
+    /\ UNCHANGED marks
+
+\* Neither store holds it.
+AMissing(p) ==
+    /\ Waiting(p)
+    /\ pub[req[p].root] = "none" /\ v1ver[req[p].root] = 0
+    /\ Answer(p, IF req[p].kind = "open" THEN "notfound" ELSE "converted")
+    /\ UNCHANGED <<v1ver, v1lock, writing, locks, bad, pub, base, staged,
+                   stagedBase, extra, conv, refused, reqs, crashes, famOf>>
+    /\ UNCHANGED marks
+
+\* Takes every present member's lock, or answers "busy" holding none. The
+\* check that v2 does not hold the root is made under the locks: another
+\* process may have converted it while this one waited.
+CBegin(p) ==
+    LET r == req[p].root
+        present == {i \in Fam(r) : v1ver[i] > 0} IN
+    /\ Waiting(p)
+    /\ pub[r] = "none" /\ v1ver[r] > 0
+    /\ IF \A i \in present : v1lock[i] = "free"
+       THEN /\ v1lock' = [i \in Ids |-> IF i \in present THEN p ELSE v1lock[i]]
+            /\ conv' = [conv EXCEPT ![p] = [pc |-> "locked", root |-> r, members |-> present, copied |-> {}]]
+            /\ UNCHANGED <<req, out>>
+       ELSE /\ Answer(p, "busy")
+            /\ UNCHANGED <<v1lock, conv>>
+    /\ UNCHANGED <<v1ver, writing, locks, bad, pub, base, staged,
+                   stagedBase, extra, refused, reqs, crashes, famOf>>
+    /\ UNCHANGED marks
+
+\* Under the locks: the family's staging leftovers go, and each member not
+\* already published gets a fresh copy in .tmp; an unreadable member drops
+\* the staging and answers "unreadable".
+CStage(p) ==
+    LET m == conv[p].members
+        copy == {i \in m : pub[i] = "none"} IN
+    /\ conv[p].pc = "locked"
+    /\ IF \E i \in copy : bad[i]
+       THEN /\ v1lock' = [i \in Ids |-> IF i \in m THEN "free" ELSE v1lock[i]]
+            /\ staged' = [i \in Ids |-> IF i \in Fam(conv[p].root) THEN FALSE ELSE staged[i]]
+            /\ conv' = [conv EXCEPT ![p] = Idle]
+            /\ Answer(p, "unreadable")
+            /\ UNCHANGED stagedBase
+       ELSE /\ staged' = [i \in Ids |-> IF i \in Fam(conv[p].root) THEN i \in copy ELSE staged[i]]
+            /\ stagedBase' = [i \in Ids |->
+                                IF i \in copy
+                                THEN (IF writing[i] THEN Torn ELSE v1ver[i])
+                                ELSE stagedBase[i]]
+            /\ conv' = [conv EXCEPT ![p].pc = "staged", ![p].copied = copy]
+            /\ UNCHANGED <<v1lock, req, out>>
+    /\ UNCHANGED <<v1ver, writing, locks, bad, pub, base, extra, refused,
+                   reqs, crashes, famOf>>
+    /\ UNCHANGED marks
+
+\* Publishing is the manager's atomic rename.
+CPublishChild(p, c) ==
+    /\ conv[p].pc = "staged"
+    /\ c \in conv[p].members \ {conv[p].root}
+    /\ staged[c]
+    /\ staged' = [staged EXCEPT ![c] = FALSE]
+    /\ pub' = [pub EXCEPT ![c] = "import"]
+    /\ base' = [base EXCEPT ![c] = stagedBase[c]]
+    /\ UNCHANGED <<v1ver, v1lock, writing, locks, bad, stagedBase, extra, conv,
+                   req, out, refused, reqs, crashes, famOf>>
+    /\ UNCHANGED marks
+
+CPublishRoot(p) ==
+    LET r == conv[p].root IN
+    /\ conv[p].pc = "staged"
+    /\ \A c \in conv[p].members \ {r} : ~staged[c]
+    /\ staged' = [staged EXCEPT ![r] = FALSE]
+    /\ pub' = [pub EXCEPT ![r] = "import"]
+    /\ base' = [base EXCEPT ![r] = stagedBase[r]]
+    /\ conv' = [conv EXCEPT ![p].pc = "published"]
+    /\ famOf' = [famOf EXCEPT ![r] = conv[p].members]
+    /\ UNCHANGED <<v1ver, v1lock, writing, locks, bad, stagedBase, extra, req,
+                   out, refused, reqs, crashes>>
+    /\ UNCHANGED marks
+
+\* A member whose v1 state p may move to v2 and remove: one it copied in
+\* this run, or a reused child still at its copy's version and fingerprint.
+Unchanged(p, i) ==
+    /\ i \in conv[p].members /\ v1ver[i] > 0 /\ v1ver[i] = base[i]
+    /\ i \in conv[p].copied \/ ~bad[i]
+
+\* Its folder goes once its usage marker has moved (D62).
+Deletable(p, i) == Unchanged(p, i) /\ ~mark1[i]
+
+\* Where p moves a member's usage marker: after it published that member's
+\* family, or for a leftover of a family v2 already holds.
+MarkScope(p, i) ==
+    \/ conv[p].pc = "published" /\ Unchanged(p, i)
+    \/ Waiting(p) /\ Live(req[p].root) /\ i \in Fam(req[p].root) /\ Leftover(p, i)
+
+\* The v2 marker is written first, then v1's is removed: usage to settle is
+\* always behind one of them, and settling both is idempotent.
+MoveMark(p, i) ==
+    /\ MarkScope(p, i)
+    /\ mark1[i] /\ ~mark2[i]
+    /\ mark2' = [mark2 EXCEPT ![i] = TRUE]
+    /\ UNCHANGED <<v1ver, v1lock, writing, locks, bad, pub, base, staged, stagedBase,
+                   extra, conv, req, out, refused, reqs, crashes, famOf, mark1, owed>>
+
+DropMark(p, i) ==
+    /\ MarkScope(p, i)
+    /\ mark1[i] /\ mark2[i]
+    /\ mark1' = [mark1 EXCEPT ![i] = FALSE]
+    /\ UNCHANGED <<v1ver, v1lock, writing, locks, bad, pub, base, staged, stagedBase,
+                   extra, conv, req, out, refused, reqs, crashes, famOf, mark2, owed>>
+
+\* D60: with the copy durable, each member's v1 folder goes, still locked.
+CDelete(p, i) ==
+    /\ conv[p].pc = "published"
+    /\ Deletable(p, i)
+    /\ i \notin refused[p]
+    /\ v1ver' = [v1ver EXCEPT ![i] = 0]
+    /\ UNCHANGED <<v1lock, writing, locks, bad, pub, base, staged, stagedBase,
+                   extra, conv, req, out, refused, reqs, crashes, famOf>>
+    /\ UNCHANGED marks
+
+\* The file system refuses that delete, or the marker move: the folder
+\* stays as a leftover.
+CDeleteRefused(p, i) ==
+    /\ conv[p].pc = "published"
+    /\ Unchanged(p, i)
+    /\ i \notin refused[p]
+    /\ crashes < MaxCrash
+    /\ refused' = [refused EXCEPT ![p] = @ \cup {i}]
+    /\ crashes' = crashes + 1
+    /\ UNCHANGED <<v1ver, v1lock, writing, locks, bad, pub, base, staged,
+                   stagedBase, extra, conv, req, out, reqs, famOf>>
+    /\ UNCHANGED marks
+
+\* Every member's folder is gone, refused, or not deletable (a reused child
+\* an older build changed or that was damaged): the locks go, it answers.
+CFinish(p) ==
+    /\ conv[p].pc = "published"
+    /\ \A i \in conv[p].members : ~Unchanged(p, i) \/ i \in refused[p]
+    /\ v1lock' = [i \in Ids |-> IF i \in conv[p].members THEN "free" ELSE v1lock[i]]
+    /\ conv' = [conv EXCEPT ![p] = Idle]
+    /\ Answer(p, Done(p))
+    /\ UNCHANGED <<v1ver, writing, locks, bad, pub, base, staged, stagedBase,
+                   extra, refused, reqs, crashes, famOf>>
+    /\ UNCHANGED marks
+
+\* The process dies: no answer, and its locks go with it.
+CCrash(p) ==
+    /\ req[p] # NoReq
+    /\ crashes < MaxCrash
+    /\ v1lock' = [i \in Ids |-> IF v1lock[i] = p THEN "free" ELSE v1lock[i]]
+    /\ conv' = [conv EXCEPT ![p] = Idle]
+    /\ req' = [req EXCEPT ![p] = NoReq]
+    /\ out' = [out EXCEPT ![p] = [ans |-> "none", root |-> req[p].root]]
+    /\ crashes' = crashes + 1
+    /\ UNCHANGED <<v1ver, writing, locks, bad, pub, base, staged,
+                   stagedBase, extra, refused, reqs, famOf>>
+    /\ UNCHANGED marks
+
+\* A converter's steps, without its faults.
+ConvWork(p) ==
+    \/ AHeld(p) \/ AMissing(p) \/ CBegin(p) \/ CStage(p) \/ CPublishRoot(p) \/ CFinish(p)
+    \/ \E c \in Ids : CPublishChild(p, c) \/ CDelete(p, c) \/ CClean(p, c) \/ MoveMark(p, c) \/ DropMark(p, c)
+
+\* Faults: a refused delete.
+ConvRefused(p) == \E c \in Ids : CDeleteRefused(p, c) \/ CCleanRefused(p, c)
+
+ConvStep(p) == ConvWork(p) \/ ConvRefused(p) \/ CCrash(p)
+
+WriterStep(i) == WCreate(i) \/ WLock(i) \/ WBegin(i) \/ WEnd(i) \/ WUnlock(i) \/ WCrash(i) \/ WMark(i)
+
+Next ==
+    \/ \E p \in Procs :
+         \/ ConvStep(p)
+         \/ \E k \in {"open", "all"}, r \in Roots : Request(p, k, r)
+    \/ \E i \in Ids : WriterStep(i) \/ Damage(i)
+    \/ \E i \in AllIds : FCreate(i) \/ FAppend(i)
+
+Spec == Init /\ [][Next]_vars
+
+\* Each converter keeps going on a request it holds, and writers release
+\* their locks; requests, crashes, writes and opens are bounded.
+FairSpec ==
+    /\ Spec
+    /\ \A p \in Procs :
+         /\ WF_vars(AHeld(p)) /\ WF_vars(AMissing(p)) /\ WF_vars(CBegin(p))
+         /\ WF_vars(CStage(p)) /\ WF_vars(CPublishRoot(p)) /\ WF_vars(CFinish(p))
+         /\ \A c \in Ids : WF_vars(CPublishChild(p, c)) /\ WF_vars(CDelete(p, c)) /\ WF_vars(CClean(p, c))
+         /\ \A c \in Ids : WF_vars(MoveMark(p, c)) /\ WF_vars(DropMark(p, c))
+    /\ \A i \in Ids : WF_vars(WUnlock(i)) /\ WF_vars(WEnd(i))
+
+(* -- properties *)
+
+\* A converter holds every member's lock from staging to the delete, so the
+\* copy it publishes is the version v1 has, never a torn one, and the
+\* folder it deletes is that version.
+LockHeld ==
+    \A p \in Procs :
+        conv[p].pc \in {"locked", "staged", "published"} =>
+            \A i \in conv[p].members : v1lock[i] = p
+CopyIsCurrent ==
+    \A p \in Procs :
+        conv[p].pc = "staged" =>
+            \A i \in conv[p].members : staged[i] => stagedBase[i] = v1ver[i]
+NoTornImport == \A i \in Ids : pub[i] = "import" => base[i] # Torn
+
+\* A converter's locks never outlive its conversion.
+NoStaleConvLock == \A p \in Procs : conv[p].pc = "idle" => \A i \in Ids : v1lock[i] # p
+
+\* A fresh v2 session never takes a live v1 root's id, which would hide that
+\* v1 session for good.
+NoShadow == \A r \in Roots : v1ver[r] > 0 => pub[r] # "fresh"
+
+\* A published root's conversion covered every member present when it
+\* began, and each of those children is published.
+ChildrenLanded ==
+    \A r \in Roots : pub[r] = "import" => \A c \in famOf[r] \ {r} : pub[c] = "import"
+
+\* A child whose root never landed still has its v1 folder: no delete
+\* happens before the whole family is published.
+OrphansKeepV1 == \A i \in Ids : Orphan(i) => v1ver[i] > 0
+
+\* Usage still to settle always has a marker, v1's or v2's (D62).
+UsageKept == \A i \in Ids : owed[i] => (mark1[i] \/ mark2[i])
+
+\* v1's marker never outlives its folder: recovery would then read a
+\* session that is gone.
+NoDanglingMark == \A i \in Ids : mark1[i] => v1ver[i] > 0
+
+\* The step at which p answers; each answer is judged when it is given.
+AnswerStep(p) == req[p] # NoReq /\ req'[p] = NoReq /\ out'[p].ans # "none"
+
+\* "Opened" or "converted" means v2 holds the root (its children by
+\* ChildrenLanded), or there is nothing to convert.
+AnsweredWhole ==
+    [][\A p \in Procs :
+         (AnswerStep(p) /\ out'[p].ans \in {"opened", "converted"}) =>
+             (pub'[req[p].root] \in {"import", "fresh"} \/ v1ver'[req[p].root] = 0)]_vars
+
+\* A live v1 session is never reported missing.
+NoFalseNotFound ==
+    [][\A p \in Procs :
+         (AnswerStep(p) /\ out'[p].ans = "notfound") =>
+             (pub'[req[p].root] = "none" /\ v1ver'[req[p].root] = 0)]_vars
+
+\* A refused request converts nothing: "busy" changes no staging and takes
+\* no lock; "unreadable" leaves no staging of the family and no lock.
+NothingHalfConverted ==
+    [][\A p \in Procs :
+         /\ (AnswerStep(p) /\ out'[p].ans = "busy") =>
+                (staged' = staged /\ pub' = pub /\ \A i \in Ids : v1lock'[i] # p)
+         /\ (AnswerStep(p) /\ out'[p].ans = "unreadable") =>
+                (pub' = pub /\ \A i \in Fam(req[p].root) : ~staged'[i] /\ v1lock'[i] # p)]_vars
+
+\* D60: a v1 folder goes only once its v2 copy is published and is that
+\* folder's version, under its converter's lock or free; no writer deletes.
+NoLossOnDelete ==
+    [][\A i \in Ids :
+         (v1ver[i] > 0 /\ v1ver'[i] = 0) =>
+             /\ pub[i] = "import" /\ pub'[i] = "import"
+             /\ base[i] = v1ver[i] /\ ~writing[i]
+             /\ v1lock[i] # "writer"]_vars
+
+\* An answered open or conversion leaves no v1 folder of the family that
+\* equals its copy, except one held by a writer or by another converter
+\* (which deletes it as it finishes), damaged since, or whose delete was
+\* refused.
+LeftoversGone ==
+    [][\A p \in Procs :
+         (AnswerStep(p) /\ out'[p].ans \in {"opened", "converted"}) =>
+             \A i \in Fam(req[p].root) :
+                 (pub'[i] = "import" /\ v1ver'[i] > 0 /\ v1ver'[i] = base'[i])
+                     => (v1lock'[i] \in {"writer"} \cup (Procs \ {p}) \/ bad'[i] \/ i \in refused'[p])]_vars
+
+\* The converter writes no v1 file: it only deletes v1 folders.
+ConverterOnlyDeletes ==
+    [][(\E p \in Procs : ConvStep(p)) =>
+         /\ \A i \in Ids : v1ver'[i] \in {v1ver[i], 0}
+         /\ UNCHANGED <<writing, bad>>]_vars
+
+\* Nothing converts without a request for that root: no background work.
+ConvertsOnlyOnRequest ==
+    [][\A r \in Roots :
+         (pub[r] = "none" /\ pub'[r] = "import") => \E p \in Procs : req[p].root = r]_vars
+
+\* A live v2 root is never replaced, and a conversion is never redone, nor
+\* is a published child's copy, reused or not: once per id.
+RootsStick ==
+    [][\A i \in Roots \cup NewIds :
+         Live(i) => (pub'[i] = pub[i] /\ base'[i] = base[i])]_vars
+ChildrenStick ==
+    [][\A c \in Ids :
+         (Parent[c] # None /\ pub[c] = "import") => (pub'[c] = "import" /\ base'[c] = base[c])]_vars
+
+\* Every request is answered, unless its process dies.
+RequestsAnswered == \A p \in Procs : (req[p] # NoReq) ~> (req[p] = NoReq)
+=============================================================================

src/core/session_manager/tla/Wiring.cfg

@@ -0,0 +1,13 @@
+SPECIFICATION Spec
+CONSTANT Sessions = {a, b, c}
+INVARIANTS
+    TypeOK
+    OneBackend
+    ParentOutlivesChildren
+    UsageNeverSilent
+    ContinueLinksInterrupted
+    SwitchIsTwoSessions
+PROPERTIES
+    ForkIsNewSession
+    ForkLeavesSource
+    ForkBetweenTurns

src/core/session_manager/tla/Wiring.tla

@@ -0,0 +1,305 @@
+------------------------------ MODULE Wiring ------------------------------
+(***************************************************************************)
+(* Step: fx wiring, through the adapter.                                   *)
+(*                                                                         *)
+(* One fx process at a time. It picks its backend once at start            *)
+(* (`--sessions-v2` or FX_SESSIONS_V2, D26) and keeps it until it exits.   *)
+(* The host has one session slot: it opens a session through the adapter, *)
+(* runs turns, may switch to another session, and closes it at exit. To    *)
+(* switch it may open the next session before closing the current one     *)
+(* (D41), which fills a second slot, `next`, until the current closes. A   *)
+(* turn may spawn a child thread, whose finish is appended through the     *)
+(* parent's Session. Usage is charged to the profile as it happens and     *)
+(* reaches the session log with the next durable batch; the profile's      *)
+(* usage-recovery marker covers the gap. "Continue" starts a new turn      *)
+(* linked to an interrupted one (D23). `/fork` (D58) makes a new session  *)
+(* from the current one's log before a prompt and switches to it. The     *)
+(* process can crash anywhere.                                            *)
+(*                                                                         *)
+(* The manager's own rules are modeled elsewhere (TurnLifecycle.tla,       *)
+(* Subagents.tla, WriterLock.tla); here a reopen simply ends a turn a      *)
+(* crash left open as interrupted (D1).                                    *)
+(*                                                                         *)
+(* Design: system-design.md "fx mapping" and D20 to D27.                   *)
+(***************************************************************************)
+EXTENDS Naturals, FiniteSets
+
+CONSTANT Sessions
+
+Backends == {"v1", "v2"}
+Ends == {"none", "commit", "interrupt"}
+
+VARIABLES
+    up,          \* the fx process is running
+    backend,     \* the backend this process chose at start
+    wrote,       \* backends this process has written since it started
+    cur,         \* the session open in the host slot, or "none"
+    turnOpen,    \* [Sessions -> BOOLEAN]: the log has an open turn
+    lastEnd,     \* [Sessions -> Ends]: how the newest ended turn ended
+    linked,      \* [Sessions -> Ends]: how the turn a continuation continues ended
+    child,       \* "none" or "running": the one child thread
+    childOf,     \* the session whose turn spawned the child, or "none"
+    usageSplit,  \* [Sessions -> BOOLEAN]: the profile and the log may disagree on usage
+    marker,      \* [Sessions -> BOOLEAN]: the profile's usage-recovery marker exists
+    next,        \* the session opened to switch to, or "none" (D41)
+    made,        \* [Sessions -> BOOLEAN]: the session exists on disk
+    forkOf       \* [Sessions -> Sessions \cup {"none"}]: the session a fork came from
+
+vars == <<up, backend, wrote, cur, turnOpen, lastEnd, linked, child, childOf, usageSplit, marker, next, made, forkOf>>
+
+\* Every component uses the backend the process chose (D26).
+ChildBackend == backend
+UsageBackend == backend
+
+TypeOK ==
+    /\ up \in BOOLEAN
+    /\ backend \in Backends
+    /\ wrote \subseteq Backends
+    /\ cur \in Sessions \cup {"none"}
+    /\ turnOpen \in [Sessions -> BOOLEAN]
+    /\ lastEnd \in [Sessions -> Ends]
+    /\ linked \in [Sessions -> Ends]
+    /\ child \in {"none", "running"}
+    /\ childOf \in Sessions \cup {"none"}
+    /\ usageSplit \in [Sessions -> BOOLEAN]
+    /\ marker \in [Sessions -> BOOLEAN]
+    /\ next \in Sessions \cup {"none"}
+    /\ made \in [Sessions -> BOOLEAN]
+    /\ forkOf \in [Sessions -> Sessions \cup {"none"}]
+
+Init ==
+    /\ up = FALSE
+    /\ backend = "v1"
+    /\ wrote = {}
+    /\ cur = "none"
+    /\ turnOpen = [s \in Sessions |-> FALSE]
+    /\ lastEnd = [s \in Sessions |-> "none"]
+    /\ linked = [s \in Sessions |-> "none"]
+    /\ child = "none"
+    /\ childOf = "none"
+    /\ usageSplit = [s \in Sessions |-> FALSE]
+    /\ marker = [s \in Sessions |-> FALSE]
+    /\ next = "none"
+    /\ made = [s \in Sessions |-> FALSE]
+    /\ forkOf = [s \in Sessions |-> "none"]
+
+Active == up /\ cur # "none"
+
+\* fx starts and picks its backend, once.
+Start(b) ==
+    /\ ~up
+    /\ up' = TRUE
+    /\ backend' = b
+    /\ wrote' = {}
+    /\ UNCHANGED <<cur, turnOpen, lastEnd, linked, child, childOf, usageSplit, marker, next, made, forkOf>>
+
+\* Startup usage recovery: a marker left by a crash is reconciled, then removed.
+RecoverUsage(s) ==
+    /\ up
+    /\ marker[s]
+    /\ usageSplit' = [usageSplit EXCEPT ![s] = FALSE]
+    /\ marker' = [marker EXCEPT ![s] = FALSE]
+    /\ UNCHANGED <<up, backend, wrote, cur, turnOpen, lastEnd, linked, child, childOf, next, made, forkOf>>
+
+\* The adapter opens a session: into the slot, or, while one is open, as the
+\* session to switch to (D41). A turn a crash left open ends as interrupted.
+Open(s) ==
+    /\ up
+    /\ next = "none"
+    /\ s # cur
+    /\ IF cur = "none" THEN cur' = s /\ next' = "none" ELSE cur' = cur /\ next' = s
+    /\ wrote' = wrote \cup {backend}
+    /\ turnOpen' = [turnOpen EXCEPT ![s] = FALSE]
+    /\ lastEnd' = IF turnOpen[s] THEN [lastEnd EXCEPT ![s] = "interrupt"] ELSE lastEnd
+    /\ made' = [made EXCEPT ![s] = TRUE]
+    /\ UNCHANGED <<up, backend, linked, child, childOf, usageSplit, marker, forkOf>>
+
+\* New work needs a session and no switch pending.
+Idle == Active /\ next = "none"
+
+BeginTurn ==
+    /\ Idle
+    /\ ~turnOpen[cur]
+    /\ turnOpen' = [turnOpen EXCEPT ![cur] = TRUE]
+    /\ linked' = [linked EXCEPT ![cur] = "none"]
+    /\ wrote' = wrote \cup {backend}
+    /\ UNCHANGED <<up, backend, cur, lastEnd, child, childOf, usageSplit, marker, next, made, forkOf>>
+
+\* "Continue" (D23): a new turn whose first item links to the newest ended
+\* turn, which must have been interrupted.
+Continue ==
+    /\ Idle
+    /\ ~turnOpen[cur]
+    /\ lastEnd[cur] = "interrupt"
+    /\ turnOpen' = [turnOpen EXCEPT ![cur] = TRUE]
+    /\ linked' = [linked EXCEPT ![cur] = lastEnd[cur]]
+    /\ wrote' = wrote \cup {backend}
+    /\ UNCHANGED <<up, backend, cur, lastEnd, child, childOf, usageSplit, marker, next, made, forkOf>>
+
+\* Before a model request is charged, the marker is written.
+MarkUsage ==
+    /\ Active
+    /\ turnOpen[cur]
+    /\ ~marker[cur]
+    /\ marker' = [marker EXCEPT ![cur] = TRUE]
+    /\ UNCHANGED <<up, backend, wrote, cur, turnOpen, lastEnd, linked, child, childOf, usageSplit, next, made, forkOf>>
+
+\* The request is charged to the profile; the log has not caught up yet.
+Charge ==
+    /\ Active
+    /\ turnOpen[cur]
+    /\ marker[cur]
+    /\ usageSplit' = [usageSplit EXCEPT ![cur] = TRUE]
+    /\ UNCHANGED <<up, backend, wrote, cur, turnOpen, lastEnd, linked, child, childOf, marker, next, made, forkOf>>
+
+\* A usage checkpoint mid-turn: `set usage` is a durability point, so the
+\* log catches up with the profile once the append returns.
+PersistUsage ==
+    /\ Active
+    /\ usageSplit[cur]
+    /\ usageSplit' = [usageSplit EXCEPT ![cur] = FALSE]
+    /\ wrote' = wrote \cup {UsageBackend}
+    /\ UNCHANGED <<up, backend, cur, turnOpen, lastEnd, linked, child, childOf, marker, next, made, forkOf>>
+
+\* The turn ends, also while a switch is pending (a cancelled turn); the
+\* usage so far is written in the same durable batch.
+EndTurn(e) ==
+    /\ Active
+    /\ turnOpen[cur]
+    /\ turnOpen' = [turnOpen EXCEPT ![cur] = FALSE]
+    /\ lastEnd' = [lastEnd EXCEPT ![cur] = e]
+    /\ usageSplit' = [usageSplit EXCEPT ![cur] = FALSE]
+    /\ wrote' = wrote \cup {UsageBackend}
+    /\ UNCHANGED <<up, backend, cur, linked, child, childOf, marker, next, made, forkOf>>
+
+\* Once a durable batch carried the usage, the marker goes.
+ClearMarker(s) ==
+    /\ up
+    /\ marker[s]
+    /\ ~usageSplit[s]
+    /\ marker' = [marker EXCEPT ![s] = FALSE]
+    /\ UNCHANGED <<up, backend, wrote, cur, turnOpen, lastEnd, linked, child, childOf, usageSplit, next, made, forkOf>>
+
+\* A turn spawns a child thread (child_spawned through the parent).
+Spawn ==
+    /\ Idle
+    /\ turnOpen[cur]
+    /\ child = "none"
+    /\ child' = "running"
+    /\ childOf' = cur
+    /\ wrote' = wrote \cup {backend, ChildBackend}
+    /\ UNCHANGED <<up, backend, cur, turnOpen, lastEnd, linked, usageSplit, marker, next, made, forkOf>>
+
+\* The child's thread appends child_finished through the parent's Session,
+\* or the parent cancels it; either way through an open parent.
+ChildDone ==
+    /\ up
+    /\ child = "running"
+    /\ cur = childOf
+    /\ child' = "none"
+    /\ childOf' = "none"
+    /\ wrote' = wrote \cup {backend}
+    /\ UNCHANGED <<up, backend, cur, turnOpen, lastEnd, linked, usageSplit, marker, next, made, forkOf>>
+
+\* The host closes a session, to switch or to exit: children are finished
+\* and joined first, then close interrupts an open turn and carries usage.
+\* Closing the current session hands the slot to the one switched to;
+\* closing that one instead abandons the switch (D41).
+Close(s) ==
+    /\ up
+    /\ s \in {cur, next} \ {"none"}
+    /\ child = "none"
+    /\ cur' = IF s = cur THEN next ELSE cur
+    /\ next' = "none"
+    /\ turnOpen' = [turnOpen EXCEPT ![s] = FALSE]
+    /\ lastEnd' = IF turnOpen[s] THEN [lastEnd EXCEPT ![s] = "interrupt"] ELSE lastEnd
+    /\ usageSplit' = [usageSplit EXCEPT ![s] = FALSE]
+    /\ wrote' = wrote \cup {backend}
+    /\ UNCHANGED <<up, backend, linked, child, childOf, marker, made, forkOf>>
+
+\* /fork (D58): a new session holding the current one's log before a chosen
+\* prompt becomes the session to switch to, and Close then hands it the
+\* slot. Only on v2, between turns and with no child running; the source
+\* is never written. The fork's newest ended turn is whichever the source
+\* had before that prompt.
+Fork(f) ==
+    /\ Idle
+    /\ backend = "v2"
+    /\ child = "none"
+    /\ f \notin {cur, next}
+    /\ ~made[f]
+    /\ ~turnOpen[cur]
+    /\ next' = f
+    /\ made' = [made EXCEPT ![f] = TRUE]
+    /\ forkOf' = [forkOf EXCEPT ![f] = cur]
+    /\ \E e \in Ends : lastEnd' = [lastEnd EXCEPT ![f] = e]
+    /\ wrote' = wrote \cup {backend}
+    /\ UNCHANGED <<up, backend, cur, turnOpen, linked, child, childOf, usageSplit, marker>>
+
+Exit ==
+    /\ up
+    /\ cur = "none"
+    /\ next = "none"
+    /\ child = "none"
+    /\ up' = FALSE
+    /\ UNCHANGED <<backend, wrote, cur, turnOpen, lastEnd, linked, child, childOf, usageSplit, marker, next, made, forkOf>>
+
+\* The process dies anywhere: memory and threads are gone; the logs, the
+\* profile ledger and the marker stay.
+Crash ==
+    /\ up
+    /\ up' = FALSE
+    /\ cur' = "none"
+    /\ next' = "none"
+    /\ child' = "none"
+    /\ childOf' = "none"
+    /\ UNCHANGED <<backend, wrote, turnOpen, lastEnd, linked, usageSplit, marker, made, forkOf>>
+
+Next ==
+    \/ \E b \in Backends : Start(b)
+    \/ \E s \in Sessions : RecoverUsage(s) \/ Open(s) \/ ClearMarker(s) \/ Close(s)
+    \/ BeginTurn \/ Continue
+    \/ MarkUsage \/ Charge \/ PersistUsage
+    \/ \E e \in {"commit", "interrupt"} : EndTurn(e)
+    \/ Spawn \/ ChildDone
+    \/ \E f \in Sessions : Fork(f)
+    \/ Exit \/ Crash
+
+Spec == Init /\ [][Next]_vars
+
+-----------------------------------------------------------------------------
+(* Invariants *)
+
+\* A process writes one backend only: no dual writes.
+OneBackend == Cardinality(wrote) <= 1
+
+\* A child thread runs only while its parent's Session is open.
+ParentOutlivesChildren == child = "running" => (up /\ cur = childOf)
+
+\* Whenever the profile and the log may disagree on usage, the marker says so.
+UsageNeverSilent == \A s \in Sessions : usageSplit[s] => marker[s]
+
+\* A pending switch names a second session, never the current one (D41).
+SwitchIsTwoSessions == next # "none" => (cur # "none" /\ cur # next)
+
+\* A continuation always continues an interrupted turn.
+ContinueLinksInterrupted == \A s \in Sessions : linked[s] \in {"none", "interrupt"}
+
+(* Properties of /fork (D58) *)
+
+ForkStep(f) == forkOf'[f] # forkOf[f]
+
+\* A fork is a session that never existed: it never replaces one.
+ForkIsNewSession == [][\A f \in Sessions : ForkStep(f) => ~made[f]]_vars
+
+\* The fork step leaves the source as it was.
+ForkLeavesSource ==
+    [][\A f \in Sessions : ForkStep(f) =>
+         /\ turnOpen'[cur] = turnOpen[cur] /\ lastEnd'[cur] = lastEnd[cur]
+         /\ linked'[cur] = linked[cur] /\ usageSplit'[cur] = usageSplit[cur]]_vars
+
+\* A fork happens on v2, between turns, with no child running.
+ForkBetweenTurns ==
+    [][\A f \in Sessions : ForkStep(f) =>
+         (backend = "v2" /\ ~turnOpen[cur] /\ child = "none")]_vars
+=============================================================================

src/core/session_manager/tla/WriterLock.cfg

@@ -0,0 +1,12 @@
+SPECIFICATION Spec
+CONSTANTS
+    Procs = {p1, p2}
+    Threads = {t1, t2}
+    MaxLines = 4
+    None = None
+INVARIANTS
+    TypeOK
+    OneWriter
+    OnlyHolderOpen
+    MutexInsideOpenSession
+    SeqIsPosition

src/core/session_manager/tla/WriterLock.tla

@@ -0,0 +1,122 @@
+---------------------------- MODULE WriterLock ----------------------------
+(***************************************************************************)
+(* Step: L0 flock plus the L2 per-session mutex.                          *)
+(*                                                                         *)
+(* One writing process per session (flock on {id}/lock) and many threads *)
+(* per process (the Session mutex inside the manager). The kernel drops  *)
+(* the flock when a process dies. Hosts never lock anything; Acquire and *)
+(* WriteAndRelease happen inside append(). Busy is modeled as Open being *)
+(* disabled while another process holds the lock.                        *)
+(*                                                                         *)
+(* Design: system-design.md "Concurrency And Ordering".                   *)
+(***************************************************************************)
+EXTENDS Naturals, Sequences
+
+CONSTANTS Procs, Threads, MaxLines, None
+
+VARIABLES
+    holder,   \* process holding the flock, or None
+    alive,    \* [Procs -> BOOLEAN]
+    opened,   \* [Procs -> BOOLEAN]: the process has an open Session
+    nextSeq,  \* [Procs -> Nat]: the Session's in-memory next seq
+    mutex,    \* [Procs -> Threads \cup {None}]: thread inside append()
+    file      \* the log: a sequence of [seq, by]
+
+vars == <<holder, alive, opened, nextSeq, mutex, file>>
+
+TypeOK ==
+    /\ holder \in Procs \cup {None}
+    /\ alive \in [Procs -> BOOLEAN]
+    /\ opened \in [Procs -> BOOLEAN]
+    /\ nextSeq \in [Procs -> 1..(MaxLines + 1)]
+    /\ mutex \in [Procs -> Threads \cup {None}]
+    /\ file \in Seq([seq : 1..MaxLines, by : Procs])
+
+Init ==
+    /\ holder = None
+    /\ alive = [p \in Procs |-> TRUE]
+    /\ opened = [p \in Procs |-> FALSE]
+    /\ nextSeq = [p \in Procs |-> 1]
+    /\ mutex = [p \in Procs |-> None]
+    /\ file = <<>>
+
+\* open(): flock succeeds only when nobody holds it; otherwise Busy.
+\* The Session learns the next seq from the file it just locked.
+Open(p) ==
+    /\ alive[p]
+    /\ ~opened[p]
+    /\ holder = None
+    /\ holder' = p
+    /\ opened' = [opened EXCEPT ![p] = TRUE]
+    /\ nextSeq' = [nextSeq EXCEPT ![p] = Len(file) + 1]
+    /\ UNCHANGED <<alive, mutex, file>>
+
+\* A thread calls append(); the manager takes the Session mutex.
+Acquire(p, t) ==
+    /\ alive[p]
+    /\ opened[p]
+    /\ mutex[p] = None
+    /\ mutex' = [mutex EXCEPT ![p] = t]
+    /\ UNCHANGED <<holder, alive, opened, nextSeq, file>>
+
+\* Under the mutex: assign seq, write the line, release the mutex.
+WriteAndRelease(p, t) ==
+    /\ alive[p]
+    /\ opened[p]
+    /\ mutex[p] = t
+    /\ Len(file) < MaxLines
+    /\ file' = Append(file, [seq |-> nextSeq[p], by |-> p])
+    /\ nextSeq' = [nextSeq EXCEPT ![p] = @ + 1]
+    /\ mutex' = [mutex EXCEPT ![p] = None]
+    /\ UNCHANGED <<holder, alive, opened>>
+
+\* close(): waits for the mutex, then releases the flock.
+Close(p) ==
+    /\ alive[p]
+    /\ opened[p]
+    /\ mutex[p] = None
+    /\ holder = p
+    /\ holder' = None
+    /\ opened' = [opened EXCEPT ![p] = FALSE]
+    /\ UNCHANGED <<alive, nextSeq, mutex, file>>
+
+\* The process dies; the kernel releases its flock.
+Crash(p) ==
+    /\ alive[p]
+    /\ alive' = [alive EXCEPT ![p] = FALSE]
+    /\ opened' = [opened EXCEPT ![p] = FALSE]
+    /\ mutex' = [mutex EXCEPT ![p] = None]
+    /\ holder' = IF holder = p THEN None ELSE holder
+    /\ UNCHANGED <<nextSeq, file>>
+
+Restart(p) ==
+    /\ ~alive[p]
+    /\ alive' = [alive EXCEPT ![p] = TRUE]
+    /\ UNCHANGED <<holder, opened, nextSeq, mutex, file>>
+
+Next ==
+    \E p \in Procs :
+        \/ Open(p)
+        \/ Close(p)
+        \/ Crash(p)
+        \/ Restart(p)
+        \/ \E t \in Threads : Acquire(p, t) \/ WriteAndRelease(p, t)
+
+Spec == Init /\ [][Next]_vars
+
+-----------------------------------------------------------------------------
+(* Invariants *)
+
+\* At most one process has the session open for writing.
+OneWriter == \A p, q \in Procs : opened[p] /\ opened[q] => p = q
+
+\* Only the flock holder has an open Session.
+OnlyHolderOpen == \A p \in Procs : opened[p] => holder = p
+
+\* A thread inside append() always belongs to an open Session.
+MutexInsideOpenSession == \A p \in Procs : mutex[p] # None => opened[p]
+
+\* File order is seq order: no duplicates, no gaps, across threads and
+\* across processes taking over after a crash.
+SeqIsPosition == \A i \in 1..Len(file) : file[i].seq = i
+=============================================================================

src/core/session_manager/tla/check.sh

@@ -0,0 +1,58 @@
+#!/bin/sh
+# Model-check every session-manager spec with TLC.
+#
+# Needs Java 11+ and tla2tools.jar:
+#   brew install openjdk
+#   mkdir -p ~/.local/share/tla
+#   curl -fL -o ~/.local/share/tla/tla2tools.jar \
+#     https://github.com/tlaplus/tlaplus/releases/latest/download/tla2tools.jar
+#
+# Usage:
+#   ./check.sh                     # every spec
+#   ./check.sh SessionLog Fork     # selected specs
+#   TLA2TOOLS_JAR=/path/tla2tools.jar ./check.sh
+set -eu
+
+cd "$(dirname "$0")"
+
+jar="${TLA2TOOLS_JAR:-$HOME/.local/share/tla/tla2tools.jar}"
+if [ ! -f "$jar" ]; then
+    echo "tla2tools.jar not found at $jar (set TLA2TOOLS_JAR)" >&2
+    exit 2
+fi
+# Prefer JAVA_HOME, then Homebrew's keg-only openjdk, then java on PATH.
+java=""
+for candidate in \
+    "${JAVA_HOME:+$JAVA_HOME/bin/java}" \
+    /opt/homebrew/opt/openjdk/bin/java \
+    /usr/local/opt/openjdk/bin/java \
+    "$(command -v java 2>/dev/null || true)"; do
+    if [ -n "$candidate" ] && [ -x "$candidate" ] && "$candidate" -version >/dev/null 2>&1; then
+        java="$candidate"
+        break
+    fi
+done
+if [ -z "$java" ]; then
+    echo "no working Java runtime (set JAVA_HOME or brew install openjdk)" >&2
+    exit 2
+fi
+
+all="SessionLog TurnLifecycle WriterLock ResumeSnapshot Fork Subagents Catalog Lifecycle Wiring MoveSideFiles V1Conversion"
+specs="${*:-$all}"
+work="${TMPDIR:-/tmp}/session-manager-tlc"
+mkdir -p "$work"
+
+status=0
+for spec in $specs; do
+    echo "== $spec"
+    # -deadlock: do not report states with no enabled action. Every spec is
+    # bounded (MaxLen, MaxLines, finite id sets), so terminal states are
+    # expected at the bound.
+    if ! "$java" -XX:+UseParallelGC -cp "$jar" tlc2.TLC \
+        -deadlock -workers auto -cleanup \
+        -metadir "$work/$spec" \
+        -config "$spec.cfg" "$spec.tla"; then
+        status=1
+    fi
+done
+exit "$status"

src/core/session_manager/tla/mutants.py

@@ -0,0 +1,199 @@
+#!/usr/bin/env python3
+"""Check that every spec still catches the bugs it exists to catch.
+
+Each mutant plants one realistic design bug in a temporary copy of a spec
+and runs TLC on it. The run passes only if TLC reports the expected
+invariant as violated. Run after changing any spec:
+
+    ./mutants.py
+
+Needs the same Java runtime and tla2tools.jar as check.sh.
+"""
+import os
+import pathlib
+import shutil
+import subprocess
+import sys
+import tempfile
+
+HERE = pathlib.Path(__file__).resolve().parent
+JAR = os.environ.get("TLA2TOOLS_JAR", os.path.expanduser("~/.local/share/tla/tla2tools.jar"))
+
+# (spec, bug description, text to replace, replacement, invariant that must fail)
+MUTANTS = [
+    ("Wiring", "a fork reuses a session that exists",
+     "    /\\ f \\notin {cur, next}\n    /\\ ~made[f]\n",
+     "    /\\ f \\notin {cur, next}\n",
+     "ForkIsNewSession"),
+    ("Wiring", "a fork while a turn is open",
+     "    /\\ ~made[f]\n    /\\ ~turnOpen[cur]\n    /\\ next' = f",
+     "    /\\ ~made[f]\n    /\\ next' = f",
+     "ForkBetweenTurns"),
+    ("Wiring", "the fork step writes the source",
+     "    /\\ \\E e \\in Ends : lastEnd' = [lastEnd EXCEPT ![f] = e]",
+     "    /\\ \\E e \\in Ends : lastEnd' = [lastEnd EXCEPT ![f] = e, ![cur] = \"interrupt\"]",
+     "ForkLeavesSource"),
+    ('V1Conversion', 'a converter takes locks another process holds', '    /\\ IF \\A i \\in present : v1lock[i] = "free"\n', '    /\\ IF TRUE\n', 'LockHeld'),
+    ('V1Conversion', 'a fresh v2 session takes a live v1 id', '(AvoidV1Ids => v1ver[i] = 0)', 'TRUE', 'NoShadow'),
+    ('V1Conversion', 'the root lands before its children', '    /\\ \\A c \\in conv[p].members \\ {r} : ~staged[c]\n', '', 'ChildrenLanded'),
+    ('V1Conversion', "a busy answer sweeps another process's staging", '       ELSE /\\ Answer(p, "busy")\n            /\\ UNCHANGED <<v1lock, conv>>\n    /\\ UNCHANGED <<v1ver, writing, locks, bad, pub, base, staged,\n                   stagedBase,', '       ELSE /\\ Answer(p, "busy")\n            /\\ UNCHANGED <<v1lock, conv>>\n    /\\ staged\' = [i \\in Ids |-> FALSE]\n    /\\ UNCHANGED <<v1ver, writing, locks, bad, pub, base,\n                   stagedBase,', 'NothingHalfConverted'),
+    ('V1Conversion', "a crash keeps the converter's locks", '    /\\ v1lock\' = [i \\in Ids |-> IF v1lock[i] = p THEN "free" ELSE v1lock[i]]\n', "    /\\ v1lock' = v1lock\n", 'NoStaleConvLock'),
+    ('V1Conversion', 'an open reports a live v1 session missing', '    /\\ pub[req[p].root] = "none" /\\ v1ver[req[p].root] = 0\n    /\\ Answer(p, IF', '    /\\ ~Live(req[p].root)\n    /\\ Answer(p, IF', 'NoFalseNotFound'),
+    ('V1Conversion', 'a conversion starts without a request', '    LET r == req[p].root\n        present == {i \\in Fam(r) : v1ver[i] > 0} IN\n    /\\ Waiting(p)\n', '    LET r == RootId\n        present == {i \\in Fam(r) : v1ver[i] > 0} IN\n    /\\ conv[p] = Idle\n', 'ConvertsOnlyOnRequest'),
+    ('V1Conversion', 'an unreadable member leaves its staging', "            /\\ staged' = [i \\in Ids |-> IF i \\in Fam(conv[p].root) THEN FALSE ELSE staged[i]]\n", "            /\\ staged' = [i \\in Ids |-> IF i \\in copy THEN TRUE ELSE staged[i]]\n", 'NothingHalfConverted'),
+    ('V1Conversion', 'a busy answer keeps the locks it took', '       ELSE /\\ Answer(p, "busy")\n            /\\ UNCHANGED <<v1lock, conv>>', '       ELSE /\\ Answer(p, "busy")\n            /\\ v1lock\' = [i \\in Ids |-> IF i \\in present /\\ v1lock[i] = "free" THEN p ELSE v1lock[i]]\n            /\\ UNCHANGED conv', 'NoStaleConvLock'),
+    ('V1Conversion', 'a child loses its v1 folder before its root is published', "    /\\ base' = [base EXCEPT ![c] = stagedBase[c]]\n    /\\ UNCHANGED <<v1ver, v1lock,", "    /\\ base' = [base EXCEPT ![c] = stagedBase[c]]\n    /\\ v1ver' = [v1ver EXCEPT ![c] = 0]\n    /\\ UNCHANGED <<v1lock,", 'OrphansKeepV1'),
+    ('V1Conversion', 'a cleanup deletes a leftover an older build changed', '    /\\ pub[i] = "import" /\\ v1ver[i] > 0 /\\ v1ver[i] = base[i] /\\ ~bad[i]\n', '    /\\ pub[i] = "import" /\\ v1ver[i] > 0 /\\ ~bad[i]\n', 'NoLossOnDelete'),
+    ('V1Conversion', "a cleanup ignores a writer's lock", '    /\\ v1lock[i] = "free" /\\ i \\notin refused[p]', '    /\\ i \\notin refused[p]', 'NoLossOnDelete'),
+    ('V1Conversion', 'a conversion keeps the v1 folders', '    /\\ \\A i \\in conv[p].members : ~Unchanged(p, i) \\/ i \\in refused[p]\n', '', 'LeftoversGone'),
+    ('V1Conversion', 'an open skips the leftover cleanup', '    /\\ ~\\E i \\in Fam(req[p].root) : Leftover(p, i)\n', '', 'LeftoversGone'),
+    ('V1Conversion', 'the locks go before the delete', '    /\\ UNCHANGED <<v1ver, v1lock, writing, locks, bad, stagedBase, extra, req,\n                   out, refused, reqs, crashes>>', '    /\\ v1lock\' = [i \\in Ids |-> IF i \\in conv[p].members THEN "free" ELSE v1lock[i]]\n    /\\ UNCHANGED <<v1ver, writing, locks, bad, stagedBase, extra, req,\n                   out, refused, reqs, crashes>>', 'LockHeld'),
+    ('V1Conversion', 'the converter writes a v1 file', '    /\\ UNCHANGED <<v1ver, writing, locks, bad, pub, base, extra, refused,\n                   reqs, crashes, famOf>>', "    /\\ bad' = [i \\in Ids |-> IF i \\in conv[p].members THEN TRUE ELSE bad[i]]\n    /\\ UNCHANGED <<v1ver, writing, locks, pub, base, extra, refused,\n                   reqs, crashes, famOf>>", 'ConverterOnlyDeletes'),
+    ('V1Conversion', 'a reused child is deleted after an older build changed it', '    /\\ i \\in conv[p].members /\\ v1ver[i] > 0 /\\ v1ver[i] = base[i]\n    /\\ i \\in conv[p].copied', '    /\\ i \\in conv[p].members /\\ v1ver[i] > 0\n    /\\ i \\in conv[p].copied', 'NoLossOnDelete'),
+    ('V1Conversion', 'the v1 usage marker goes before the v2 one is written', "    /\\ mark1[i] /\\ mark2[i]\n    /\\ mark1' = [mark1 EXCEPT ![i] = FALSE]", "    /\\ mark1[i]\n    /\\ mark1' = [mark1 EXCEPT ![i] = FALSE]", 'UsageKept'),
+    ('V1Conversion', 'a folder goes before its usage marker moved', 'Deletable(p, i) == Unchanged(p, i) /\\ ~mark1[i]', 'Deletable(p, i) == Unchanged(p, i)', 'NoDanglingMark'),
+    ('V1Conversion', 'a leftover is cleaned before its usage marker moved', "    /\\ Leftover(p, i) /\\ ~mark1[i]\n    /\\ v1ver' = [v1ver EXCEPT ![i] = 0]", "    /\\ Leftover(p, i)\n    /\\ v1ver' = [v1ver EXCEPT ![i] = 0]", 'NoDanglingMark'),
+    ('V1Conversion', 'a reused child is copied again', '        copy == {i \\in m : pub[i] = "none"} IN', '        copy == m IN', 'ChildrenStick'),
+    ("SessionLog", "fsync acks a half-written line",
+     'Fsync ==\n    /\\ status = "open"',
+     'Fsync ==\n    /\\ status \\in {"open", "writing"}',
+     "AckedSurvive"),
+    ("SessionLog", "open() keeps a torn tail",
+     "IF LastDone THEN log ELSE SubSeq(log, 1, Len(log) - 1)", "log",
+     "OpenIsClean"),
+    ("TurnLifecycle", "reopen skips turn_interrupted",
+     "log' = IF IsOpen(log) THEN Append(log, \"interrupt\") ELSE log", "log' = log",
+     "NoStaleTurnAfterReopen"),
+    ("TurnLifecycle", "manager accepts an item outside a turn",
+     '[] k = "item"      -> IsOpen(l)', '[] k = "item"      -> TRUE',
+     "ItemsInsideTurns"),
+    ("WriterLock", "open ignores the flock",
+     "    /\\ holder = None\n    /\\ holder' = p", "    /\\ holder' = p",
+     "OneWriter"),
+    ("ResumeSnapshot", "snapshot stores the wrong state",
+     'Entry("snap", NoVal, Full(log))', 'Entry("snap", NoVal, Empty)',
+     "ResumeEqualsFullReplay"),
+    ("Fork", "fork forgets blob links",
+     "links' = [links EXCEPT ![f] = links[src]]", "links' = links",
+     "RefsExist"),
+    ("Fork", "fork copies a line whose blob was lost",
+     "    /\\ \\A i \\in 2..at : lg[src][i].b # NoBlob => lg[src][i].b \\in links[src]\n", "",
+     "RefsExist"),
+    ("Fork", "fork allowed inside an open turn",
+     "    /\\ ~IsOpen(SubSeq(lg[src], 1, at))\n", "",
+     "ForkAtBoundary"),
+    ("Subagents", "repair marks every child lost",
+     'o |-> IF childLog[c] THEN "interrupted" ELSE "lost"', 'o |-> "lost"',
+     "LostMeansNoLog"),
+    ("Subagents", "spawn while the child's work is open",
+     "    /\\ ~Unfinished(c)\n    /\\ Works(c) < MaxWork",
+     "    /\\ Works(c) < MaxWork",
+     "OneOpenWork"),
+    ("Wiring", "a subagent opens its session on v1",
+     "ChildBackend == backend", 'ChildBackend == "v1"',
+     "OneBackend"),
+    ("Wiring", "close without joining child threads",
+     "    /\\ child = \"none\"\n    /\\ cur' = IF s = cur",
+     "    /\\ cur' = IF s = cur",
+     "ParentOutlivesChildren"),
+    ("Wiring", "switch to the session already open",
+     "    /\\ s # cur\n",
+     "",
+     "SwitchIsTwoSessions"),
+    ("Wiring", "charge usage before writing the marker",
+     "    /\\ marker[cur]\n    /\\ usageSplit'",
+     "    /\\ usageSplit'",
+     "UsageNeverSilent"),
+    ("Wiring", "clear the marker before usage is durable",
+     "    /\\ marker[s]\n    /\\ ~usageSplit[s]\n",
+     "    /\\ marker[s]\n",
+     "UsageNeverSilent"),
+    ("Wiring", "continue a committed turn",
+     "    /\\ lastEnd[cur] = \"interrupt\"\n",
+     "",
+     "ContinueLinksInterrupted"),
+    ("Subagents", "reopen skips child repair",
+     "    /\\ repairing' = TRUE\n    /\\ UNCHANGED <<plog, childLog, thread>>",
+     "    /\\ repairing' = FALSE\n    /\\ UNCHANGED <<plog, childLog, thread>>",
+     "NoIndeterminate"),
+    ("Catalog", "list skips the folder check",
+     'Listed == {s \\in Indexed : dir[s] = "live"}', "Listed == Indexed",
+     "ListedAreLive"),
+    ("Fork", "a setting lists a blob the session lacks",
+     "    /\\ b \\in links[s]\n    /\\ lg' = [lg EXCEPT ![s] = Append(@, E(\"set\", b))]",
+     "    /\\ lg' = [lg EXCEPT ![s] = Append(@, E(\"set\", b))]",
+     "RefsExist"),
+    ("MoveSideFiles", "the map is written before every body is a blob",
+     "    /\\ ~mapped\n    /\\ blobs = Handles\n    /\\ mapped' = TRUE",
+     "    /\\ ~mapped\n    /\\ mapped' = TRUE",
+     "Resolvable"),
+    ("MoveSideFiles", "the side folder goes before the terminal moved",
+     "    /\\ mapped\n    /\\ terminal = \"moved\"\n    /\\ folder = \"present\"",
+     "    /\\ mapped\n    /\\ folder = \"present\"",
+     "TerminalKept"),
+    ("Catalog", "an index refresh for a session never published",
+     'Refresh(s) ==\n    /\\ dir[s] = "live"', "Refresh(s) ==\n    /\\ TRUE",
+     "IndexNamesPublished"),
+    ("Lifecycle", "rename before fsync of line 1",
+     'Advance(s, "synced", "renamed")', 'Advance(s, "written", "renamed")',
+     "VisibleHasLine1"),
+    ("Lifecycle", "ack before fsync of the directory",
+     'Advance(s, "renamed", "done")', 'Advance(s, "synced", "done")',
+     "AckedIsVisible"),
+]
+
+
+def find_java():
+    candidates = []
+    if os.environ.get("JAVA_HOME"):
+        candidates.append(os.path.join(os.environ["JAVA_HOME"], "bin", "java"))
+    candidates += ["/opt/homebrew/opt/openjdk/bin/java", "/usr/local/opt/openjdk/bin/java"]
+    on_path = shutil.which("java")
+    if on_path:
+        candidates.append(on_path)
+    for candidate in candidates:
+        if os.access(candidate, os.X_OK):
+            probe = subprocess.run([candidate, "-version"], capture_output=True)
+            if probe.returncode == 0:
+                return candidate
+    return None
+
+
+def main():
+    java = find_java()
+    if java is None or not os.path.isfile(JAR):
+        print("needs a Java runtime and tla2tools.jar (see check.sh)", file=sys.stderr)
+        return 2
+    survivors = 0
+    with tempfile.TemporaryDirectory(prefix="session-manager-mutants-") as tmp:
+        for index, (spec, desc, old, new, expected) in enumerate(MUTANTS):
+            work = pathlib.Path(tmp) / f"{index:02d}-{spec}"
+            work.mkdir()
+            text = (HERE / f"{spec}.tla").read_text()
+            if old not in text:
+                print(f"{spec:15s} {desc:42s} STALE: mutation no longer applies")
+                survivors += 1
+                continue
+            (work / f"{spec}.tla").write_text(text.replace(old, new, 1))
+            # A smaller model, when the full one is too large to search per mutant.
+            small = HERE / f"{spec}.mutants.cfg"
+            shutil.copy(small if small.exists() else HERE / f"{spec}.cfg", work / f"{spec}.cfg")
+            run = subprocess.run(
+                [java, "-XX:+UseParallelGC", "-cp", JAR, "tlc2.TLC", "-deadlock",
+                 "-workers", "auto", "-cleanup", "-metadir", str(work / "states"),
+                 "-config", f"{spec}.cfg", f"{spec}.tla"],
+                cwd=work, capture_output=True, text=True, timeout=900,
+            )
+            output = run.stdout + run.stderr
+            if (f"Invariant {expected} is violated" in output
+                    or f"Action property {expected} is violated" in output):
+                print(f"{spec:15s} {desc:42s} caught by {expected}")
+            else:
+                print(f"{spec:15s} {desc:42s} SURVIVED (expected {expected} to fail)")
+                survivors += 1
+    print("all mutants caught" if survivors == 0 else f"{survivors} mutant(s) survived")
+    return 0 if survivors == 0 else 1
+
+
+if __name__ == "__main__":
+    sys.exit(main())

src/core/session_manager/tla/trace/CatalogTrace.cfg

@@ -0,0 +1,4 @@
+SPECIFICATION TraceSpec
+CONSTANT Ids <- TraceIds
+CONSTRAINT Progress
+INVARIANT TraceIncomplete

src/core/session_manager/tla/trace/CatalogTrace.tla

@@ -0,0 +1,57 @@
+---------------------------- MODULE CatalogTrace ----------------------------
+(***************************************************************************)
+(* Trace validation for Catalog.tla (index.jsonl, delete, heal, rebuild). *)
+(*                                                                         *)
+(* One trace line per action:                                              *)
+(*   event     Publish | IndexPut | Trash | IndexDel | Purge | Heal (with  *)
+(*             s) | Crash | Rebuild                                        *)
+(*   s         "s1" | "s2" | "s3"                                          *)
+(*   dir       per session, from the folders: "live" ({id}/), "trash"      *)
+(*             (.trash/{id}/), else "gone" once published, else "none"     *)
+(*   index     [id, op] per put or del line of index.jsonl, in file order; *)
+(*             a put that follows a put for the same id only updates the   *)
+(*             summary and is left out, as are `opened` lines              *)
+(*   pending, everDeleted   what the code still owes, and a ghost          *)
+(***************************************************************************)
+EXTENDS Catalog, TraceData, TLC
+
+VARIABLE l
+tvars == <<vars, l>>
+
+TraceIds == {"s1", "s2", "s3"}
+
+ASSUME TLCSet(1, 0)
+
+Matches(e) ==
+    /\ dir' = e.dir
+    /\ index' = e.index
+    /\ pending' = e.pending
+    /\ everDeleted' = e.everDeleted
+
+Act(e) ==
+    CASE e.event = "Publish"  -> Publish(e.s)
+      [] e.event = "IndexPut" -> IndexPut(e.s)
+      [] e.event = "Trash"    -> Trash(e.s)
+      [] e.event = "IndexDel" -> IndexDel(e.s)
+      [] e.event = "Purge"    -> Purge(e.s)
+      [] e.event = "Heal"     -> Heal(e.s)
+      [] e.event = "Crash"    -> Crash
+      [] e.event = "Rebuild"  -> Rebuild
+
+TraceInit == Init /\ l = 1
+
+TraceNext ==
+    /\ l <= Len(Trace)
+    /\ Act(Trace[l])
+    /\ Matches(Trace[l])
+    /\ l' = l + 1
+
+TraceSpec == TraceInit /\ [][TraceNext]_tvars
+
+Progress ==
+    IF l - 1 > TLCGet(1)
+    THEN TLCSet(1, l - 1) /\ PrintT(<<"matched_lines", l - 1>>)
+    ELSE TRUE
+
+TraceIncomplete == l <= Len(Trace)
+=============================================================================

src/core/session_manager/tla/trace/ForkLog.tla

@@ -0,0 +1,31 @@
+------------------------------ MODULE ForkLog ------------------------------
+(***************************************************************************)
+(* A saved fork against its saved source (D5, D58).                        *)
+(*                                                                         *)
+(* `Copied` is the fork's lines after line 1 up to its `forked_from.seq`,  *)
+(* the lines the manager copied; `Source` is the source's lines after      *)
+(* line 1. Both leave out snapshots, which a fork encodes again. Each line *)
+(* is a record [k, h]: k its kind as TurnLifecycleLog names kinds, h a     *)
+(* hash of its exact bytes. Accepted when the copied lines are exactly the *)
+(* source's first lines, byte for byte, and end at a turn boundary: every  *)
+(* turn they start, they also end. `NotWritten` then fails.                *)
+(***************************************************************************)
+EXTENDS Naturals, Sequences, FiniteSets, SavedFork
+
+VARIABLE checked
+
+Starts(s) == {i \in 1..Len(s) : s[i].k = "start"}
+Ends(s) == {i \in 1..Len(s) : s[i].k \in {"commit", "interrupt"}}
+
+IsPrefix ==
+    /\ Len(Copied) <= Len(Source)
+    /\ \A i \in 1..Len(Copied) : Copied[i] = Source[i]
+
+AtBoundary == Cardinality(Starts(Copied)) = Cardinality(Ends(Copied))
+
+LogInit == checked = FALSE
+LogNext == ~checked /\ IsPrefix /\ AtBoundary /\ checked' = TRUE
+LogSpec == LogInit /\ [][LogNext]_checked
+
+NotWritten == ~checked
+=============================================================================

src/core/session_manager/tla/trace/ForkTrace.cfg

@@ -0,0 +1,8 @@
+SPECIFICATION TraceSpec
+CONSTANTS
+    Ids <- TraceIds
+    Blobs <- TraceBlobs
+    MaxLen <- TraceMaxLen
+    NoBlob <- TraceNoBlob
+CONSTRAINT Progress
+INVARIANT TraceIncomplete

src/core/session_manager/tla/trace/ForkTrace.tla

@@ -0,0 +1,58 @@
+----------------------------- MODULE ForkTrace -----------------------------
+(***************************************************************************)
+(* Trace validation for Fork.tla (blobs, fork at a boundary, delete).     *)
+(*                                                                         *)
+(* One trace line per action:                                              *)
+(*   event  Create | Start | Commit | Delete (with s) | PutBlob | Item     *)
+(*          (with s and b) | Fork (with src, f, at)                        *)
+(*   s, src, f   "s1" | "s2" | "s3";  b  "b1" | "b2";  at  the fork's S    *)
+(*   st     per session: "none" | "live" | "deleted"                       *)
+(*   lg     per session, parsed from its log.jsonl: [k, b] for every       *)
+(*          created, start, commit and item line; b is the item's blob     *)
+(*   links  per session: the blob files in its blobs/ folder               *)
+(*   base   per session: the prefix a fork copied, as the code copied it   *)
+(***************************************************************************)
+EXTENDS Fork, TraceData, TLC
+
+VARIABLE l
+tvars == <<vars, l>>
+
+TraceIds == {"s1", "s2", "s3"}
+TraceBlobs == {"b1", "b2"}
+TraceMaxLen == 32
+TraceNoBlob == "none"
+
+ASSUME TLCSet(1, 0)
+
+Matches(e) ==
+    /\ st' = e.st
+    /\ lg' = e.lg
+    /\ links' = e.links
+    /\ base' = e.base
+
+Act(e) ==
+    CASE e.event = "Create"  -> Create(e.s)
+      [] e.event = "Start"   -> Start(e.s)
+      [] e.event = "Commit"  -> Commit(e.s)
+      [] e.event = "Delete"  -> Delete(e.s)
+      [] e.event = "PutBlob" -> PutBlob(e.s, e.b)
+      [] e.event = "Item"    -> Item(e.s, e.b)
+      [] e.event = "Fork"    -> Fork(e.src, e.f, e.at)
+
+TraceInit == Init /\ l = 1
+
+TraceNext ==
+    /\ l <= Len(Trace)
+    /\ Act(Trace[l])
+    /\ Matches(Trace[l])
+    /\ l' = l + 1
+
+TraceSpec == TraceInit /\ [][TraceNext]_tvars
+
+Progress ==
+    IF l - 1 > TLCGet(1)
+    THEN TLCSet(1, l - 1) /\ PrintT(<<"matched_lines", l - 1>>)
+    ELSE TRUE
+
+TraceIncomplete == l <= Len(Trace)
+=============================================================================

src/core/session_manager/tla/trace/LifecycleTrace.cfg

@@ -0,0 +1,4 @@
+SPECIFICATION TraceSpec
+CONSTANT Ids <- TraceIds
+CONSTRAINT Progress
+INVARIANT TraceIncomplete

src/core/session_manager/tla/trace/LifecycleTrace.tla

@@ -0,0 +1,58 @@
+-------------------------- MODULE LifecycleTrace --------------------------
+(***************************************************************************)
+(* Trace validation for Lifecycle.tla (lazy creation and the first-turn   *)
+(* publish).                                                               *)
+(*                                                                         *)
+(* One trace line per action:                                              *)
+(*   event  OpenNew | MkTmp | WriteLine1 | FsyncLog | Rename |             *)
+(*          FsyncDirAndAck | Sweep (with s) | ProcessCrash | PowerLoss     *)
+(*   s      "s1" or "s2", for the per-session actions                      *)
+(*   step   [s1 |-> ..., s2 |-> ...], how far each publish has got         *)
+(*   where  per session: "none" | "tmp" | "visible", from the folders      *)
+(*   line1  per session: "none" | "cached" | "durable", from the log file  *)
+(*          and the fault layer's record of what was synced                *)
+(*   acked  per session: the caller was told the first turn was saved      *)
+(***************************************************************************)
+EXTENDS Lifecycle, Sequences, TraceData, TLC
+
+VARIABLE l
+tvars == <<vars, l>>
+
+TraceIds == {"s1", "s2"}
+
+ASSUME TLCSet(1, 0)
+
+Matches(e) ==
+    /\ step' = e.step
+    /\ where' = e.where
+    /\ line1' = e.line1
+    /\ acked' = e.acked
+
+Act(e) ==
+    CASE e.event = "OpenNew"        -> OpenNew(e.s)
+      [] e.event = "MkTmp"          -> MkTmp(e.s)
+      [] e.event = "WriteLine1"     -> WriteLine1(e.s)
+      [] e.event = "FsyncLog"       -> FsyncLog(e.s)
+      [] e.event = "Rename"         -> Rename(e.s)
+      [] e.event = "FsyncDirAndAck" -> FsyncDirAndAck(e.s)
+      [] e.event = "Sweep"          -> Sweep(e.s)
+      [] e.event = "ProcessCrash"   -> ProcessCrash
+      [] e.event = "PowerLoss"      -> PowerLoss
+
+TraceInit == Init /\ l = 1
+
+TraceNext ==
+    /\ l <= Len(Trace)
+    /\ Act(Trace[l])
+    /\ Matches(Trace[l])
+    /\ l' = l + 1
+
+TraceSpec == TraceInit /\ [][TraceNext]_tvars
+
+Progress ==
+    IF l - 1 > TLCGet(1)
+    THEN TLCSet(1, l - 1) /\ PrintT(<<"matched_lines", l - 1>>)
+    ELSE TRUE
+
+TraceIncomplete == l <= Len(Trace)
+=============================================================================

src/core/session_manager/tla/trace/README.md

@@ -0,0 +1,145 @@
+# Trace validation: checking the code against the specs
+
+TLC cannot read Zig. Instead, the implementation writes one JSON line per
+step it takes, and TLC checks that the whole sequence is a behavior the spec
+allows. A trace is **accepted** only if some behavior of the spec produces
+exactly the logged states, step by step. Otherwise it is **rejected**, and
+`validate.sh` names the first step the spec does not allow.
+
+The models in `..` check the design exhaustively within their bounds. Trace
+validation checks that the real code stays inside the design on every run
+we execute: unit tests, the standalone driver, and the `kill -9` and
+machine-crash matrix.
+
+## How it works
+
+```text
+Zig test build             trace.ndjson            to_tla.py         TLC
+------------------         --------------          ---------         ---
+each L1/L2 step  ------->  {"event": "Fsync",  -->  TraceData.tla -->  SpecTrace.tla
+emits one line              "log_len": 2, ...}      (Trace == <<...>>)  EXTENDS Spec, TraceData
+                                                                        step l must be action
+                                                                        Trace[l].event, and the
+                                                                        next state must equal
+                                                                        Trace[l]'s fields
+```
+
+- `SpecTrace.tla` extends the spec unchanged. It adds a counter `l` over the
+  trace, and each TLC step must be the action named by `Trace[l].event`,
+  landing in a state whose variables equal that line's fields.
+- Nondeterministic actions such as `PowerLoss` are resolved by the logged
+  state: TLC tries every choice and keeps the ones that match.
+- The trick for the verdict: the invariant `TraceIncomplete == l <= Len(Trace)`
+  is violated exactly when the whole trace was matched, so TLC reporting a
+  violation means ACCEPTED. A state constraint prints the furthest line
+  matched, which names the rejected step.
+
+## Files
+
+| File | Purpose |
+|---|---|
+| `validate.sh SPEC trace.ndjson` | Runs the check in a temp directory. Exit 0 accepted, 1 rejected, 2 tool error |
+| `to_tla.py` | Converts JSON lines into `TraceData.tla`. Lists become sequences, objects records, `{"$set": [...]}` sets |
+| `SessionLogTrace.tla`, `.cfg` | Wrapper for `SessionLog.tla`. The event contract is in its header |
+| `stand_in_log.py` | A small Python stand-in for L1, used only to self-test this tooling |
+| `check_saved_logs.py ROOT...` | Checks logs fx saved (`{id}/log.jsonl` under each ROOT) after the fact: every log against `TurnLifecycle`, every parent with child lines against `Subagents`, and every fork against its source with `ForkLog`. `--selftest` requires 7 good and 9 planted logs to get their verdicts |
+| `ForkLog.tla` | A fork's copied lines against its source's: accepted only when they are the source's first lines byte for byte (snapshots aside, which a fork encodes again) and end at a turn boundary |
+| `TurnLifecycleLog.tla`, `SubagentsLog.tla` | Its wrappers. Only the disk is known, so TLC searches the process state between lines; accepted when some behavior writes exactly the saved lines |
+| `check_wiring_traces.py LOG...` | Checks the adapter's `wiring` trace lines (a run with `FX_TRACE_SCOPES=wiring`) against `Wiring.tla`: each process's lines become Start, the host steps and Exit, or Crash when it stops without Exit. A log where two processes overlap is skipped. `--selftest` requires 6 good and 8 planted traces to get their verdicts, the fork cases included |
+| `WiringTrace.tla` | Its wrapper. Accepted when every step is allowed in turn; the usage steps change nothing a traced step reads, so they are left out |
+| `bun_tlc_check.sh FX_WORKTREE [FILE [PATTERN]]` | Runs fx's E2E tests under Bun with `FX_E2E_TLA_DIR` set, then checks every kept run with TLC: the `wiring` traces with `check_wiring_traces.py` and the saved logs with `check_saved_logs.py`. Exit 0 only when all are ACCEPTED and at least `MIN_FORKS` (default 1) fork steps and saved forks were checked; a skipped trace counts as a failure |
+| `check_conversion.py --request R --report D` | Checks a v1-to-v2 conversion run against `V1Conversion.tla` (D59). The request comes from the pipeline harness suite `session-conversion-tlc`, which drives the real binary step by step (older-build v1 writes, opens, `fx sessions convert`, holds, damage, a crash mid-conversion) and observes each step's result on disk and through fx's own readers and listing. Exit 0 ACCEPTED only when TLC matched every observation, 1 REJECTED, 2 INCONCLUSIVE, 3 TOOL_ERROR. `--selftest` requires 6 good and 7 planted runs to get their verdicts |
+| `V1ConversionTrace.tla` | Its wrapper. Each observation's step kind limits the model actions that may run before it; a request step makes exactly one request, and only a writer an earlier hold step left running may write during it |
+| `selftest.sh` | Proves the tooling both accepts and rejects (below) |
+
+## Self-test
+
+`./selftest.sh` runs the stand-in three ways and requires these verdicts:
+
+| Case | Required verdict |
+|---|---|
+| Correct stand-in (writes, fsync, a crash in the middle of a write, recovery, a machine crash that tears a line, recovery) | ACCEPTED, 15 steps |
+| Recovery keeps a torn tail (planted bug) | REJECTED at step 8, the `Recover` |
+| Good trace with `acked` changed from 2 to 3 on line 5 | REJECTED at step 5 |
+
+Last run: 2026-09-27, TLC2 2.19. All three verdicts matched.
+
+## The contract for the Zig trace hook
+
+These rules apply to the test-only trace hook, `../../trace.zig`:
+
+1. **Test builds only.** The hook is behind a build option and compiles to
+   nothing in release builds, so it adds no cost and no I/O to fx.
+2. **One line per spec action,** named exactly like the action in the spec
+   (`BeginWrite`, `Fsync`, `Recover`, ...), with one field per spec variable
+   under the names in the wrapper header.
+3. **Real state, not bookkeeping.** Fields that model the disk (line count,
+   torn tail, seq numbers, which folders exist) are computed by reading the
+   actual files after the step. Fields that model memory (status, acked, open
+   turn) come from the manager's own state. A trace built only from the
+   writer's counters would agree with itself and prove nothing.
+4. **One order.** Steps inside a Session are emitted while holding the
+   Session mutex, so the trace order is the real order. Multi-process tests
+   (`WriterLock`) run through the standalone driver, which serializes the
+   steps of all processes into one trace.
+5. **Crashes are logged by the driver.** A killed process cannot log its own
+   crash. After `kill -9` or a simulated machine crash, the driver appends the
+   `ProcessCrash` or `PowerLoss` line, reading the disk state itself.
+6. **Every trace gets checked.** The driver runs `validate.sh` on every trace
+   it produces, and any rejection fails the run.
+
+## Adding a wrapper for another spec
+
+Copy `SessionLogTrace.tla` and change three things:
+
+- `EXTENDS` names the new spec.
+- `Matches(e)` compares every variable of that spec with the fields of `e`.
+- `Act(e)` maps each event name to the spec's action. For an action with
+  parameters, such as `Write(k)` or `Open(p)`, the line carries the argument,
+  and `Act` passes it on, for example
+  `[] e.event = "Write" -> Write(e.kind)`.
+
+Keep `TraceInit`, `TraceNext`, `Progress` and `TraceIncomplete` as they are,
+and copy the `.cfg`, setting the spec's constants large enough for real
+traces. Then add a stand-in case, or a real Zig test, that the new wrapper
+must reject. A wrapper that has never rejected anything is not yet trusted.
+
+Each of these wrappers has rejected its planted bug: `TurnLifecycleTrace`,
+`WriterLockTrace`, `ResumeSnapshotTrace`, `LifecycleTrace`, `ForkTrace`,
+`SubagentsTrace` and `CatalogTrace`.
+
+## Limits
+
+- **Guard with IF, never with `\/`, inside `Matches`.** Within an action,
+  TLC explores both sides of a disjunction, so
+  `Len(log') = 0 \/ log'[Len(log')].done` still indexes an empty sequence and
+  ends in a tool error. The first Zig traces (an `Fsync` and a `Recover` on an
+  empty log) found this in `SessionLogTrace.tla`; it now uses IF.
+
+- **Give every TLC run its own `java.io.tmpdir`.** TLC unpacks `TLC.tla`,
+  `Naturals.tla` and the other standard modules there. With a shared
+  folder, parallel checks read each other's half-written copies and fail
+  with "Fatal errors while parsing". `validate.sh` points it into the
+  run's private work folder, and `check_saved_logs.py` and
+  `check_wiring_traces.py` give each parallel check its own (`JOBS`,
+  default 6).
+- **A batch is one write; trace views end at the observed line.** The
+  manager writes each batch in one append, observed or not, so traced runs
+  and the crash matrix see production's write pattern (a process kill never
+  splits a batch). Its lines are observed one by one after the write, so
+  a tracer that reads the log bounds its view by the observed line's seq.
+- **Only what runs is checked.** Trace validation checks the runs we
+  execute. That is why the driver's crash matrix matters: it decides which
+  code paths get traced.
+- **The mapping from files to spec state must be right.** A wrong mapping can
+  hide a bug. Keep it small, and read the real files (rule 3).
+- **Traces must fit the model's constants.** `SessionLogTrace.cfg` raises
+  `MaxLines` to 64 for that reason, and `TurnLifecycleTrace.tla` sets
+  `TraceMaxLen` to 4096 for the driver's host models, whose logs run to
+  hundreds of lines. A longer trace is rejected at the bound, so raise the
+  constant or split the trace. In a trace check the bound adds no states:
+  the trace fixes every step.
+- **TLC 2.19 plus the Community Modules jar crashes**
+  (`NoClassDefFoundError: tlc2/value/impl/KSubsetValue`). That is why the
+  converter exists instead of `Json!ndJsonDeserialize`. Revisit when a TLC
+  release matches the modules jar.

src/core/session_manager/tla/trace/ResumeSnapshotTrace.cfg

@@ -0,0 +1,7 @@
+SPECIFICATION TraceSpec
+CONSTANTS
+    Vals <- TraceVals
+    MaxLen <- TraceMaxLen
+    NoVal <- TraceNoVal
+CONSTRAINT Progress
+INVARIANT TraceIncomplete

src/core/session_manager/tla/trace/ResumeSnapshotTrace.tla

@@ -0,0 +1,51 @@
+------------------------ MODULE ResumeSnapshotTrace ------------------------
+(***************************************************************************)
+(* Trace validation for ResumeSnapshot.tla (the fold and its snapshots).  *)
+(*                                                                         *)
+(* One trace line per action:                                              *)
+(*   event  Set (with v) | Start | Commit | Snapshot                       *)
+(*   v      for Set: "v1" | "v2", the prefs value written                  *)
+(*   log    every modeled line on disk, parsed from log.jsonl:             *)
+(*          [k |-> "set" | "start" | "commit" | "snap", v, st]. For a      *)
+(*          snapshot, st is read from the snapshot's own state object:     *)
+(*          [pref, turns (committed), open]. Other kinds are outside this  *)
+(*          spec and left out.                                             *)
+(* The Snapshot action requires st to equal the full fold at that point,   *)
+(* so a snapshot that stores the wrong state is rejected.                  *)
+(***************************************************************************)
+EXTENDS ResumeSnapshot, TraceData, TLC
+
+VARIABLE l
+tvars == <<vars, l>>
+
+TraceVals == {"v1", "v2"}
+TraceMaxLen == 64
+TraceNoVal == "none"
+
+ASSUME TLCSet(1, 0)
+
+Matches(e) == log' = e.log
+
+Act(e) ==
+    CASE e.event = "Set"      -> Set(e.v)
+      [] e.event = "Start"    -> Start
+      [] e.event = "Commit"   -> Commit
+      [] e.event = "Snapshot" -> Snapshot
+
+TraceInit == Init /\ l = 1
+
+TraceNext ==
+    /\ l <= Len(Trace)
+    /\ Act(Trace[l])
+    /\ Matches(Trace[l])
+    /\ l' = l + 1
+
+TraceSpec == TraceInit /\ [][TraceNext]_tvars
+
+Progress ==
+    IF l - 1 > TLCGet(1)
+    THEN TLCSet(1, l - 1) /\ PrintT(<<"matched_lines", l - 1>>)
+    ELSE TRUE
+
+TraceIncomplete == l <= Len(Trace)
+=============================================================================

src/core/session_manager/tla/trace/SessionLogTrace.cfg

@@ -0,0 +1,4 @@
+SPECIFICATION TraceSpec
+CONSTANT MaxLines = 64
+CONSTRAINT Progress
+INVARIANT TraceIncomplete

src/core/session_manager/tla/trace/SessionLogTrace.tla

@@ -0,0 +1,66 @@
+------------------------- MODULE SessionLogTrace -------------------------
+(***************************************************************************)
+(* Trace validation for SessionLog.tla.                                    *)
+(*                                                                         *)
+(* TLC accepts an implementation trace only if some behavior of SessionLog *)
+(* produces exactly the logged states, step by step. TraceData.tla is      *)
+(* generated from the implementation's JSON-lines trace by to_tla.py.      *)
+(*                                                                         *)
+(* One trace line per L1 step:                                             *)
+(*   event      BeginWrite | FinishWrite | Fsync | ProcessCrash |          *)
+(*              PowerLoss | Recover                                        *)
+(*   log_len    lines in log.jsonl, counting a torn final line             *)
+(*   tail_done  whether the file ends in "\n"                              *)
+(*   seqs       seq of every complete line, parsed from the file bytes     *)
+(*   durable    lines covered by the last fsync                            *)
+(*   acked      lines acknowledged to callers as durable                   *)
+(*   status     "open" | "writing" | "down"                                *)
+(* log_len, tail_done and seqs must come from reading the real file, not   *)
+(* from the writer's own counters.                                         *)
+(***************************************************************************)
+EXTENDS SessionLog, TraceData, TLC
+
+VARIABLE l
+tvars == <<vars, l>>
+
+ASSUME TLCSet(1, 0)
+
+\* IF, not \/: inside an action TLC explores both sides of a disjunction,
+\* so `Len(log') = 0 \/ log'[Len(log')].done` would index an empty log.
+Matches(e) ==
+    /\ Len(log') = e.log_len
+    /\ IF Len(log') = 0 THEN e.tail_done ELSE log'[Len(log')].done = e.tail_done
+    /\ Len(e.seqs) <= Len(log')
+    /\ \A i \in 1..Len(e.seqs) : log'[i].seq = e.seqs[i]
+    /\ durable' = e.durable
+    /\ acked' = e.acked
+    /\ status' = e.status
+
+Act(e) ==
+    CASE e.event = "BeginWrite"   -> BeginWrite
+      [] e.event = "FinishWrite"  -> FinishWrite
+      [] e.event = "Fsync"        -> Fsync
+      [] e.event = "ProcessCrash" -> ProcessCrash
+      [] e.event = "PowerLoss"    -> PowerLoss
+      [] e.event = "Recover"      -> Recover
+
+TraceInit == Init /\ l = 1
+
+TraceNext ==
+    /\ l <= Len(Trace)
+    /\ Act(Trace[l])
+    /\ Matches(Trace[l])
+    /\ l' = l + 1
+
+TraceSpec == TraceInit /\ [][TraceNext]_tvars
+
+\* State constraint: prints each new furthest trace line matched.
+Progress ==
+    IF l - 1 > TLCGet(1)
+    THEN TLCSet(1, l - 1) /\ PrintT(<<"matched_lines", l - 1>>)
+    ELSE TRUE
+
+\* Violated exactly when the whole trace was matched: TLC reporting this
+\* invariant as violated means ACCEPTED.
+TraceIncomplete == l <= Len(Trace)
+=============================================================================

src/core/session_manager/tla/trace/SubagentsLog.tla

@@ -0,0 +1,31 @@
+--------------------------- MODULE SubagentsLog ---------------------------
+(***************************************************************************)
+(* Checks a parent log fx saved against Subagents.tla, after the fact.     *)
+(*                                                                         *)
+(* Only the disk is known: the parent's child lines, in order (`Target`,   *)
+(* records [k, c, w, o]), and which children have a log at the end         *)
+(* (`FinalChildLog`), both from SavedChildren.tla. Threads, crashes,       *)
+(* reopens and when each child's log appeared are left to TLC. Accepted    *)
+(* when some behavior of the spec writes exactly these lines and ends      *)
+(* with those child logs: the invariant `NotWritten` then fails.           *)
+(*                                                                         *)
+(* check_saved_logs.py writes SavedChildren.tla and runs this.             *)
+(***************************************************************************)
+EXTENDS Subagents, SavedChildren, TLC
+
+ASSUME TLCSet(1, 0)
+
+LogNext ==
+    /\ Next
+    /\ Len(plog') <= Len(Target)
+    /\ plog' = SubSeq(Target, 1, Len(plog'))
+
+LogSpec == Init /\ [][LogNext]_vars
+
+Progress ==
+    IF Len(plog) > TLCGet(1)
+    THEN TLCSet(1, Len(plog)) /\ PrintT(<<"matched_lines", Len(plog)>>)
+    ELSE TRUE
+
+NotWritten == ~(plog = Target /\ childLog = FinalChildLog)
+=============================================================================

src/core/session_manager/tla/trace/SubagentsTrace.cfg

@@ -0,0 +1,5 @@
+SPECIFICATION TraceSpec
+CONSTANT Children <- TraceChildren
+CONSTANT MaxWork <- TraceMaxWork
+CONSTRAINT Progress
+INVARIANT TraceIncomplete

src/core/session_manager/tla/trace/SubagentsTrace.tla

@@ -0,0 +1,58 @@
+--------------------------- MODULE SubagentsTrace ---------------------------
+(***************************************************************************)
+(* Trace validation for Subagents.tla (children and parent reopen repair).*)
+(*                                                                         *)
+(* One trace line per action:                                              *)
+(*   event     Spawn | ChildStart | ChildFinish | Cancel | RepairChild    *)
+(*             (with c) | Crash | Reopen | RepairDone                      *)
+(*   c         "c1" | "c2"                                                 *)
+(*   plog      the parent's child lines, parsed from its log.jsonl:        *)
+(*             [k |-> "spawned" | "finished", c, w (the child's work       *)
+(*             number, counted from its spawn lines), o]                   *)
+(*   childLog  per child: {child}/log.jsonl exists                         *)
+(*   thread, up, repairing   the process's own state, as the code runs it  *)
+(***************************************************************************)
+EXTENDS Subagents, TraceData, TLC
+
+VARIABLE l
+tvars == <<vars, l>>
+
+TraceChildren == {"c1", "c2"}
+TraceMaxWork == 2
+
+ASSUME TLCSet(1, 0)
+
+Matches(e) ==
+    /\ plog' = e.plog
+    /\ childLog' = e.childLog
+    /\ thread' = e.thread
+    /\ up' = e.up
+    /\ repairing' = e.repairing
+
+Act(e) ==
+    CASE e.event = "Spawn"          -> Spawn(e.c)
+      [] e.event = "ChildStart"     -> ChildStart(e.c)
+      [] e.event = "ChildFinish"    -> ChildFinish(e.c)
+      [] e.event = "Cancel"         -> Cancel(e.c)
+      [] e.event = "RepairChild"    -> RepairChild(e.c)
+      [] e.event = "Crash"          -> Crash
+      [] e.event = "Reopen"         -> Reopen
+      [] e.event = "RepairDone"     -> RepairDone
+
+TraceInit == Init /\ l = 1
+
+TraceNext ==
+    /\ l <= Len(Trace)
+    /\ Act(Trace[l])
+    /\ Matches(Trace[l])
+    /\ l' = l + 1
+
+TraceSpec == TraceInit /\ [][TraceNext]_tvars
+
+Progress ==
+    IF l - 1 > TLCGet(1)
+    THEN TLCSet(1, l - 1) /\ PrintT(<<"matched_lines", l - 1>>)
+    ELSE TRUE
+
+TraceIncomplete == l <= Len(Trace)
+=============================================================================

src/core/session_manager/tla/trace/TurnLifecycleLog.tla

@@ -0,0 +1,29 @@
+------------------------- MODULE TurnLifecycleLog -------------------------
+(***************************************************************************)
+(* Checks a log fx saved against TurnLifecycle.tla, after the fact.        *)
+(*                                                                         *)
+(* Only the disk is known: the log's kinds, in order (`Target`, from       *)
+(* SavedLog.tla). The process state (status, fresh), and with it every     *)
+(* close, crash and reopen that wrote no line, is left to TLC. The log is  *)
+(* accepted when some behavior of the spec writes exactly these lines:     *)
+(* every step keeps the log a prefix of `Target`, and the invariant        *)
+(* `NotWritten` fails once the whole log is written.                       *)
+(*                                                                         *)
+(* check_saved_logs.py writes SavedLog.tla and runs this.                  *)
+(***************************************************************************)
+EXTENDS TurnLifecycle, SavedLog, TLC
+
+ASSUME TLCSet(1, 0)
+
+LogNext == Next /\ Prefix(log', Target)
+
+LogSpec == Init /\ [][LogNext]_vars
+
+\* Prints the longest prefix written, which names the rejected line.
+Progress ==
+    IF Len(log) > TLCGet(1)
+    THEN TLCSet(1, Len(log)) /\ PrintT(<<"matched_lines", Len(log)>>)
+    ELSE TRUE
+
+NotWritten == log # Target
+=============================================================================

src/core/session_manager/tla/trace/TurnLifecycleTrace.cfg

@@ -0,0 +1,4 @@
+SPECIFICATION TraceSpec
+CONSTANT MaxLen <- TraceMaxLen
+CONSTRAINT Progress
+INVARIANT TraceIncomplete

src/core/session_manager/tla/trace/TurnLifecycleTrace.tla

@@ -0,0 +1,53 @@
+------------------------ MODULE TurnLifecycleTrace ------------------------
+(***************************************************************************)
+(* Trace validation for TurnLifecycle.tla (turn rules, close, reopen).    *)
+(*                                                                         *)
+(* One trace line per action:                                              *)
+(*   event   Create | Write (with kind) | Close | Crash | Reopen           *)
+(*   kind    for Write: start | item | compacted | commit | interrupt | set *)
+(*   log     the kinds on disk, in order, parsed from log.jsonl; snapshot  *)
+(*           and child lines are outside this spec and left out            *)
+(*   status  "new" | "open" | "closed" | "down"                            *)
+(*   fresh   TRUE from a reopen until the next turn starts                 *)
+(***************************************************************************)
+EXTENDS TurnLifecycle, TraceData, TLC
+
+VARIABLE l
+tvars == <<vars, l>>
+
+\* Only bounds the log a trace may build; the trace fixes every step, so
+\* a large bound adds no states. The driver's host models run to hundreds
+\* of lines.
+TraceMaxLen == 4096
+
+ASSUME TLCSet(1, 0)
+
+Matches(e) ==
+    /\ log' = e.log
+    /\ status' = e.status
+    /\ fresh' = e.fresh
+
+Act(e) ==
+    CASE e.event = "Create" -> Create
+      [] e.event = "Write"  -> Write(e.kind)
+      [] e.event = "Close"  -> Close
+      [] e.event = "Crash"  -> Crash
+      [] e.event = "Reopen" -> Reopen
+
+TraceInit == Init /\ l = 1
+
+TraceNext ==
+    /\ l <= Len(Trace)
+    /\ Act(Trace[l])
+    /\ Matches(Trace[l])
+    /\ l' = l + 1
+
+TraceSpec == TraceInit /\ [][TraceNext]_tvars
+
+Progress ==
+    IF l - 1 > TLCGet(1)
+    THEN TLCSet(1, l - 1) /\ PrintT(<<"matched_lines", l - 1>>)
+    ELSE TRUE
+
+TraceIncomplete == l <= Len(Trace)
+=============================================================================

src/core/session_manager/tla/trace/V1ConversionTrace.tla

@@ -0,0 +1,108 @@
+--------------------------- MODULE V1ConversionTrace ---------------------------
+(***************************************************************************)
+(* Trace validation for V1Conversion.tla from what real fx runs leave.    *)
+(*                                                                         *)
+(* A driver runs real fx processes one step at a time and observes the    *)
+(* result after each (`Obs`, from ConversionData.tla), a record with      *)
+(*   k      the step: create | write | hold | release (older-build v1     *)
+(*          writers), open | all | crash (a request, the last one killed  *)
+(*          mid-request), open2 (two processes opening the same root at   *)
+(*          once), damage, fresh (a new v2 session), list                 *)
+(*   r      the requested root ("none" for other steps)                    *)
+(*   ans    the request's answer: opened | converted | busy | unreadable  *)
+(*          | notfound, or none; ans2 the second process's, for open2     *)
+(*   v1     [Ids -> version]: each v1 member's distinct contents in order *)
+(*          of first appearance, 0 absent                                  *)
+(*   pub    [AllIds -> Status]: each id in v2                              *)
+(*   base   [AllIds -> version]: for a converted id, the v1 version its   *)
+(*          copy equals, -1 when it equals none                            *)
+(*   extra  [AllIds -> Nat]: v2 turns after the copied ones                *)
+(*   dirty  conversion leftovers in .tmp                                   *)
+(*   listed the ids the listing shows                                      *)
+(*   bad    [Ids -> BOOLEAN]: members the driver made unreadable          *)
+(*   held   the members a still-running older build has open               *)
+(*   denied the driver made the file system refuse deletes in this step    *)
+(* Between observations, only the actions of that step's kind may run,   *)
+(* any number of them; a request step makes exactly its requests, by     *)
+(* process p1 (and p2 for open2). Accepted when some behavior of          *)
+(* V1Conversion passes through every observation in order: `NotDone`     *)
+(* then fails.                                                             *)
+(***************************************************************************)
+EXTENDS V1Conversion, ConversionData, Sequences, TLC
+
+VARIABLE l
+tvars == <<vars, l>>
+
+ASSUME TLCSet(1, 0)
+
+P1 == "p1"
+P2 == "p2"
+
+\* The requests observation `j` makes.
+Made(o) == CASE o.k = "open2" -> 2 [] o.k \in {"open", "all", "crash"} -> 1 [] OTHER -> 0
+RECURSIVE ReqCount(_)
+ReqCount(n) == IF n = 0 THEN 0 ELSE Made(Obs[n]) + ReqCount(n - 1)
+
+\* A refused delete is a fault only a step that injected it may show.
+ConvAllowed(p, o) == ConvWork(p) \/ (o.denied /\ ConvRefused(p))
+
+\* During a request, an older build may write only if an earlier hold step
+\* left it holding the session; it cannot take a lock there.
+HolderStep(i) == WBegin(i) \/ WEnd(i) \/ WMark(i)
+
+\* The actions a step of kind `o.k` may take, at observation index `n`.
+Hidden(o, n) ==
+    CASE o.k \in {"create", "write", "hold", "release"} ->
+            \E i \in Ids : WriterStep(i)
+      [] o.k = "damage" -> \E i \in Ids : Damage(i)
+      [] o.k = "fresh" -> \E i \in NewIds : FCreate(i) \/ FAppend(i)
+      [] o.k \in {"open", "all"} ->
+            \/ reqs < ReqCount(n) /\ Request(P1, o.k, o.r)
+            \/ ConvAllowed(P1, o)
+            \/ \E i \in Ids : HolderStep(i)
+            \/ req[P1] = NoReq /\ reqs = ReqCount(n) /\ \E i \in AllIds : FAppend(i)
+      [] o.k = "open2" ->
+            \/ reqs = ReqCount(n) - 2 /\ Request(P1, "open", o.r)
+            \/ reqs = ReqCount(n) - 1 /\ Request(P2, "open", o.r)
+            \/ \E p \in {P1, P2} : ConvAllowed(p, o)
+            \/ \E i \in Ids : HolderStep(i)
+            \/ req[P1] = NoReq /\ req[P2] = NoReq /\ reqs = ReqCount(n) /\ \E i \in AllIds : FAppend(i)
+      [] o.k = "crash" ->
+            \/ reqs < ReqCount(n) /\ \E kk \in {"open", "all"} : Request(P1, kk, o.r)
+            \/ ConvAllowed(P1, o) \/ CCrash(P1)
+            \/ \E i \in Ids : HolderStep(i)
+      [] OTHER -> FALSE
+
+Match(o, n) ==
+    /\ v1ver = o.v1
+    /\ pub = o.pub
+    /\ \A i \in AllIds : pub[i] = "import" => base[i] = o.base[i]
+    /\ extra = o.extra
+    /\ Dirty = o.dirty
+    /\ Listed = o.listed
+    /\ bad = o.bad
+    /\ {i \in Ids : v1lock[i] = "writer"} = o.held
+    /\ reqs = ReqCount(n)
+    /\ \A p \in Procs : req[p] = NoReq /\ conv[p] = Idle
+    /\ o.k \in {"open", "all"} => out[P1].ans = o.ans
+    /\ o.k = "open2" =>
+         \/ out[P1].ans = o.ans /\ out[P2].ans = o.ans2
+         \/ out[P1].ans = o.ans2 /\ out[P2].ans = o.ans
+    /\ o.k = "crash" => out[P1].ans = "none"
+
+TraceInit == Init /\ l = 1
+
+TraceNext ==
+    /\ l <= Len(Obs)
+    /\ \/ Hidden(Obs[l], l) /\ UNCHANGED l
+       \/ Match(Obs[l], l) /\ l' = l + 1 /\ UNCHANGED vars
+
+TraceSpec == TraceInit /\ [][TraceNext]_tvars
+
+Progress ==
+    IF l - 1 > TLCGet(1)
+    THEN TLCSet(1, l - 1) /\ PrintT(<<"matched_lines", l - 1>>)
+    ELSE TRUE
+
+NotDone == l <= Len(Obs)
+=============================================================================

src/core/session_manager/tla/trace/WiringTrace.tla

@@ -0,0 +1,55 @@
+------------------------------ MODULE WiringTrace ------------------------------
+(***************************************************************************)
+(* Trace validation for Wiring.tla, from fx's `wiring` trace lines.        *)
+(*                                                                         *)
+(* One trace line per step the adapter logs, in order (`Trace`, from       *)
+(* WiringData.tla): a record [a, s, e] with                                *)
+(*   a   Start | Open | BeginTurn | EndTurn | Spawn | ChildDone | Close    *)
+(*       | Fork | Exit | Crash                                             *)
+(*   s   the session, "s1".. (Open, Close, and Fork's new session), else  *)
+(*       "none"                                                            *)
+(*   e   "commit" | "interrupt" (EndTurn only), else "none"                *)
+(* Start and Exit are the store's first open and last close in a process  *)
+(* (a process whose tracing starts after its store opened starts at its  *)
+(* first line);                                                          *)
+(* Crash is added by check_wiring_traces.py when a process's lines stop    *)
+(* without Exit. The usage steps (the marker, charges, checkpoints) happen *)
+(* in code the adapter does not see; they change only `usageSplit` and    *)
+(* `marker`, which no traced step reads, so they are left out. Accepted    *)
+(* when every line is an allowed step in turn: `NotDone` then fails.       *)
+(***************************************************************************)
+EXTENDS Wiring, WiringData, Sequences, TLC
+
+VARIABLE l
+tvars == <<vars, l>>
+
+ASSUME TLCSet(1, 0)
+
+Act(e) ==
+    CASE e.a = "Start"     -> Start("v2")
+      [] e.a = "Open"      -> Open(e.s)
+      [] e.a = "BeginTurn" -> BeginTurn
+      [] e.a = "EndTurn"   -> EndTurn(e.e)
+      [] e.a = "Spawn"     -> Spawn
+      [] e.a = "ChildDone" -> ChildDone
+      [] e.a = "Close"     -> Close(e.s)
+      [] e.a = "Fork"      -> Fork(e.s)
+      [] e.a = "Exit"      -> Exit
+      [] e.a = "Crash"     -> Crash
+
+TraceInit == Init /\ l = 1
+
+TraceNext ==
+    /\ l <= Len(Trace)
+    /\ Act(Trace[l])
+    /\ l' = l + 1
+
+TraceSpec == TraceInit /\ [][TraceNext]_tvars
+
+Progress ==
+    IF l - 1 > TLCGet(1)
+    THEN TLCSet(1, l - 1) /\ PrintT(<<"matched_lines", l - 1>>)
+    ELSE TRUE
+
+NotDone == l <= Len(Trace)
+=============================================================================

src/core/session_manager/tla/trace/WriterLockTrace.cfg

@@ -0,0 +1,8 @@
+SPECIFICATION TraceSpec
+CONSTANTS
+    Procs <- TraceProcs
+    Threads <- TraceThreads
+    MaxLines <- TraceMaxLines
+    None <- TraceNone
+CONSTRAINT Progress
+INVARIANT TraceIncomplete

src/core/session_manager/tla/trace/WriterLockTrace.tla

@@ -0,0 +1,62 @@
+-------------------------- MODULE WriterLockTrace --------------------------
+(***************************************************************************)
+(* Trace validation for WriterLock.tla (flock plus the Session mutex).    *)
+(*                                                                         *)
+(* One trace line per action:                                              *)
+(*   event    Open | Close | Crash | Restart (with p) |                    *)
+(*            Acquire | WriteAndRelease (with p and t)                     *)
+(*   p, t     "p1" | "p2" and "t1" | "t2"                                  *)
+(*   holder   the process holding the flock, or "none"                     *)
+(*   alive, opened, nextSeq, mutex   per process                           *)
+(*   file     [seq, by] for each line written since the trace began,       *)
+(*            parsed from log.jsonl: seq counts from 1 at the first traced *)
+(*            line, `by` is the writer named in the line. `closed` lines   *)
+(*            are bookkeeping outside this spec and are left out, and the  *)
+(*            seqs after them shift down, so a skipped or duplicated seq   *)
+(*            still shows as a mismatch.                                   *)
+(***************************************************************************)
+EXTENDS WriterLock, TraceData, TLC
+
+VARIABLE l
+tvars == <<vars, l>>
+
+TraceProcs == {"p1", "p2"}
+TraceThreads == {"t1", "t2"}
+TraceMaxLines == 64
+TraceNone == "none"
+
+ASSUME TLCSet(1, 0)
+
+Matches(e) ==
+    /\ holder' = e.holder
+    /\ alive' = e.alive
+    /\ opened' = e.opened
+    /\ nextSeq' = e.nextSeq
+    /\ mutex' = e.mutex
+    /\ file' = e.file
+
+Act(e) ==
+    CASE e.event = "Open"            -> Open(e.p)
+      [] e.event = "Close"           -> Close(e.p)
+      [] e.event = "Crash"           -> Crash(e.p)
+      [] e.event = "Restart"         -> Restart(e.p)
+      [] e.event = "Acquire"         -> Acquire(e.p, e.t)
+      [] e.event = "WriteAndRelease" -> WriteAndRelease(e.p, e.t)
+
+TraceInit == Init /\ l = 1
+
+TraceNext ==
+    /\ l <= Len(Trace)
+    /\ Act(Trace[l])
+    /\ Matches(Trace[l])
+    /\ l' = l + 1
+
+TraceSpec == TraceInit /\ [][TraceNext]_tvars
+
+Progress ==
+    IF l - 1 > TLCGet(1)
+    THEN TLCSet(1, l - 1) /\ PrintT(<<"matched_lines", l - 1>>)
+    ELSE TRUE
+
+TraceIncomplete == l <= Len(Trace)
+=============================================================================

src/core/session_manager/tla/trace/bun_tlc_check.sh

@@ -0,0 +1,60 @@
+#!/usr/bin/env bash
+# Runs fx's E2E tests under Bun with traces kept, then checks every run with
+# TLC: each process's `wiring` trace against Wiring.tla, and each saved log
+# against TurnLifecycle, Subagents and, for a fork, ForkLog. Exits 0 only when
+# every check is ACCEPTED and the runs held at least MIN_FORKS fork steps.
+#
+#   bun_tlc_check.sh FX_WORKTREE [TEST_FILE [TEST_NAME_PATTERN]]
+#
+# FX_WORKTREE is an fx checkout whose zig-out/bin/fx is built. MIN_FORKS
+# (default 1) guards against a run that never reached the code under check.
+set -euo pipefail
+
+here="$(cd "$(dirname "$0")" && pwd)"
+fx="${1:?usage: bun_tlc_check.sh FX_WORKTREE [TEST_FILE [TEST_NAME_PATTERN]]}"
+file="${2:-sessions-v2.test.ts}"
+pattern="${3:-fork}"
+min_forks="${MIN_FORKS:-1}"
+
+[ -x "$fx/zig-out/bin/fx" ] || { echo "build fx first: $fx/zig-out/bin/fx" >&2; exit 2; }
+out="$(mktemp -d "${TMPDIR:-/tmp}/fx-bun-tlc.XXXXXX")"
+echo "runs kept in $out"
+
+(cd "$fx/tests/e2e" && env -u AI_GATEWAY_API_KEY -u AI_GATEWAY_TEST_API_KEY \
+    FX_E2E_TLA_DIR="$out" bun test "$file" -t "$pattern") || {
+    echo "bun: the tests failed; TLC not run" >&2
+    exit 1
+}
+
+traces=()
+while IFS= read -r f; do traces+=("$f"); done < <(find "$out" -name '*.wiring.log' | sort)
+roots=()
+while IFS= read -r d; do roots+=("$d"); done < <(find "$out" -type d -name 'sessions-v2' | sort)
+[ "${#traces[@]}" -gt 0 ] || { echo "no wiring traces kept: is FX_E2E_TLA_DIR honored?" >&2; exit 1; }
+[ "${#roots[@]}" -gt 0 ] || { echo "no saved logs kept" >&2; exit 1; }
+
+forks="$(cat "${traces[@]}" | grep -c 'action=Fork ' || true)"
+echo "traces ${#traces[@]}, saved roots ${#roots[@]}, fork steps $forks"
+[ "$forks" -ge "$min_forks" ] || { echo "fewer than $min_forks fork steps reached TLC" >&2; exit 1; }
+
+status=0
+echo "== wiring traces against Wiring.tla"
+wiring="$(python3 "$here/check_wiring_traces.py" "${traces[@]}")" || status=1
+echo "$wiring"
+if echo "$wiring" | grep -q -E '^(REJECTED|SKIPPED|TOOL ERROR) +/'; then status=1; fi
+# An empty trace is right only for a run on v1, which saves no v2 sessions.
+while IFS= read -r path; do
+    [ -n "$path" ] || continue
+    if [ -d "$(dirname "$path")/sessions-v2" ]; then
+        echo "a v2 run left an empty trace: $path" >&2
+        status=1
+    fi
+done < <(echo "$wiring" | sed -n -E 's/^EMPTY +(.*): no wiring lines$/\1/p')
+echo "$wiring" | grep -q -E '^ACCEPTED +[1-9]' || { echo "no trace was accepted" >&2; status=1; }
+echo "== saved logs against TurnLifecycle, Subagents and ForkLog"
+saved="$(python3 "$here/check_saved_logs.py" "${roots[@]}")" || status=1
+echo "$saved"
+fork_jobs="$(echo "$saved" | awk '$1 == "fork" && $2 == "ACCEPTED" {print $3}')"
+[ "${fork_jobs:-0}" -ge "$min_forks" ] || { echo "fewer than $min_forks saved forks checked" >&2; status=1; }
+[ "$status" -eq 0 ] && echo "ALL ACCEPTED" || echo "NOT ALL ACCEPTED"
+exit "$status"

src/core/session_manager/tla/trace/check_conversion.py

@@ -0,0 +1,311 @@
+#!/usr/bin/env python3
+"""Check what real fx runs did against V1Conversion.tla, with TLC.
+
+    check_conversion.py --request REQUEST.json --report DIR
+    check_conversion.py --selftest
+
+REQUEST is written by the Bun driver: {"version": 1, "ids": {"root": ID,
+"child": ID or null, "fresh": [ID, ...]}, "observations": [...]}, one
+observation per real step, as V1ConversionTrace.tla describes. The verdict
+is printed as JSON and kept in DIR with TLC's log and its generated inputs:
+ACCEPTED (exit 0) only when TLC reached its sentinel with every observation
+matched; REJECTED (1) when TLC ran to the end without matching them all;
+INCONCLUSIVE (2) for malformed or empty evidence; TOOL_ERROR (3) otherwise.
+"""
+import argparse
+import hashlib
+import json
+import os
+import pwd
+import re
+import shutil
+import subprocess
+import sys
+from pathlib import Path
+
+HERE = Path(__file__).resolve().parent
+TLA = HERE.parent
+JAVA = os.environ.get("JAVA", "/opt/homebrew/opt/openjdk/bin/java")
+# The account's home, not $HOME: drivers run fx under a disposable HOME.
+JAR = os.environ.get("TLA_JAR", os.path.join(pwd.getpwuid(os.getuid()).pw_dir, ".local/share/tla/tla2tools.jar"))
+
+KINDS = {"create", "write", "hold", "release", "open", "all", "crash", "open2", "damage", "fresh", "list"}
+REQUESTS = {"open", "all", "crash", "open2"}
+ANSWERS = {"none", "opened", "converted", "busy", "unreadable", "notfound"}
+STATUS = {"none", "import", "fresh"}
+EXIT = {"ACCEPTED": 0, "REJECTED": 1, "INCONCLUSIVE": 2, "TOOL_ERROR": 3}
+
+
+class Inconclusive(Exception):
+    pass
+
+
+def tla_str(s):
+    return '"' + s.replace("\\", "\\\\").replace('"', '\\"') + '"'
+
+
+def tla_fun(mapping, render):
+    return "(" + " @@ ".join(f"{tla_str(k)} :> {render(v)}" for k, v in mapping.items()) + ")"
+
+
+def model_ids(ids):
+    """Real id -> model id: the root "r", the child "c", fresh sessions "n1".."""
+    root, child, fresh = ids.get("root"), ids.get("child"), ids.get("fresh", [])
+    if not isinstance(root, str) or not root:
+        raise Inconclusive("the request names no root id")
+    names = {root: "r"}
+    if child:
+        names[child] = "c"
+    for n, fid in enumerate(fresh, 1):
+        names[fid] = f"n{n}"
+    if len(names) != 1 + bool(child) + len(fresh):
+        raise Inconclusive("ids repeat")
+    return names
+
+
+def model_obs(request):
+    names = model_ids(request.get("ids", {}))
+    obs = request.get("observations")
+    if not isinstance(obs, list) or not obs:
+        raise Inconclusive("no observations")
+    if not any(o.get("k") in REQUESTS for o in obs):
+        raise Inconclusive("no request step was observed")
+    member = ["r", "c"]
+    every = member + sorted(v for v in names.values() if v.startswith("n"))
+    out = []
+    for n, o in enumerate(obs, 1):
+        try:
+            k, ans, ans2 = o["k"], o.get("ans", "none"), o.get("ans2", "none")
+            if k not in KINDS or ans not in ANSWERS or ans2 not in ANSWERS:
+                raise Inconclusive(f"observation {n}: unknown step or answer")
+            r = names.get(o.get("r"), "none") if k in REQUESTS else "none"
+            if k in REQUESTS and r != "r":
+                raise Inconclusive(f"observation {n}: a request names no known root")
+
+            def by_model(field, default, check):
+                got = {names[i]: v for i, v in o[field].items() if i in names}
+                if len(got) != len(o[field]):
+                    raise Inconclusive(f"observation {n}: {field} names an unknown id")
+                for v in got.values():
+                    check(v)
+                return got, default
+
+            def nat(v):
+                if not isinstance(v, int) or v < -1:
+                    raise Inconclusive(f"observation {n}: a count is not an integer")
+
+            def status(v):
+                if v not in STATUS:
+                    raise Inconclusive(f"observation {n}: unknown v2 status {v!r}")
+
+            def flag(v):
+                if not isinstance(v, bool):
+                    raise Inconclusive(f"observation {n}: a flag is not a boolean")
+
+            v1, _ = by_model("v1", 0, nat)
+            pub, _ = by_model("pub", "none", status)
+            base, _ = by_model("base", 0, nat)
+            extra, _ = by_model("extra", 0, nat)
+            bad, _ = by_model("bad", False, flag)
+            listed, held, denied = o["listed"], o.get("held", []), o.get("denied", False)
+            if not isinstance(o["dirty"], bool) or not isinstance(listed, list) or not isinstance(held, list) \
+                    or not isinstance(denied, bool):
+                raise Inconclusive(f"observation {n}: dirty, listed, held or denied is malformed")
+            if denied and k not in REQUESTS:
+                raise Inconclusive(f"observation {n}: deletes can only be refused during a request")
+            if any(names.get(i) not in member for i in held):
+                raise Inconclusive(f"observation {n}: held names an id that is not a v1 member")
+            unknown = [i for i in listed if i not in names]
+            out.append({
+                "k": k, "r": r, "ans": ans, "ans2": ans2,
+                "v1": {i: v1.get(i, 0) for i in member},
+                "pub": {i: pub.get(i, "none") for i in every},
+                "base": {i: base.get(i, 0) for i in every},
+                "extra": {i: extra.get(i, 0) for i in every},
+                "bad": {i: bad.get(i, False) for i in member},
+                "dirty": o["dirty"],
+                "denied": denied,
+                "held": sorted(names[i] for i in held),
+                # An id the run does not know can never match the model's listing.
+                "listed": sorted({names[i] for i in listed if i in names} | ({"unknown"} if unknown else set())),
+            })
+        except KeyError as missing:
+            raise Inconclusive(f"observation {n}: missing {missing}")
+    return out, [v for v in every if v.startswith("n")]
+
+
+def data_module(obs):
+    def rec(o):
+        return ("[k |-> " + tla_str(o["k"]) + ", r |-> " + tla_str(o["r"]) + ", ans |-> " + tla_str(o["ans"])
+                + ", ans2 |-> " + tla_str(o["ans2"])
+                + ", v1 |-> " + tla_fun(o["v1"], str) + ", pub |-> " + tla_fun(o["pub"], tla_str)
+                + ", base |-> " + tla_fun(o["base"], str) + ", extra |-> " + tla_fun(o["extra"], str)
+                + ", bad |-> " + tla_fun(o["bad"], lambda b: "TRUE" if b else "FALSE")
+                + ", dirty |-> " + ("TRUE" if o["dirty"] else "FALSE")
+                + ", denied |-> " + ("TRUE" if o["denied"] else "FALSE")
+                + ", held |-> {" + ", ".join(tla_str(i) for i in o["held"]) + "}"
+                + ", listed |-> {" + ", ".join(tla_str(i) for i in o["listed"]) + "}]")
+    body = ",\n    ".join(rec(o) for o in obs)
+    return f"---- MODULE ConversionData ----\nEXTENDS TLC, Integers, FiniteSets\nObs == <<\n    {body}\n>>\n====\n"
+
+
+def config(obs, fresh):
+    kinds = [o["k"] for o in obs]
+    max_v = max([1] + [v for o in obs for v in o["v1"].values()])
+    max_extra = max([1] + [v for o in obs for v in o["extra"].values()])
+    writes = sum(k in {"create", "write", "hold"} for k in kinds) + 1
+    crashes = sum(k in {"crash", "release"} for k in kinds) + 3 * sum(o["denied"] for o in obs) + 1
+    reqs = sum(2 if k == "open2" else 1 for k in kinds if k in REQUESTS)
+    fresh_set = "{" + ", ".join(tla_str(f) for f in fresh) + "}"
+    return (f'CONSTANTS\n    Procs = {{"p1", "p2"}}\n    RootId = "r"\n    ChildId = "c"\n    NewIds = {fresh_set}\n    None = None\n'
+            f"    Torn = Torn\n    MaxV = {max_v}\n    MaxLocks = {writes}\n    MaxExtra = {max_extra}\n"
+            f"    MaxCrash = {crashes}\n    MaxReq = {reqs}\n    AvoidV1Ids = TRUE\n"
+            "SPECIFICATION TraceSpec\nINVARIANT NotDone\nCONSTRAINT Progress\n")
+
+
+def sha256(path):
+    return hashlib.sha256(Path(path).read_bytes()).hexdigest()
+
+
+def run_tlc(obs, fresh, work):
+    work.mkdir(parents=True)
+    (work / "tmp").mkdir()
+    for name in ("V1Conversion.tla",):
+        shutil.copyfile(TLA / name, work / name)
+    shutil.copyfile(HERE / "V1ConversionTrace.tla", work / "V1ConversionTrace.tla")
+    (work / "ConversionData.tla").write_text(data_module(obs))
+    (work / "V1ConversionTrace.cfg").write_text(config(obs, fresh))
+    command = [JAVA, "-XX:+UseParallelGC", f"-Djava.io.tmpdir={work / 'tmp'}", "-cp", JAR, "tlc2.TLC",
+               "-workers", "1", "-deadlock", "-metadir", str(work / "states"),
+               "-config", "V1ConversionTrace.cfg", "V1ConversionTrace"]
+    with (work / "tlc.log").open("w") as log:
+        code = subprocess.run(command, cwd=work, stdout=log, stderr=subprocess.STDOUT, timeout=600).returncode
+    text = (work / "tlc.log").read_text(errors="replace")
+    matched = max([int(m) for m in re.findall(r'"matched_lines", (\d+)', text)] or [0])
+    expected = len(obs)
+    if code == 12 and "Invariant NotDone is violated" in text and matched == expected:
+        verdict = "ACCEPTED"
+    elif code == 0 and "No error has been found" in text and matched < expected:
+        verdict = "REJECTED"
+    else:
+        verdict = "TOOL_ERROR"
+    shutil.rmtree(work / "states", ignore_errors=True)
+    shutil.rmtree(work / "tmp", ignore_errors=True)
+    return {"verdict": verdict, "matched": matched, "expected": expected, "exitCode": code,
+            "log": str(work / "tlc.log"),
+            "modelHashes": {n: sha256(work / n) for n in ("V1Conversion.tla", "V1ConversionTrace.tla")}}
+
+
+def verify(request, report):
+    if request.get("version") != 1:
+        raise Inconclusive("version 1 required")
+    obs, fresh = model_obs(request)
+    result = run_tlc(obs, fresh, report / "tlc")
+    if result["verdict"] == "REJECTED":
+        step = obs[result["matched"]]
+        result["detail"] = (f"observations 1..{result['matched']} match; observation {result['matched'] + 1} "
+                            f"({step['k']}, answer {step['ans']}) is not a behavior of V1Conversion")
+    return result
+
+
+def selftest():
+    """Planted observation sequences: each must get its verdict."""
+    ids = {"root": "R", "child": None, "fresh": []}
+
+    def ob(k, v1=0, pub="none", base=0, extra=0, ans="none", dirty=False, listed=None, bad=False, r="R", held=(),
+           denied=False, ans2="none"):
+        return {"k": k, "r": r, "ans": ans, "ans2": ans2, "v1": {"R": v1}, "pub": {"R": pub}, "base": {"R": base},
+                "extra": {"R": extra}, "bad": {"R": bad}, "dirty": dirty, "held": list(held),
+                "listed": ["R"] if listed is None else listed, "denied": denied}
+    made = ob("create", v1=1)
+    kept = ob("open", v1=1, pub="import", base=1, ans="opened", denied=True)
+    cases = [
+        ("an open converts the v1 session and deletes it, then a turn lands in v2",
+         [made, ob("open", pub="import", base=1, extra=1, ans="opened")], "ACCEPTED"),
+        ("convert-all, then an open of the converted session",
+         [made, ob("all", pub="import", base=1, ans="converted"),
+          ob("open", pub="import", base=1, ans="opened")], "ACCEPTED"),
+        ("busy while an older build holds it, opened once released",
+         [made, ob("hold", v1=1, held=["R"]), ob("open", v1=1, ans="busy", held=["R"]), ob("release", v1=1),
+          ob("open", pub="import", base=1, ans="opened")], "ACCEPTED"),
+        ("unreadable: refused, nothing converted or deleted",
+         [made, ob("damage", v1=1, bad=True), ob("open", v1=1, bad=True, ans="unreadable")], "ACCEPTED"),
+        ("a refused delete leaves the folder; the next open deletes it",
+         [made, kept, ob("open", pub="import", base=1, ans="opened")], "ACCEPTED"),
+        ("an older build changes a leftover; the next open keeps it, and v2 keeps its copy",
+         [made, kept, ob("write", v1=2, pub="import", base=1),
+          ob("open", v1=2, pub="import", base=1, ans="opened")], "ACCEPTED"),
+        ("a crash mid-conversion leaves staging; the next open sweeps it",
+         [made, ob("crash", v1=1, dirty=True), ob("open", pub="import", base=1, ans="opened")], "ACCEPTED"),
+        ("two processes open it at once: one converts, both open the copy",
+         [made, ob("open2", pub="import", base=1, ans="opened", ans2="opened")], "ACCEPTED"),
+        ("planted: of two processes opening it at once, one calls it unreadable",
+         [made, ob("open2", pub="import", base=1, ans="opened", ans2="unreadable")], "REJECTED"),
+        ("planted: a live v1 session reported missing",
+         [made, ob("open", v1=1, ans="notfound")], "REJECTED"),
+        ("planted: the copy matches no v1 version",
+         [made, ob("open", pub="import", base=-1, ans="opened")], "REJECTED"),
+        ("planted: busy with no holder",
+         [made, ob("open", v1=1, ans="busy")], "REJECTED"),
+        ("planted: the listing hides an unconverted v1 session",
+         [made, ob("list", v1=1, listed=[]), ob("open", pub="import", base=1, ans="opened")], "REJECTED"),
+        ("planted: unreadable, yet half converted",
+         [made, ob("damage", v1=1, bad=True), ob("open", v1=1, bad=True, dirty=True, ans="unreadable")], "REJECTED"),
+        ("planted: an older build's later write reaches the v2 copy",
+         [made, kept, ob("write", v1=2, pub="import", base=2)], "REJECTED"),
+        ("planted: converted with no request",
+         [made, ob("list", v1=1, pub="import", base=1), ob("open", pub="import", base=1, ans="opened")], "REJECTED"),
+        ("planted: the v1 folder stays though no delete was refused",
+         [made, ob("open", v1=1, pub="import", base=1, ans="opened")], "REJECTED"),
+        ("planted: a leftover an older build changed is deleted",
+         [made, kept, ob("write", v1=2, pub="import", base=1), ob("open", pub="import", base=1, ans="opened")],
+         "REJECTED"),
+        ("planted: the v1 folder deleted before its copy was published",
+         [made, ob("crash", dirty=True)], "REJECTED"),
+    ]
+    bad = 0
+    root = Path(os.environ.get("TMPDIR", "/tmp")) / f"check-conversion-selftest-{os.getpid()}"
+    for n, (label, observations, want) in enumerate(cases, 1):
+        try:
+            got = verify({"version": 1, "ids": ids, "observations": observations}, root / str(n))
+            verdict = got["verdict"]
+        except Inconclusive as why:
+            verdict = f"INCONCLUSIVE ({why})"
+        ok = verdict == want
+        bad += not ok
+        print(f"{'ok  ' if ok else 'FAIL'}  {label}: {verdict}, wanted {want}")
+    print(f"selftest: {len(cases) - bad}/{len(cases)} verdicts as required")
+    if not bad:
+        shutil.rmtree(root, ignore_errors=True)
+    return 1 if bad else 0
+
+
+def main():
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument("--request", type=Path)
+    parser.add_argument("--report", type=Path)
+    parser.add_argument("--selftest", action="store_true")
+    args = parser.parse_args()
+    if args.selftest:
+        return selftest()
+    if not args.request or not args.report:
+        parser.error("--request and --report are required")
+    report = args.report.resolve()
+    report.mkdir(parents=True, exist_ok=False)
+    try:
+        raw = args.request.read_bytes()
+        (report / "request.json").write_bytes(raw)
+        result = verify(json.loads(raw), report)
+    except Inconclusive as why:
+        result = {"verdict": "INCONCLUSIVE", "detail": str(why)}
+    except (OSError, ValueError, subprocess.SubprocessError) as error:
+        result = {"verdict": "TOOL_ERROR", "detail": str(error)}
+    result["version"] = 1
+    result["report"] = str(report)
+    (report / "verdict.json").write_text(json.dumps(result, indent=2) + "\n")
+    print(json.dumps(result))
+    return EXIT[result["verdict"]]
+
+
+if __name__ == "__main__":
+    sys.exit(main())

src/core/session_manager/tla/trace/check_saved_logs.py

@@ -0,0 +1,298 @@
+#!/usr/bin/env python3
+"""Checks logs fx saved against TurnLifecycle.tla and Subagents.tla.
+
+usage: check_saved_logs.py ROOT...    each ROOT holds session folders
+                                      ({id}/log.jsonl), as ~/.fx/sessions/v2
+       check_saved_logs.py --selftest planted logs: each must get its verdict
+
+JOBS=N runs N TLC checks at once (default 6).
+
+Every session's log is checked against TurnLifecycle (TurnLifecycleLog.tla);
+a log with child lines is also checked against Subagents (SubagentsLog.tla),
+with each child's log existence read at the end. Only the disk is known, so
+TLC searches the process state in between (see the two wrappers). A torn
+tail is left out, as the manager reads it. A log that does not parse is
+reported as unreadable, not checked. Exit 0 when every readable log is
+accepted.
+"""
+import hashlib
+import json
+import os
+import pwd
+import re
+import shutil
+import subprocess
+import sys
+import tempfile
+from concurrent.futures import ThreadPoolExecutor
+
+HERE = os.path.dirname(os.path.abspath(__file__))
+TLA = os.path.dirname(HERE)
+JAVA = os.environ.get("JAVA", "/opt/homebrew/opt/openjdk/bin/java")
+# The account's home, not $HOME: drivers run fx under a disposable HOME.
+JAR = os.environ.get("TLA_JAR", os.path.join(pwd.getpwuid(os.getuid()).pw_dir, ".local/share/tla/tla2tools.jar"))
+
+TURN_KINDS = {
+    "session_created": "created",
+    "set": "set",
+    "turn_started": "start",
+    "item": "item",
+    "compacted": "compacted",
+    "turn_committed": "commit",
+    "turn_interrupted": "interrupt",
+    "closed": "closed",
+}
+CHILD_KINDS = {"child_spawned", "child_finished"}
+OUTSIDE = {"snapshot"} | CHILD_KINDS
+
+
+class Unreadable(Exception):
+    pass
+
+
+def read_lines(path, raw=False):
+    """The log's whole lines; a torn tail is left out. With `raw`, each line
+    comes with its exact bytes."""
+    data = open(path, "rb").read()
+    end = data.rfind(b"\n")
+    out = []
+    for n, line in enumerate(data[: end + 1].split(b"\n")[:-1], 1):
+        try:
+            value = json.loads(line)
+        except ValueError:
+            raise Unreadable(f"line {n} is not JSON")
+        out.append((value, line) if raw else value)
+    return out
+
+
+def fork_records(lines, upto=None):
+    """[k, h] records of lines 2.. (those with seq <= `upto`), snapshots left
+    out: a fork encodes its copied snapshots again."""
+    out = []
+    for value, line in lines[1:]:
+        if upto is not None and value.get("seq", 0) > upto:
+            break
+        kind = value.get("kind")
+        if kind == "snapshot":
+            continue
+        out.append({"k": TURN_KINDS.get(kind, kind), "h": hashlib.sha256(line).hexdigest()[:16]})
+    return out
+
+
+def fork_target(lines, root):
+    """For a fork, its copied lines and its source's lines; else None."""
+    origin = lines[0][0].get("forked_from")
+    if not origin:
+        return None
+    source = os.path.join(root, origin["id"], "log.jsonl")
+    if not os.path.isfile(source):
+        raise Unreadable(f"fork source {origin['id']} is not in this root")
+    return fork_records(lines, origin["seq"]), fork_records(read_lines(source, raw=True))
+
+
+def turn_target(lines):
+    target = []
+    for n, line in enumerate(lines, 1):
+        kind = line.get("kind")
+        if kind in OUTSIDE:
+            continue
+        if kind not in TURN_KINDS:
+            raise Unreadable(f"line {n} has unknown kind {kind!r}")
+        target.append(TURN_KINDS[kind])
+    return target
+
+
+def child_target(lines, root):
+    names, works, target = {}, {}, []
+    for line in lines:
+        kind = line.get("kind")
+        if kind not in CHILD_KINDS:
+            continue
+        child = line["child"]
+        c = names.setdefault(child, f"c{len(names) + 1}")
+        if kind == "child_spawned":
+            works[c] = works.get(c, 0) + 1
+            target.append({"k": "spawned", "c": c, "w": works[c], "o": "none"})
+        else:
+            target.append({"k": "finished", "c": c, "w": works.get(c, 0), "o": line["outcome"]})
+    final = {c: os.path.exists(os.path.join(root, child, "log.jsonl")) for child, c in names.items()}
+    return target, final
+
+
+def tla_str(s):
+    return '"' + s.replace("\\", "\\\\").replace('"', '\\"') + '"'
+
+
+def tla_record(r):
+    return "[" + ", ".join(f"{k} |-> {tla_str(v) if isinstance(v, str) else v}" for k, v in r.items()) + "]"
+
+
+def run_tlc(module, spec_files, generated, cfg, invariant="NotWritten"):
+    work = tempfile.mkdtemp(prefix="fx-log-check-")
+    try:
+        for f in spec_files:
+            shutil.copy(f, work)
+        for name, text in generated.items():
+            open(os.path.join(work, name), "w").write(text)
+        open(os.path.join(work, module + ".cfg"), "w").write(cfg)
+        proc = subprocess.run(
+            # Its own java.io.tmpdir: TLC unpacks its standard modules there,
+            # and parallel runs sharing one folder read each other's
+            # half-written files.
+            [JAVA, "-XX:+UseParallelGC", f"-Djava.io.tmpdir={work}", "-cp", JAR, "tlc2.TLC", "-workers", "1", "-deadlock",
+             "-metadir", os.path.join(work, "states"), "-config", module + ".cfg", module],
+            cwd=work, capture_output=True, text=True, timeout=600,
+        )
+        out = proc.stdout + proc.stderr
+        matched = max([int(m) for m in re.findall(r'"matched_lines", (\d+)', out)] or [0])
+        if f"Invariant {invariant} is violated" in out:
+            return "ACCEPTED", matched
+        if "No error has been found" in out:
+            return "REJECTED", matched
+        return "TOOL ERROR", out[-600:]
+    finally:
+        shutil.rmtree(work, ignore_errors=True)
+
+
+def check_turns(target):
+    body = ", ".join(tla_str(k) for k in target)
+    saved = f"---- MODULE SavedLog ----\nTarget == <<{body}>>\n====\n"
+    cfg = (f"CONSTANT MaxLen = {len(target) + 2}\nSPECIFICATION LogSpec\n"
+           "INVARIANT NotWritten\nCONSTRAINT Progress\n")
+    specs = [os.path.join(TLA, "TurnLifecycle.tla"), os.path.join(HERE, "TurnLifecycleLog.tla")]
+    return run_tlc("TurnLifecycleLog", specs, {"SavedLog.tla": saved}, cfg)
+
+
+def check_children(target, final):
+    children = sorted(final)
+    body = ", ".join(tla_record(r) for r in target)
+    fin = " @@ ".join(f"{tla_str(c)} :> {'TRUE' if final[c] else 'FALSE'}" for c in children)
+    saved = (f"---- MODULE SavedChildren ----\nEXTENDS TLC\nTarget == <<{body}>>\n"
+             f"FinalChildLog == {fin}\n====\n")
+    max_work = max([r["w"] for r in target] or [1])
+    cfg = ("CONSTANTS Children = {" + ", ".join(tla_str(c) for c in children) + "}\n"
+           f"          MaxWork = {max_work}\nSPECIFICATION LogSpec\n"
+           "INVARIANT NotWritten\nCONSTRAINT Progress\n")
+    specs = [os.path.join(TLA, "Subagents.tla"), os.path.join(HERE, "SubagentsLog.tla")]
+    return run_tlc("SubagentsLog", specs, {"SavedChildren.tla": saved}, cfg)
+
+
+def check_fork(copied, source):
+    def seq(rs):
+        return ", ".join(tla_record(r) for r in rs)
+    saved = f"---- MODULE SavedFork ----\nCopied == <<{seq(copied)}>>\nSource == <<{seq(source)}>>\n====\n"
+    cfg = "SPECIFICATION LogSpec\nINVARIANT NotWritten\n"
+    verdict, _ = run_tlc("ForkLog", [os.path.join(HERE, "ForkLog.tla")], {"SavedFork.tla": saved}, cfg)
+    return verdict, len(copied)
+
+
+def jobs_for(roots):
+    jobs = []
+    for root in roots:
+        for sid in sorted(os.listdir(root)):
+            path = os.path.join(root, sid, "log.jsonl")
+            if not os.path.isfile(path):
+                continue
+            name = f"{os.path.basename(os.path.dirname(root.rstrip('/')))}/{sid}"
+            try:
+                raw = read_lines(path, raw=True)
+                lines = [value for value, _ in raw]
+                turns = turn_target(lines)
+                children = child_target(lines, root)
+                fork = fork_target(raw, root)
+            except Unreadable as err:
+                jobs.append((name, "unreadable", str(err)))
+                continue
+            jobs.append((name, "turns", turns))
+            if children[0]:
+                jobs.append((name, "children", children))
+            if fork:
+                jobs.append((name, "fork", fork))
+    return jobs
+
+
+def run(job):
+    name, what, arg = job
+    if what == "unreadable":
+        return name, what, "UNREADABLE", arg
+    if what == "turns":
+        verdict, detail = check_turns(arg)
+    elif what == "fork":
+        verdict, detail = check_fork(*arg)
+    else:
+        verdict, detail = check_children(*arg)
+    size = len(arg) if what == "turns" else len(arg[0])
+    return name, what, verdict, f"{detail}/{size} lines" if verdict != "TOOL ERROR" else detail
+
+
+def selftest():
+    cases = [
+        ("turns: a committed turn, then close", "turns", ["created", "set", "start", "item", "commit", "closed"], "ACCEPTED"),
+        ("turns: crash, reopen interrupts, next turn", "turns", ["created", "start", "item", "interrupt", "start", "commit"], "ACCEPTED"),
+        ("turns: close interrupts the open turn", "turns", ["created", "start", "interrupt", "closed", "start", "commit"], "ACCEPTED"),
+        ("planted: item outside a turn", "turns", ["created", "item"], "REJECTED"),
+        ("planted: two open turns", "turns", ["created", "start", "start"], "REJECTED"),
+        ("planted: closed inside a turn", "turns", ["created", "start", "closed"], "REJECTED"),
+        ("planted: commit without a start", "turns", ["created", "set", "commit"], "REJECTED"),
+        ("children: spawn, finish ok",
+         "children", ([{"k": "spawned", "c": "c1", "w": 1, "o": "none"}, {"k": "finished", "c": "c1", "w": 1, "o": "ok"}], {"c1": True}), "ACCEPTED"),
+        ("children: lost, then a fresh start (D33)",
+         "children", ([{"k": "spawned", "c": "c1", "w": 1, "o": "none"}, {"k": "finished", "c": "c1", "w": 1, "o": "lost"},
+                       {"k": "spawned", "c": "c1", "w": 2, "o": "none"}, {"k": "finished", "c": "c1", "w": 2, "o": "ok"}], {"c1": True}), "ACCEPTED"),
+        ("planted: lost, yet the child has a log",
+         "children", ([{"k": "spawned", "c": "c1", "w": 1, "o": "none"}, {"k": "finished", "c": "c1", "w": 1, "o": "lost"}], {"c1": True}), "REJECTED"),
+        ("planted: interrupted, yet the child has no log",
+         "children", ([{"k": "spawned", "c": "c1", "w": 1, "o": "none"}, {"k": "finished", "c": "c1", "w": 1, "o": "interrupted"}], {"c1": False}), "REJECTED"),
+        ("planted: a finish with no spawn",
+         "children", ([{"k": "finished", "c": "c1", "w": 0, "o": "ok"}], {"c1": False}), "REJECTED"),
+    ]
+    def rec(k, h):
+        return {"k": k, "h": h}
+    src = [rec("set", "p"), rec("start", "a"), rec("item", "b"), rec("commit", "c"), rec("start", "d"), rec("commit", "e")]
+    cases += [
+        ("fork: the source's lines to the end of turn 1", "fork", (src[:4], src), "ACCEPTED"),
+        ("fork: before the first turn", "fork", (src[:1], src), "ACCEPTED"),
+        ("planted: a copied line differs from the source's", "fork", (src[:2] + [rec("item", "x"), src[3]], src), "REJECTED"),
+        ("planted: the copy ends inside a turn", "fork", (src[:3], src), "REJECTED"),
+    ]
+    bad = 0
+
+    def verdict_of(c):
+        if c[1] == "turns":
+            return check_turns(c[2])
+        if c[1] == "fork":
+            return check_fork(*c[2])
+        return check_children(*c[2])
+    with ThreadPoolExecutor(int(os.environ.get("JOBS", "6"))) as pool:
+        results = pool.map(lambda c: (c, verdict_of(c)), cases)
+        for (label, _, _, want), (verdict, detail) in results:
+            ok = verdict == want
+            bad += not ok
+            print(f"{'ok  ' if ok else 'FAIL'}  {label}: {verdict} (matched {detail}), wanted {want}")
+    print(f"selftest: {len(cases) - bad}/{len(cases)} verdicts as required")
+    return 1 if bad else 0
+
+
+def main(argv):
+    if argv[1:] == ["--selftest"]:
+        return selftest()
+    if len(argv) < 2:
+        print(__doc__)
+        return 2
+    jobs = jobs_for(argv[1:])
+    counts = {}
+    failed = 0
+    with ThreadPoolExecutor(int(os.environ.get("JOBS", "6"))) as pool:
+        for name, what, verdict, detail in pool.map(run, jobs):
+            counts[(what, verdict)] = counts.get((what, verdict), 0) + 1
+            if verdict not in ("ACCEPTED", "UNREADABLE"):
+                failed += 1
+            if verdict != "ACCEPTED":
+                print(f"{verdict:10} {what:9} {name}: {detail}")
+    for (what, verdict), n in sorted(counts.items()):
+        print(f"{what:9} {verdict:10} {n}")
+    return 1 if failed else 0
+
+
+if __name__ == "__main__":
+    sys.exit(main(sys.argv))

src/core/session_manager/tla/trace/check_wiring_traces.py

@@ -0,0 +1,155 @@
+#!/usr/bin/env python3
+"""Checks fx's `wiring` trace lines against Wiring.tla (WiringTrace.tla).
+
+usage: check_wiring_traces.py FILE...   trace logs written with FX_TRACE=1,
+                                        FX_TRACE_SCOPES=wiring, FX_TRACE_LOG
+       check_wiring_traces.py --selftest
+
+JOBS=N runs N TLC checks at once (default 6).
+
+The adapter writes one line per step (`action=... session=... pid=...`).
+Each process's first store open and last close become Start and Exit; a
+process whose lines stop without Exit gets a Crash. Wiring.tla models one fx
+process at a time, so a file whose processes overlap is skipped and named.
+Exit 0 when every checked trace is accepted.
+"""
+import os
+import re
+import sys
+from concurrent.futures import ThreadPoolExecutor
+
+sys.path.insert(0, os.path.dirname(os.path.abspath(__file__)))
+from check_saved_logs import HERE, TLA, run_tlc, tla_str  # noqa: E402
+
+LINE = re.compile(r"^\d+ \[wiring\] action=(\w+) session=(\S+)(?: end=(\w+))? pid=(-?\d+)$")
+
+
+class Skip(Exception):
+    pass
+
+
+def parse(path):
+    events = []
+    for raw in open(path, errors="replace"):
+        m = LINE.match(raw.rstrip("\n"))
+        if m:
+            events.append((int(m.group(4)), m.group(1), m.group(2), m.group(3)))
+    return events
+
+
+def steps_for(events):
+    """The Wiring steps, and the sessions they name."""
+    order, seen = [], set()
+    for pid, *_ in events:
+        if pid in seen and order[-1] != pid:
+            raise Skip("processes overlap")
+        if pid not in seen:
+            seen.add(pid)
+            order.append(pid)
+    names, steps = {}, []
+    for pid in order:
+        depth = 0
+        mine = [e for e in events if e[0] == pid]
+        # ACP opens its store before tracing starts: its first line is
+        # then a later step, and the process started just before it.
+        if mine[0][1] != "StoreOpen":
+            steps.append(("Start", "none", "none"))
+            depth = 1
+        for p, action, session, end in mine:
+            if action == "StoreOpen":
+                if depth == 0:
+                    steps.append(("Start", "none", "none"))
+                depth += 1
+            elif action == "StoreClose":
+                depth -= 1
+                if depth == 0:
+                    steps.append(("Exit", "none", "none"))
+            elif depth == 0:
+                raise Skip(f"{action} outside an open store")
+            elif action in ("Open", "Close", "Fork"):
+                steps.append((action, names.setdefault(session, f"s{len(names) + 1}"), "none"))
+            elif action == "EndTurn":
+                steps.append(("EndTurn", "none", end))
+            else:
+                steps.append((action, "none", "none"))
+        if depth > 0:
+            steps.append(("Crash", "none", "none"))
+    return steps, sorted(names.values()) or ["s1"]
+
+
+def check(steps, sessions):
+    body = ", ".join(f"[a |-> {tla_str(a)}, s |-> {tla_str(s)}, e |-> {tla_str(e)}]" for a, s, e in steps)
+    data = f"---- MODULE WiringData ----\nTrace == <<{body}>>\n====\n"
+    cfg = ("CONSTANT Sessions = {" + ", ".join(tla_str(s) for s in sessions) + "}\n"
+           "SPECIFICATION TraceSpec\nINVARIANT NotDone\nCONSTRAINT Progress\n")
+    specs = [os.path.join(TLA, "Wiring.tla"), os.path.join(HERE, "WiringTrace.tla")]
+    verdict, detail = run_tlc("WiringTrace", specs, {"WiringData.tla": data}, cfg, invariant="NotDone")
+    return verdict, detail
+
+
+def run(path):
+    events = parse(path)
+    if not events:
+        return path, "EMPTY", "no wiring lines"
+    try:
+        steps, sessions = steps_for(events)
+    except Skip as why:
+        return path, "SKIPPED", str(why)
+    verdict, detail = check(steps, sessions)
+    if verdict == "REJECTED":
+        step = steps[detail] if detail < len(steps) else None
+        return path, verdict, f"steps 1..{detail} match; step {detail + 1} {step} is not allowed ({len(steps)} steps)"
+    return path, verdict, f"{detail}/{len(steps)} steps" if verdict == "ACCEPTED" else detail
+
+
+def selftest():
+    S, O, B, C, X = ("Start", "none", "none"), ("Open", "s1", "none"), ("BeginTurn", "none", "none"), ("Close", "s1", "none"), ("Exit", "none", "none")
+    O2, C2 = ("Open", "s2", "none"), ("Close", "s2", "none")
+    commit, crash = ("EndTurn", "none", "commit"), ("Crash", "none", "none")
+    spawn, done = ("Spawn", "none", "none"), ("ChildDone", "none", "none")
+    cases = [
+        ("a turn, then close and exit", [S, O, B, commit, C, X], ["s1"], "ACCEPTED"),
+        ("a crash mid-turn, then a resume", [S, O, B, crash, S, O, B, commit, C, X], ["s1"], "ACCEPTED"),
+        ("a child inside a turn", [S, O, B, spawn, done, commit, C, X], ["s1"], "ACCEPTED"),
+        ("planted: close while a child runs", [S, O, B, spawn, C], ["s1"], "REJECTED"),
+        ("a switch: the next session opens before the current closes (D41)", [S, O, B, commit, O2, C, B, commit, C2, X], ["s1", "s2"], "ACCEPTED"),
+        ("a failed switch closes the next session and keeps the current", [S, O, O2, C2, B, commit, C, X], ["s1", "s2"], "ACCEPTED"),
+        ("planted: a third open while a switch is pending", [S, O, O2, ("Open", "s3", "none")], ["s1", "s2", "s3"], "REJECTED"),
+        ("planted: a turn starts while a switch is pending", [S, O, O2, B], ["s1", "s2"], "REJECTED"),
+        ("planted: a turn ends that never began", [S, O, commit], ["s1"], "REJECTED"),
+        ("planted: exit with a session open", [S, O, X], ["s1"], "REJECTED"),
+        ("planted: a child done after its parent closed", [S, O, B, spawn, commit, C, done], ["s1"], "REJECTED"),
+        ("a fork becomes the next session, and closing the source switches to it (D58)", [S, O, B, commit, ("Fork", "s2", "none"), C, B, commit, C2, X], ["s1", "s2"], "ACCEPTED"),
+        ("planted: a fork while a turn is open", [S, O, B, ("Fork", "s2", "none")], ["s1", "s2"], "REJECTED"),
+        ("planted: a fork into a session that exists", [S, O2, C2, O, ("Fork", "s2", "none")], ["s1", "s2"], "REJECTED"),
+    ]
+    bad = 0
+    with ThreadPoolExecutor(int(os.environ.get("JOBS", "6"))) as pool:
+        for (label, _, _, want), (verdict, detail) in zip(cases, pool.map(lambda c: check(c[1], c[2]), cases)):
+            ok = verdict == want
+            bad += not ok
+            print(f"{'ok  ' if ok else 'FAIL'}  {label}: {verdict} (matched {detail}), wanted {want}")
+    print(f"selftest: {len(cases) - bad}/{len(cases)} verdicts as required")
+    return 1 if bad else 0
+
+
+def main(argv):
+    if argv[1:] == ["--selftest"]:
+        return selftest()
+    if len(argv) < 2:
+        print(__doc__)
+        return 2
+    counts, failed = {}, 0
+    with ThreadPoolExecutor(int(os.environ.get("JOBS", "6"))) as pool:
+        for path, verdict, detail in pool.map(run, argv[1:]):
+            counts[verdict] = counts.get(verdict, 0) + 1
+            failed += verdict in ("REJECTED", "TOOL ERROR")
+            if verdict != "ACCEPTED":
+                print(f"{verdict:10} {path}: {detail}")
+    for verdict, n in sorted(counts.items()):
+        print(f"{verdict:10} {n}")
+    return 1 if failed else 0
+
+
+if __name__ == "__main__":
+    sys.exit(main(sys.argv))

src/core/session_manager/tla/trace/selftest.sh

@@ -0,0 +1,42 @@
+#!/bin/sh
+# Prove the trace tooling can both accept and reject.
+#
+# Runs the Python stand-in log three ways and checks the verdicts:
+#   correct implementation            -> ACCEPTED
+#   recovery keeps a torn tail (bug)  -> REJECTED at step 8 (the Recover)
+#   one field changed in a good trace -> REJECTED at step 5 (acked 2 -> 3)
+set -eu
+
+here=$(cd "$(dirname "$0")" && pwd)
+tmp=$(mktemp -d "${TMPDIR:-/tmp}/session-manager-selftest.XXXXXX")
+trap 'rm -rf "$tmp"' EXIT
+
+python3 "$here/stand_in_log.py" "$tmp/good.log" "$tmp/good.ndjson"
+python3 "$here/stand_in_log.py" "$tmp/bad.log" "$tmp/bad.ndjson" keep_torn_tail
+sed '5s/"acked": 2/"acked": 3/' "$tmp/good.ndjson" > "$tmp/tampered.ndjson"
+
+failures=0
+expect() { # name trace wanted_exit wanted_text
+    set +e
+    got=$("$here/validate.sh" SessionLog "$2" 2>&1)
+    code=$?
+    set -e
+    if [ "$code" -eq "$3" ] && printf '%s' "$got" | grep -q "$4"; then
+        echo "ok    $1: $(printf '%s' "$got" | head -1)"
+    else
+        echo "FAIL  $1: exit $code, wanted $3 and '$4'"
+        printf '%s\n' "$got" | sed 's/^/      /'
+        failures=$((failures + 1))
+    fi
+}
+
+expect "correct implementation" "$tmp/good.ndjson" 0 "ACCEPTED"
+expect "recovery keeps a torn tail" "$tmp/bad.ndjson" 1 "step 8 of"
+expect "tampered acked field" "$tmp/tampered.ndjson" 1 "step 5 of"
+
+if [ "$failures" -eq 0 ]; then
+    echo "trace selftest passed"
+    exit 0
+fi
+echo "trace selftest failed: $failures case(s)"
+exit 1

src/core/session_manager/tla/trace/stand_in_log.py

@@ -0,0 +1,115 @@
+#!/usr/bin/env python3
+"""A small stand-in for the L1 log, used only to self-test the trace tooling.
+
+It writes a real file with O_APPEND, fsync and simulated crashes, and emits
+one trace line per step. The state in each line is read back from the actual
+file bytes, the same way the Zig trace hook must do it. Not a design
+reference for the Zig code.
+
+usage: stand_in_log.py LOG_PATH TRACE_PATH [keep_torn_tail]
+"""
+import json
+import os
+import sys
+
+
+class Log:
+    def __init__(self, path, trace, bug=None):
+        self.path, self.trace, self.bug = path, trace, bug
+        self.fd = os.open(path, os.O_WRONLY | os.O_CREAT | os.O_APPEND, 0o600)
+        self.durable = self.acked = 0
+        self.status, self.pending, self.seq = "open", None, 0
+
+    def disk(self):
+        """Abstraction function: file bytes -> (line count, tail done, seqs)."""
+        with open(self.path, "rb") as f:
+            data = f.read()
+        torn = len(data) > 0 and not data.endswith(b"\n")
+        complete = data.split(b"\n")[: data.count(b"\n")]
+        seqs = []
+        for raw in complete:
+            try:
+                seqs.append(int(json.loads(raw)["seq"]))
+            except (ValueError, KeyError, TypeError):
+                seqs.append(-1)
+        return len(complete) + (1 if torn else 0), not torn, seqs
+
+    def emit(self, event):
+        n, done, seqs = self.disk()
+        self.trace.write(json.dumps({
+            "event": event, "log_len": n, "tail_done": done, "seqs": seqs,
+            "durable": self.durable, "acked": self.acked, "status": self.status,
+        }) + "\n")
+
+    def begin_write(self):
+        """First half of one write(): the newline is not on disk yet."""
+        self.seq += 1
+        line = json.dumps({"v": 1, "seq": self.seq, "kind": "item"}).encode() + b"\n"
+        half = len(line) // 2
+        os.write(self.fd, line[:half])
+        self.pending = line[half:]
+        self.status = "writing"
+        self.emit("BeginWrite")
+
+    def finish_write(self):
+        os.write(self.fd, self.pending)
+        self.pending = None
+        self.status = "open"
+        self.emit("FinishWrite")
+
+    def fsync(self):
+        os.fsync(self.fd)
+        self.durable = self.acked = self.disk()[0]
+        self.emit("Fsync")
+
+    def process_crash(self):
+        os.close(self.fd)
+        self.status = "down"
+        self.emit("ProcessCrash")
+
+    def power_loss(self, keep, tear):
+        """Simulated: keep `keep` complete lines (at least durable), then tear
+        the last kept line if it was never fsynced."""
+        if self.status != "down":
+            os.close(self.fd)
+        with open(self.path, "rb") as f:
+            data = f.read()
+        kept = b"".join(p + b"\n" for p in data.split(b"\n")[:keep])
+        if tear and keep > self.durable:
+            kept = kept[:-3]
+        with open(self.path, "wb") as f:
+            f.write(kept)
+        self.status = "down"
+        self.emit("PowerLoss")
+
+    def recover(self):
+        """open(.resume): cut a torn tail, fsync, reopen for append."""
+        with open(self.path, "rb") as f:
+            data = f.read()
+        if data and not data.endswith(b"\n") and self.bug != "keep_torn_tail":
+            data = data[: data.rfind(b"\n") + 1]
+            with open(self.path, "wb") as f:
+                f.write(data)
+        self.fd = os.open(self.path, os.O_WRONLY | os.O_APPEND)
+        os.fsync(self.fd)
+        self.durable = self.disk()[0]
+        self.seq = data.count(b"\n")
+        self.status = "open"
+        self.emit("Recover")
+
+
+def scenario(path, trace_path, bug=None):
+    with open(trace_path, "w") as trace:
+        log = Log(path, trace, bug)
+        log.begin_write(); log.finish_write()
+        log.begin_write(); log.finish_write(); log.fsync()   # 2 acknowledged lines
+        log.begin_write(); log.process_crash()                # torn 3rd line
+        log.recover()                                         # must cut it
+        log.begin_write(); log.finish_write()                 # new 3rd line, not fsynced
+        log.power_loss(keep=3, tear=True)                     # machine crash tears it
+        log.recover()
+        log.begin_write(); log.finish_write(); log.fsync()
+
+
+if __name__ == "__main__":
+    scenario(sys.argv[1], sys.argv[2], sys.argv[3] if len(sys.argv) > 3 else None)

src/core/session_manager/tla/trace/to_tla.py

@@ -0,0 +1,59 @@
+#!/usr/bin/env python3
+"""Convert an implementation trace (JSON lines) into the TLA+ module TraceData.
+
+usage: to_tla.py trace.ndjson TraceData.tla
+
+Each JSON line becomes one record in `Trace == << ... >>`. Values map as:
+  true/false -> TRUE/FALSE, integers -> integers, strings -> strings,
+  lists -> sequences, objects -> records, {"$set": [...]} -> a set.
+Floats and null are rejected: the specs have no use for them.
+"""
+import json
+import sys
+
+
+def value(v):
+    if isinstance(v, bool):
+        return "TRUE" if v else "FALSE"
+    if isinstance(v, int):
+        return str(v)
+    if isinstance(v, str):
+        return json.dumps(v)
+    if isinstance(v, list):
+        return "<<" + ", ".join(value(x) for x in v) + ">>"
+    if isinstance(v, dict):
+        if set(v) == {"$set"}:
+            return "{" + ", ".join(value(x) for x in v["$set"]) + "}"
+        if not v:
+            raise ValueError("empty objects have no TLA+ record form")
+        return "[" + ", ".join(f"{k} |-> {value(x)}" for k, x in v.items()) + "]"
+    raise ValueError(f"unsupported trace value: {v!r}")
+
+
+def main():
+    if len(sys.argv) != 3:
+        print(__doc__.strip().splitlines()[2], file=sys.stderr)
+        return 2
+    records = []
+    with open(sys.argv[1]) as trace:
+        for number, line in enumerate(trace, start=1):
+            if not line.strip():
+                continue
+            try:
+                records.append(value(json.loads(line)))
+            except (ValueError, json.JSONDecodeError) as err:
+                print(f"trace line {number}: {err}", file=sys.stderr)
+                return 2
+    body = ",\n  ".join(records)
+    with open(sys.argv[2], "w") as out:
+        out.write("---- MODULE TraceData ----\n")
+        # Integers gives negative literals (for example a seq of -1 for a
+        # line the implementation could not parse).
+        out.write("EXTENDS Integers\n")
+        out.write(f"Trace == <<\n  {body}\n>>\n" if records else "Trace == <<>>\n")
+        out.write("====\n")
+    return 0
+
+
+if __name__ == "__main__":
+    sys.exit(main())

src/core/session_manager/tla/trace/validate.sh

@@ -0,0 +1,79 @@
+#!/bin/sh
+# Check that an implementation trace is a behavior of a spec.
+#
+# usage: ./validate.sh SPEC trace.ndjson
+#   SPEC is a spec with a trace wrapper here, for example SessionLog.
+#   Needs ../SPEC.tla, ./SPECTrace.tla and ./SPECTrace.cfg.
+#
+# Exit codes: 0 accepted, 1 rejected (prints the first step the spec does
+# not allow), 2 tool or usage error.
+set -u
+
+if [ "$#" -ne 2 ]; then
+    echo "usage: $0 SPEC trace.ndjson" >&2
+    exit 2
+fi
+spec=$1
+here=$(cd "$(dirname "$0")" && pwd)
+trace=$(cd "$(dirname "$2")" && pwd)/$(basename "$2")
+
+for f in "$here/../$spec.tla" "$here/${spec}Trace.tla" "$here/${spec}Trace.cfg" "$trace"; do
+    if [ ! -f "$f" ]; then
+        echo "missing $f" >&2
+        exit 2
+    fi
+done
+
+jar="${TLA2TOOLS_JAR:-$HOME/.local/share/tla/tla2tools.jar}"
+java=""
+for candidate in \
+    "${JAVA_HOME:+$JAVA_HOME/bin/java}" \
+    /opt/homebrew/opt/openjdk/bin/java \
+    /usr/local/opt/openjdk/bin/java \
+    "$(command -v java 2>/dev/null || true)"; do
+    if [ -n "$candidate" ] && [ -x "$candidate" ] && "$candidate" -version >/dev/null 2>&1; then
+        java="$candidate"
+        break
+    fi
+done
+if [ -z "$java" ] || [ ! -f "$jar" ]; then
+    echo "needs a Java runtime and tla2tools.jar (see ../check.sh)" >&2
+    exit 2
+fi
+
+work=$(mktemp -d "${TMPDIR:-/tmp}/session-manager-trace.XXXXXX")
+trap 'rm -rf "$work"' EXIT
+cp "$here/../$spec.tla" "$here/${spec}Trace.tla" "$here/${spec}Trace.cfg" "$work/"
+python3 "$here/to_tla.py" "$trace" "$work/TraceData.tla" || exit 2
+steps=$(grep -c . "$trace" || true)
+
+# One worker: the progress register (TLCSet/TLCGet) is per worker. TLC
+# unpacks its standard modules into java.io.tmpdir; a private one lets
+# several checks run at once.
+mkdir "$work/java-tmp"
+out=$(cd "$work" && "$java" -Djava.io.tmpdir="$work/java-tmp" -cp "$jar" tlc2.TLC -deadlock -workers 1 -cleanup \
+    -metadir "$work/states" -config "${spec}Trace.cfg" "${spec}Trace.tla" 2>&1)
+
+# Match with case, not a pipe into grep -q: grep exits at the first match
+# and a large TLC output then fails printf with a broken pipe.
+case $out in
+    *'Invariant TraceIncomplete is violated'*) verdict=accepted ;;
+    *'No error has been found'*) verdict=rejected ;;
+    *) verdict=unfinished ;;
+esac
+
+if [ "$verdict" = accepted ]; then
+    echo "ACCEPTED: all $steps steps are a behavior of $spec"
+    exit 0
+fi
+if [ "$verdict" = rejected ]; then
+    matched=$(printf '%s\n' "$out" | sed -n 's/.*"matched_lines", \([0-9]*\)>>.*/\1/p' | tail -1)
+    matched=${matched:-0}
+    bad=$((matched + 1))
+    echo "REJECTED: steps 1..$matched match; step $bad of $steps is not allowed by $spec:"
+    sed -n "${bad}p" "$trace"
+    exit 1
+fi
+printf '%s\n' "$out" | tail -15
+echo "TOOL ERROR: TLC did not finish the trace check" >&2
+exit 2

src/core/session_manager/trace.zig

@@ -2,7 +2,7 @@
 //!
 //! Each traced run writes `zig-out/traces/SPEC--CASE.ndjson`: one JSON line
 //! per spec action, named like the action, with one field per spec variable
-//! (`docs/session-manager/tla/trace/README.md`). Fields that model the disk
+//! (`tla/trace/README.md`). Fields that model the disk
 //! are read back from the real files after the step; fields that model
 //! memory come from the code's own state.
 //!

src/core/subagent/tool_host.zig

@@ -153,7 +153,7 @@ pub const Runtime = struct {
 
     /// A host over a v2 parent, whose children live in its log (D22).
     /// Borrows `children` and the callback contexts until deinit; the
-    /// parent stays open until then (`tla/Wiring.tla`
+    /// parent stays open until then (`src/core/session_manager/tla/Wiring.tla`
     /// ParentOutlivesChildren).
     pub fn createV2(
         alloc: Allocator,

src/mcp/io/trace.zig

@@ -1,4 +1,4 @@
-//! JSONL trace of core steps (docs/approach.md §6, format version 1).
+//! JSONL trace of core steps (format version 1).
 //!
 //! The I/O layer writes one line per `step` call when tracing is on. The Bun
 //! bridge turns a trace into a TLA+ observation and asks TLC whether it is a

src/mcp/mcp.zig

@@ -1,7 +1,7 @@
 //! MCPv2 module root and public API.
 //!
 //! Files under `src/mcp/` import only `std` and each other. The host passes in
-//! `std.Io` and everything else through `host.zig`. See `docs/approach.md`.
+//! `std.Io` and everything else through `host.zig`.
 
 const std = @import("std");
 

tests/e2e/sessions-v2.test.ts

@@ -2025,9 +2025,9 @@ test("a crash while a named subagent works records it interrupted, and its next
     expect(JSON.parse(resumed.stdout).output).toBe("AFTER_LOST_DONE");
 
     // The reopen recorded the started work as interrupted, as
-    // `tla/Subagents.tla` repairs a child with a log; the next message is new
-    // work for the same child. A child streams no pieces, so its log holds
-    // nothing of the lost work.
+    // `src/core/session_manager/tla/Subagents.tla` repairs a child with a
+    // log; the next message is new work for the same child. A child streams
+    // no pieces, so its log holds nothing of the lost work.
     const lines = childLines(fixture, id);
     expect(lines.map((line) => [line.kind, line.outcome ?? null])).toEqual([
       ["child_spawned", null], ["child_finished", "interrupted"], ["child_spawned", null], ["child_finished", "ok"],