---
name: tla-spec-pilot-progress
description: "ADR-0035 living-TLA+-specs pilot — now PR #122 on ORIGIN (#65 is the dead mirror). Pilot COMPLETE on substance @fdb4b42, all gates measured green; parks only on TRACEABLE_REQS_TOKEN."
metadata: 
  node_type: memory
  type: project
  originSessionId: bbac2312-aca2-4666-95cf-7a0e2144bf3e
  modified: 2026-07-29T16:07:21.709Z
---

ADR-0035 = living TLA+ specs for crash-recovery protocols (CI-gated fidelity, catches spec↔code drift). Agent **chert** (RENAMED from hertz 2026-07-09 — send to `chert`) = TLA+/docs-reorg lane (isolated `.worktrees/spec-pilot` + `.worktrees/docs-reorg`); **doyle** design-reviews/gates; spec review == design review (ratified Q9 flow). Pilot = `spec/brain-handoff-pilot` (PR **#65**, stacked on **#64** docs-reorg). Models ADR-0018 promote/rollback + `epoch.rs` single-writer; main cfg green **3362 states**, 5 invariants; 4 weakened variants each re-find a recorded production bug.

**doyle 4 DESIGN-REVIEW RULINGS (2026-07-09, PR#65 comment; chert folded @dc4abc6):**
1. model-boundary (broker-crash/A9, output ring/seq, liveness DEFERRED to wave-1) — APPROVE (pilot rightly bounds scope).
2. mint `REQ-HAZARD-EPOCH-SINGLE-WRITER` — YES, minted doc-stage, scope BOTH dims (intra-brain funnel + cross-process).
3. **THE meaty one — do brain epoch mint sites SERIALIZE or race? ANSWERED via code: SERIALIZED, model assumption SOUND.** All live-brain canonical-`epoch_file()` mints funnel through ONE `Arc<RegistryHost>` `Mutex<EpochSource>` (registry advertise registryhost.rs:466/548/591 + pump UPDATE leg pump/update.rs:161, both via `with_epoch`); other listed sites mint DISTINCT counter files (pump-ops=`paths.ops`, psyche/notif=`psyche_ops_epoch_file()` lifecycle.rs:1084, cli-ops=`cli-ops.json`). No intra-brain lost-update. **BUT the serialization is by CONVENTION not construction** — `next_epoch` caches `current` in-memory (no re-read), so a 2nd EpochSource over the same file would REWRITE DOWNWARD + reissue consumed epochs (worse than lost-update). Two guards keep it safe: single-Arc funnel + broker touches canonical epoch only in brain-dead windows (brainproc.rs:566 D6 rollback). **CROSS-PROCESS HOLE FOUND (real, outside model scope): CLI `cmd_notify` (cli.rs:4363) + `fire_spawn_consent_notif` (cli.rs:10986) mint canonical `identity/epoch` UNGUARDED (bare `EpochSource::load()`, no daemon-forward, no lock) concurrently with a live brain.** epoch.rs doc (11-19) names only the broker, misses these. Folded to wave-1 boundary list + REQ-HAZARD-EPOCH-SINGLE-WRITER scope. Pilot's first real-bug yield.
4. broker-mint-atomic — reword: `atomic_write` = crash-consistency, NOT mutual exclusion (two minters both read N, both rename N+1 = lost update). Safety comes from the funnel + brain-dead-window rule, not atomicity. chert reworded to thread-structure.

**EXECUTION PLAN GATED APPROVED (doyle 2026-07-09, PR#65 comment):** plan file was chert scratchpad `adr-0035-execution-plan.md`. Shape sound, all 5 sequencing pins honored, no scope balloon. Pilot files `specs/brain_handoff/`: `BrainHandoff.tla` (5 guard CONSTANTS GateDrain/TwoPhaseApplied/CanonicalExe/BytesGate/EpochGuard) + main `.cfg` (3362 states, invs InvAppliedTruthful/InvNoFalsePromote/InvRespawnBytes/InvEpochNoDup/InvRecordShape) + 4 `weakened/*.cfg` + `SOURCES.txt` drift-map. **Weakened→bug map:** AppliedBeforeReady→enlyzeam v0.3.2 applied.json; NoDrainGate→22:47 false-promote; RenameFollow→v0.4.1 rename-follow KH6.11; EpochDualWriter→KH4.8 lost-update.

**FIDELITY GATE (doyle-hardened, = pilot DoD) = 3 parts:** (a) TLC green on main cfg + (b) weakened-variant discipline committed (each re-finds its recorded bug; §2-step-4 greps for an ACTUAL invariant violation so a wrong-reason/parse failure is rejected — the rigor that makes must-FAIL mean something) + (c) **CI TLC job STOOD UP & gating** (ADR-0035 = *living* specs; a one-shot local model is NOT the deliverable). CI job = `ci.yml` `tla`, kitsubito, tla2tools 1.8.0 sha-pinned, 15min cap, steps: java-preflight / checked-specs-PASS `specs/*/*.cfg` / weakened-must-FAIL `specs/*/weakened/*.cfg` / spec-drift-gate (PR-only: touch SOURCES.txt paths → must touch spec dir or `[spec-nochange]`).

**⚠ HARD MERGE-BLOCKER (doyle pin):** the `tla` job lands IN #65 → once merged, `ci.yml` on main runs it every push. **Do NOT merge #65 until Java on kitsubito AND `tla` GREEN on the #65 PR run** — else main goes RED fleet-wide (W2/releases inherit red base).
**✅ JAVA BLOCKER CLEARED 2026-07-29 (doyle):** `default-jre-headless` (OpenJDK 21.0.11) installed on kitsubito + `~/tla/tla2tools.jar` staged (TLC 2.19 smoke-tested via `java -cp ~/tla/tla2tools.jar tlc2.TLC -h`). Install done in a quiet window, no live build collision. W-SPEC (access-model spec, milestone A ACCESS-CONTROL) no longer gated on java; CI `tla` job wants a sha-pinned tla2tools download step regardless (don't depend on the home-dir jar).

**🔥 FIRST REAL CI EXECUTION 2026-07-29 — PR #122 on ORIGIN (run 30443…/30448474189, head b253c2c).** #65 on the mirror was never re-runnable ([[mirror-repo-ci-dead]]); chert rebased `spec/brain-handoff-pilot` cfd97a8→b253c2c onto main @ffc7e9e and re-opened on `BigscreenVR/spt-bs-core`. ⚠ **A CONFLICTING PR PRODUCES NO `pull_request` RUN AT ALL** — GitHub builds the run from a merge commit it cannot create, so #122 sat with ZERO checks and looked like a queue delay; `mergeable:CONFLICTING`/`mergeStateStatus:DIRTY` was the tell. Verdicts: **java PASS** (openjdk 21.0.11 — 2026-07-09 blocker cleared, measured not assumed); **tla job RAN** (parses/schedules/checks out/preflights) but **died at the fetch step, so model-check + fidelity gate + spec-drift gate are STILL UNEXECUTED**; **sha pin TRIPPED**.

**⭐⭐ THE PIN IS THE WRONG SHAPE (not a bump).** tlaplus **`v1.8.0` is `prerelease=true` — the ONLY prerelease in the repo — and is a ROLLING NIGHTLY under a fixed tag**: asset `created_at` 2026-07-18 (pin authored 2026-07-09), and the jar self-reports `TLC2 Version 2026.07.18.145032` — *the version string is a build timestamp*. So sha256-pinning that URL is a tripwire on a moving target that goes red at every upstream rebuild, forever. Bumping 9e27b5e1→cc4803dc would be green today, red next nightly. **Proposed instead: pin the stable line v1.7.4** — asset `created_at == updated_at` 2024-08-08, untouched ~2 years — `sha256=936a262061c914694dfd669a543be24573c45d5aa0ff20a8b96b23d01e050e88`, size 2274532 (== kitsubito's independently-downloaded `~/tla/tla2tools.jar`, self-reports TLC 2.19 of 08 Aug 2024). ⚠ **Verification honesty: every observation still traces to GitHub** (tla2tools is NOT on Maven Central under `org/lamport` — 404), so what's proven is internal consistency across independent observations, NOT non-GitHub provenance. ✅ **TLC 2.19 COMPAT VERIFIED 2026-07-29 (chert, announced kitsubito window): 14/14** — both main cfgs green with distinct-state counts EXACTLY matching the nightly (3362 / 123842; two TLC versions two years apart = version-robustness evidence), all 12 weakened still fail each on its OWN invariant, kill-mapping undrifted. ⭐ **COMPANION DEFECT the run exposed: TLC 2.19 metadirs are SECOND-resolution** (nightly = millisecond) — back-to-back sub-second runs in the CI for-loop collide ("directory already exists" abort pre-model-check), which the wrong-reason grep correctly classifies as job-fail ⇒ pin move alone = nondeterministic false-red loop. **doyle RULED: ONE commit, both halves** — pin 9e27b5e1→936a2620 + `-metadir "$RUNNER_TEMP/tlc/<specdir>-<cfgname>"` on BOTH loops, mechanism named in commit message. **Commit = `7c920a1`** (local scratch branch `spec/brain-handoff-pilot-rebase` in `.worktrees/pilot-rebase`; 2 files, +36/-10; also moves `specs/README.md`, which was carrying the dead pin labelled "same pin as CI"). **PUSH HELD** by doyle's box sequencing (todlando block → hertz → chert push window; #122 unmergeable anyway until operator lands TRACEABLE_REQS_TOKEN). ⚠ `-metadir` was VERIFIED not assumed (flag accepted on 2.19, 3 runs correct verdicts) — but the **control did NOT reproduce the collision locally** (Windows JVM startup crosses the second boundary), so the bug rests on ONE kitsubito observation, quoted verbatim in the commit; the fix removes the class by construction, not by tuning.

**⏳ THIRD RED on #122, NOT the spec: Windows Phase B `daemon_hosts_lifecycle_and_survives_brain_restart`** (`daemon_e2e.rs:334`, "child exit must reap the session from the broker table"). Classified **environmental-suspect, NOT seam-touched**, on four checks: branch's ENTIRE `crates/` delta is comment-only (grep of changed non-comment lines = empty set); same test green on the SAME box 20min earlier in #121 (182/182); no concurrent run (#121 ended 11:53:57Z, mine started 11:58:27Z); NOT FLAKE-LEDGER #9's `set_var` class (anchored `^#\[test\]` count = 1, same exclusion as brain_survive/n1_pairing). Mechanism = bounded-window assertion, 200×10ms = **hard 2s ceiling** on child-exit→broker reap; load pushes it toward RED. **doyle fires leg-1 single-job at-sha rerun @6a8c8505** (NOT `--failed` — would re-burn tla+traceability for zero info). Green ⇒ environmental; 2nd red ⇒ defect, dispatch by mechanism (reap-path product defect → todlando, too-tight test ceiling → hertz).
⏳ **OPEN: #122 Windows Phase B red** — daemon_e2e::daemon_hosts_lifecycle_and_survives_brain_restart, :334 2s reap-window assertion. Classified environmental-suspect NOT seam-touched (crates/ delta comment-only, verified independently by chert+doyle; same test green same box 20min earlier in #121's leg; sequential runs, no contention; load pushes window toward red). Leg 1 = single-job at-sha rerun (sha 6a8c8505, NOT --failed which re-burns known reds) — doyle fires it after hertz's lane. 2nd sighting = defect, dispatch by mechanism (reap-path → todlando, test ceiling → hertz). ⭐ unwired-notify consequence FIELD-CONFIRMED: informant ping listed traceability+test, tla ABSENT (notify.needs omits it) — ruling stands, recorded.

**✅ TLA LEG GREEN 2026-07-29 — run 30462297623 @93c4017 (chert push 14:43, force-with-lease clean).** tla job 10s, ALL THREE gates measured for the first time: fetch PASS (v1.7.4 pin 936a2620 resolves+matches, tripwire class gone); jar identity verified from run output (TLC2 2.19 rev 5a47802 = local rig ⇒ 14/14 compat evidence TRANSFERS); main model "No error" 8457 generated / **3362 distinct = EXACT match local 2.19 + original nightly (three independent executions state-for-state)**; fidelity gate green (all 4 weakened violated); spec-drift exit 0 vs BASE=ffc7e9e. Traceability red = token blocker, expected. Reap-red closed UNEXPLAINED-mechanism (see [[w3-engine-room-progress]]); 2nd Windows sighting fires recurrence protocol.
**⚠ FIDELITY-GATE GAP (chert-found, doyle-ruled, chert-CORRECTED 2026-07-29): kill-mapping not gated by the generic violation grep — but the real exposure is W-SPEC, not the pilot.** Chert's correction: 3 of 4 pilot weakened cfgs RESTRICT their INVARIANTS list to the expected one(s) ⇒ kill-mapping enforced STRUCTURALLY (TLC can't report an undeclared invariant); only RenameFollow exposed (lists 2 — a half-regressed pair fix stays green). **W-SPEC access_model: all EIGHT weakened cfgs list all NINE invariants — generic grep genuinely blind (8×9). Count fix: W-SPEC has 8 variants, not 12 (12 was the combined compat total, 4+8).** **RULED: rider rides PILOT (#122) = commit `6fce813`** (amended from 808a3e0: six-path list folded into ci.yml gate block, cases 1+6 flagged as mis-parse detectors) — `\* expects: <Inv> [<Inv>...]` per weakened cfg; gate extracts + requires membership of TLC's actually-reported invariant; **missing expects line = HARD ERROR** (forces W-SPEC's eight to declare at land); `expects: TEMPORAL` escape for liveness variants; non-violation wrong-reason message kept. ⭐ ERE trap chert caught BY TESTING: `'^\\*'` quoting didn't survive ⇒ empty extract ⇒ fail-closed would red every variant for the wrong reason (the exact class the gate catches) — now `'^.\* *expects:'` + six decision paths simulated offline. README pairs both directions generically (SilentReMint is access_model, not visible to pilot README readers). **✅ RIDER GREEN — run 30464698675 @6fce813**: all four kill-mapping-OK lines executed on the real extractor (mis-parse discharged by MEASUREMENT — the all-four-hard-error signature did not appear); main model still exact 8457/3362. W-SPEC option at land: ALSO restrict INVARIANTS lists (structural belt + expects suspenders) — ⭐ TLC-halts-at-FIRST-violation now EMPIRICAL (RenameFollow reported only InvAppliedTruthful, InvRespawnBytes never reached).
**✅ RESOLVED BY MEASUREMENT — RenameFollow pair is DEFENSE-IN-DEPTH, and the split is IMPOSSIBLE, not merely unattractive (chert 2026-07-29, commit `fdb4b42`, run 30466921260 green).** Ran each half alone on TLC 2.19 with the FULL five-invariant list (excluding any invariant would have presupposed the answer): `CanonicalExe=FALSE` alone → **NO violation**, 5646 gen / 2048 distinct; `BytesGate=FALSE` alone → **NO violation**, 8607 gen / **3362 distinct = the MAIN MODEL'S OWN count**. ⭐ That equality IS the mechanism, not a coincidence: with `CanonicalExe=TRUE` no stale-bytes candidate is ever produced, so `BytesGate` has nothing to gate and its removal is literally **unobservable** — same reachable distinct states as the shipped protocol. Asymmetric defense-in-depth: canonical **prevents**, bytes-gate **catches** if prevention fails. ⭐⭐ **KEEPER — the gate's boundary, now written verbatim into `specs/README.md` AND `RenameFollow.cfg` next to an explicit do-not-split instruction: a variant expected to go GREEN is INEXPRESSIBLE in this gate, because green is its failure signal.** Splitting would yield two expected-green variants and red the build. **No hertz seed** — checked rather than assumed, since "no seed" is the claim needing evidence: both unwitnessable halves are pinned under `REQ-HAZARD-BRAIN-RESPAWN-PATH` (`select_brain_exe_prefers_canonical_over_per_spawn_current_exe` brainproc.rs:1843 + `bytes_gate_truth_table` 1868 + behavioral `ready_but_wrong_bytes_rolls_back_never_promotes` 1885 + E2E `crates/spt/tests/brain_respawn_rename.rs`). Minor unfixed nit: that cfg cites the E2E as `tests/…` but it lives at `crates/spt/tests/`, not `crates/spt-daemon/tests/` — left to ride the next touch. Method notes worth reusing: jar provenance established **by sha256 against the CI pin** (not filename/ownership), and the verification run done in a **scratchpad copy** of the spec dir because a violating run emits a `_TTrace_` module — the litter trap documented two commits earlier.

**🏁 PILOT COMPLETE ON SUBSTANCE @`fdb4b42`** (run 30466921260: tla ✅, both n1-gates ✅, both test legs ✅, changes ✅, notify ✅; traceability ❌ = token only). Windows reap-red now green **four consecutive runs** — still ledgered UNEXPLAINED, not reclassified. Everything ADR-0035 claimed is measured not asserted: unrottable pinned fetch, exact model check across three independent executions, fidelity gated on WHICH invariant, spec-drift green, and **two gate defects found by verifying the gate itself rather than banking its green**. #122 parks on `TRACEABLE_REQS_TOKEN` (doyle holds the operator item).

**NEXT LEG (proposed to doyle, awaiting dispatch):** rebase `spec/access-model` (W-SPEC) onto the pilot @fdb4b42 — **stacking on an unmerged branch, not waiting for one**. Apply both banked decisions: (1) `expects:` lines on all 8 access_model variants — FORCED by the hard error, not optional; (2) restrict each variant's INVARIANTS list to its expected invariant(s) — free, since halts-at-first means the 9-name lists never verified the other 8. Rebase should be near-noop on overlap (access-model already carries the identical scan root, `weakened/` exclude, TLC gitignore entries). ⚠ **Open scope question for doyle: check W-SPEC's 8 for the same expected-green trap** — any variant flipping >1 guard has RenameFollow's shape, and measuring at land beats discovering it after golden assembly.

**⚠ UNSOUGHT: `TRACEABLE_REQS_TOKEN` DOES NOT EXIST on `spt-bs-core`** (`gh secret list` → only `RELEASES_TOKEN`), so the traceability job's private-repo clone dies `exit 128` / "Invalid username or token". **Main is green only by CACHE ACCIDENT** — the step clones solely on a cache miss, and kitsubito's cached binary is 0.1.2 == main's pin. Any cache eviction, runner rebuild, or pin bump turns main's traceability gate red with an opaque 128. chert's 0.1.4 bump (needed for `[scan].exclude` + `.tla` scanning) merely made it observable — env blocks on main and the branch are character-identical, rebase did NOT drop it. **Fix = operator provisions the PAT secret; not a code fix.**

**MILESTONES M0-M5:** M0 unblock #65 CI (java install + traceability-401-rerun + kitsubito test brain-startup-flake rerun) → M1 land #64→#65 (mint `REQ-SPEC-BRAIN-HANDOFF` inactive→activate-at-land + inactive `REQ-SPEC-REGISTRY-CONVERGENCE`) → **M2 = fidelity gate closes (tla green on main = a+b+c)** → **M3 = doyle promotion decision** (first-class traceable `model` stage? decide with pilot cost/yield in hand, NOT pre-decided; the cross-process epoch hole = evidence-in-favor) → M4 = `REQ-HAZARD-EPOCH-SINGLE-WRITER` impl/unit (funnel-assert test + CLI-minter guard fix, parallel-safe, OUTSIDE pilot gate) → M5 = wave-2 registry-CRDT-convergence spec (§5 sketch: N-node epoch-lease merge, status derivation under partition/heal; safety no-false-ONLINE/never-self-gossip-Offline/cold→Suspended/ghost-heal-terminates + liveness eventual-convergence; fidelity from recorded ghost/stale-ONLINE bugs; + wave-1 deferred A9/ring + CLI-minter third-writer; scope ruled by doyle AT wave-2 start).

**doyle hardening notes (non-blockers):** pin weakened-cfg bounds to what's proven to reach each violation (a weakened going green could be bounds-too-small masquerading as fidelity-lost); traceable-hygiene — confirm the `.tla` doc-tags on already-shipped REQs (REQ-UPDATE-PROMOTE-DRAINED etc.) ADD doc-evidence without disturbing their `required_stages`. Related: [[spt-core-findings-backlog]] (epoch cross-process seed material), [[presence-dead-shows-online]] (wave-2 false-ONLINE fidelity source).