[roodboi]

Restores the repository-local TLC checker and adds bun run check:tla for supervisor job lifecycle verification. The command checks the pinned TLC 1.7.4 checksum, runs actual-code models and passing reference controls, requires five named mutation failures, replays the schedules against the implementation, and reruns restored baselines.

The statechart and usage walkthrough were reviewed and committed before modeling. Coverage records the full source sync revision, atomic boundaries, bounds, fairness, and mutation evidence. Contributor and worker guidance point to tlaplus-workbench and the check command.

Property outcomes:

• P1 — bug / requested guarantee absent: two exported runner calls can execute the same stored job concurrently. Ordinary service creation uses a fresh ID.
• P2 — bug / stronger requested guarantee: cancellation can acknowledge while the child remains alive; a cancelled ID can also run again. The existing contract promises persisted cancellation, not process exit.
• P3 — bug / requested guarantee absent: retrying a completed stored ID executes again. There is no automatic job retry policy or job-wide attempt budget.
• P4 — bug under transient persistence failure: a claimed terminal write can fail permanently, leaving running metadata after exit. Progress passes with successful I/O and stated fairness.
• P5 — in sync: accepted cancellation preserves one terminal outcome/event within one invocation.

Additional deterministic replays confirm that a startup persistence failure can leave a live child after the service reports failure, without a cancellation handle.

Validation:

• mise exec -- bun run check:tla: all expected baseline outcomes, passing controls, five model mutations, real-code mutations, startup replays, and restored baselines matched. Wrapper success includes reproduced bugs.
• bun run typecheck, root TypeScript check, bun run check, and focused script/test lint passed.
• The full test command recorded 940 passes and 5 skips; sandbox capability restrictions affected 35 tests. All affected files passed in isolated reruns: 62 socket/process tests and 12 command tests. New supervisor tests and checker harness tests also passed.
• Agent-plugin generation produced no changes; documentation links and commit-range privacy/secret scans passed.

The model bounds one stored job and one or two invocations. Store calls are restricted to serialized schedules; hypothetical reference controls are sensitivity evidence, not shipped repairs. Shell transitions were source-reviewed as a separate lifecycle; no shell formal proof is claimed.

Release signal: verification only. Product code is unchanged. No strategy, vision, roadmap, planning artifacts, or unrelated preserved source were imported. No merge or deployment is part of this change.

---

^{Need help on this PR? Tag @codesmith-bot with what you need.}