# specs/ — living TLA+ models Checked design documents for spt-core's crash/recovery and replication protocols. Discipline, scope, and acceptance gates: ADR-0035; glossary: CONTEXT.md §formal specs. Each spec dir holds: - `.tla` + `.cfg` — the model and its pinned small config (cfg comments document what N proves what and what stays unexplored). Doc-stage tags (`[->REQ-*]`-shaped, bare stage word in real specs) sit above the invariant definitions. - `SOURCES.txt` — the machine-readable module map. The CI **spec-drift gate** reads it: a PR touching a listed path must also touch this spec dir, or carry `[spec-nochange]` in a commit message (loud waiver, recorded in history). - `weakened/` — the **fidelity gate**: variants that deliberately re-introduce recorded historical bugs. CI runs them expecting an invariant violation; a weakened variant going GREEN fails the build (the model lost the fidelity that made it trustworthy). Weakened variants are excluded from traceability scanning (deliberately broken ≠ evidence). **Both failure directions are gated, and the second one is easy to forget.** Going green is one; killing the *wrong* invariant is the other — a variant that still violates *something* looks fine to a gate that only greps for "a violation", so the kill-mapping can drift silently and the gate reports fidelity it no longer has. Every weakened cfg therefore carries a machine-readable `\* expects: […]` line, and the gate requires the invariant TLC actually reports to be one of those. The line is **mandatory** — a cfg without it is a hard error, so a new variant cannot opt out by omission. Use `\* expects: TEMPORAL` when the recorded bug is a liveness failure. Note the check earns most of its keep where a cfg lists *several* `INVARIANTS`: with a single-invariant cfg TLC can only report the one, but a broad list makes any violation look like the intended one. **Known boundary of this gate: a variant expected to go GREEN is inexpressible here, because green is the gate's failure signal.** That matters for a variant flipping two guards at once, since TLC halts at the *first* violation and can only ever witness one of them. `RenameFollow` is the case in this tree: it flips `CanonicalExe` and `BytesGate` together and reports `InvAppliedTruthful`, so `InvRespawnBytes` is never reached. Measured before assuming (TLC 2.19, each half alone, full invariant list): `CanonicalExe=FALSE` alone → **no violation** (2048 distinct); `BytesGate=FALSE` alone → **no violation** (3362 distinct, i.e. the main model's own count). So the pair is genuine defense-in-depth, not two independent bugs — with `CanonicalExe=TRUE` no stale-bytes candidate is ever produced, leaving `BytesGate` nothing to gate and its removal unobservable. **Do not "helpfully" split `RenameFollow` into single-flip variants: neither half violates alone, so both would go green and fail the gate.** Each half is instead pinned in product tests under `REQ-HAZARD-BRAIN-RESPAWN-PATH` — `select_brain_exe_prefers_canonical_over_per_spawn_current_exe` and `ready_but_wrong_bytes_rolls_back_never_promotes` in `brainproc.rs`, plus the `crates/spt/tests/brain_respawn_rename.rs` E2E. CI: the `tla` job (kitsubito-only, required) — TLC over every `specs/*/*.cfg` (must pass), every `specs/*/weakened/*.cfg` (must fail), then the drift gate. Run locally: ``` cd specs/ && java -cp tlc2.TLC -workers auto \ -metadir "$(mktemp -d)" -config .cfg .tla ``` (jar: https://github.com/tlaplus/tlaplus/releases/download/v1.7.4/tla2tools.jar, sha256 936a262061c914694dfd669a543be24573c45d5aa0ff20a8b96b23d01e050e88 — same pin as CI.) Three things that look optional and are not: - **Use the v1.7.4 STABLE jar, not v1.8.0.** The `v1.8.0` tag is a *prerelease* and is republished continuously — its jar self-reports `TLC2 Version 2026.07.18.145032`, a build timestamp. Pinning a sha256 against it goes red on every upstream rebuild. - **Pass `-metadir`.** TLC names its run directory from the clock, and on 2.19 that name is second-resolution. These models finish in well under a second, so consecutive runs collide and abort *before* model-checking — which reads as a spec failure and is not one. - **Clean TLC litter out of the spec dir before you exit.** A local run drops `states/` into the spec dir, and a run that finds a violation also drops a `_TTrace_.tla` trace module next to the model. Both are `.gitignore`d, so they will not reach a commit — but the ignore is a backstop, not the fix. The bite is CI's fidelity loop, which resolves the module name with `mod=$(basename "$specdir"/*.tla .tla)`: a leftover `_TTrace_` module makes that glob match two files and the job fails on a name that is not a spec. In CI the `-metadir` under `$RUNNER_TEMP` keeps the run directory out of the tree entirely; locally, `-metadir "$(mktemp -d)"` plus deleting any `*_TTrace_*` you generated is the equivalent. ## Spec ↔ module map | Spec | Source modules | Status | |------|----------------|--------| | `brain_handoff/` (wave 1, pilot) | see `brain_handoff/SOURCES.txt` — brainproc/brain/update/applyhost + spt-store epoch | checked — main cfg green (3362 states); all 4 weakened variants re-find their recorded bug (enlyzeam optimistic-applied, 22:47 false-promote, v0.4.1 rename-follow, KH 4.8 epoch dup); pending design review | ## Candidate backlog (surveyed 2026-07-08, TLA+ grill) Ranked by expected payoff. Each entry names the protocol, the invariant class already stated in prose, and why it is (or is not) model-checker-shaped. ### Strong fits 1. **Broker↔brain promote/rollback/generation protocol + epoch single-writer** — wave 1 (above). Historically wedged (BROKER-BRAIN-SPLIT-RESTORATION); epoch ownership is a prose convention with no lock (`epoch.rs`), violation windows = brain-dead/handoff windows. Safety: never two live brains; no false-promote; single epoch writer; `applied` ⟹ running code is new. Liveness: promote-or-rollback, no wedge. 2. **Registry CRDT convergence + endpoint status derivation** — wave 2. Epoch-lease merge (`merge_instance`), Active/Dormant/Suspended/Offline under partition, ghost-heal, never-self-gossip-Offline, cold→Suspended-never-Dormant. Safety: no false-ONLINE. Liveness: eventual convergence to true state. Directly targets the slow/inconsistent discovery pain — and separates *wrong* (missed transition) from *slow* (cadence math, out of scope). 3. **Broker gapless-handoff seq/ring/resume** — bounded `OutputLog` ring + `subscribe last_seq+1` replay across brain restart. Open question with definitive checker answer: can a restart window evict unreplayed output? Safety: no gap, no duplicate, in-order. 4. **Message delivery axes** — window (default/idle-only/active-only) × channel (unrestricted/prefer-native/force-native) × persistence (durable/ephemeral). Ratified core property: only ephemeral drops silently; everything else spools and reports (REQ-HAZARD-IDLE-SILENT-NONDELIVERY carve-out). One leg already known PARTIAL (relay no-live-listener ephemeral evaporation) — model documents the exact contract before that leg is finished. 5. **Instance lifecycle cross-node** — active/dormant/suspended/offline, driver-attach, attention-shift, wake resolution, transition echo commune, deferred-message gate. Properties: at-most-one-active-per-ID convergence; no lost wake; deferred messages never starve forever. 6. **Mixed-version subnet (N/N-1 rollout)** — brain↔broker ABI window, peer update propagation with every-hop re-gating, epoch rows from old nodes. The CI N-1 gate tests one pairing empirically; a model checks the version lattice generally. 7. **Pump due/stagger/poisoned-read escalation** — prime-all-on-restart, wake markers, poisoned-client → supervised-restart-never-retry (the 2.2h hfenduleam wedge class). Liveness: every leg eventually runs. Safety: no unbounded block. ### Moderate fits 8. **Perch bind lifecycle** — seed → skeleton → live; PID-recycling defense (KH 5.1); boot nonce vs stale duplicate (KH 2.4); session-id rotation credential (ADR-0032, stranded-perch hazard). Small state machine, subtle crash-respawn races. 9. **Rename / fork / join-time collision** — concurrent rename × concurrent subnet join. Rare ops, but identity corruption has high blast radius. 10. **Notif replication** — per-subnet replicated spool, eventually-consistent dismiss, resurface gating (per-endpoint seen-set + cross-endpoint suppression timeout). Properties: undismissed eventually surfaces; dismissed never resurfaces after convergence; no ping-pong nagging. 11. **Mind-sync merge** — version-vector precedence, concurrent writes surface as explicit conflict never silent newest-wins (KH 6.5), single reconciler (active instance's node). Classic replicated-store spec; moderate because the custom merge driver + Psyche reconcile make the model boundary wide. ### Poor fits (do not spend TLA+ here) - **Viewer eviction, PTY input backpressure, bounded-queue wedges** — in-process memory-model concurrency. That's **loom** territory (Rust interleaving permutation), not TLA+ (message/process interleavings). - **Adapter live update** (stop/swap/restart resident binary) — sequential local orchestration; tests cover it. - **Presence MRA** — trivially convergent; skew → duplicate surface is accepted behavior. - **Discovery latency numbers** — TLA+ finds wrong, not slow. Cadence/TTL tuning is arithmetic.