# 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:

- `<Name>.tla` + `<Name>.cfg` — the model and its pinned small config (cfg comments document
  what N proves what and what stays unexplored). Doc-stage tags (`[<doc>->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).

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/<name> && java -cp <tla2tools-1.8.0.jar> tlc2.TLC -workers auto -config <Name>.cfg <Name>.tla
```

(jar: https://github.com/tlaplus/tlaplus/releases/download/v1.8.0/tla2tools.jar,
sha256 9e27b5e19a69ae1f56aabf8403a6ed5598dbfa6e638908e5278ac39736c1543d — same pin as CI.)

## 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.