[kixelated]

Summary

Three TLC runs from one session's ad-hoc scripts took 10 to 13 of a 24-core desktop's cores for over an hour and held every other session's quest gate shut. This PR makes a TLC run cheaper and polite, and plans two ways to check faster.

• The tla recipes (rs/justfile, js/justfile) run TLC 1.8.0 on Java 21 (nixpkgs#tlaplus18) instead of TLC 1.7.4 on Java 8 (nixpkgs#tlaplus).
• TLC runs at nice -n 19 with a 4 GB heap. The JVM default is a quarter of RAM per run, which was 14 GB each here.
• -noGenerateSpecTE: TLC 1.8.0 otherwise writes a *_TTrace_*.tla and .bin beside the spec on every broken rule.
• The four verify-* skills run their commands through quest gate. The rs recipe's comment says how to pass a spec outside rs/, so a generated config needs no runner of its own.
• New quest quest/m1/tla-native-checker.md [M]: spike the Rust TLA+ checkers.
• New quest quest/m1/route-exhaustive-sim.md [M]: spike an exhaustive search over route::tests::Sim on the real Router.

Measurements

RouteHandoff.cfg, 24 workers, on the 24-core desktop while other sessions were building (load average 25 to 43). Every run generated 17,671,735 states and found 3,674,389 distinct.

Setup	Wall	CPU-seconds
TLC 1.7.4, Java 8, 4 GB heap	114 s, 122 s	1,675, 1,791
TLC 1.8.0, Java 21, 4 GB heap	51 s	937
TLC 1.8.0, Java 21, 2 GB heap	51 s	938
TLC 1.8.0, Java 21, default 14 GB heap	49 s	909
TLC 1.8.0, Java 21, OffHeapDiskFPSet	51 s	977
TLC 1.8.0, Java 21, OffHeapDiskFPSet and BAQueue	57 s	1,060

Worker sweep on TLC 1.8.0 with a 4 GB heap, on a quieter host:

Workers	Wall	CPU-seconds
24	65 s	980
12	73 s	900
8	93 s	815
4	165 s	765
2	367 s	837

Decisions

Maintainer, /quest-plan, 2026-11-10:

• ✅ The goal is model checks that cost fewer core-seconds and never starve the host (rejected: polite only; moving off TLA+).
• ✅ Tune TLC now, in this PR, rather than as a quest.
• ✅ Spike both a Rust TLA+ checker and an exhaustive search over Sim, in m1.
• ✅ A Rust checker that agrees with TLC runs locally and Nightly cross-checks it (rejected: local only; replacing TLC; report only).
• ✅ The Sim search is hand-written (rejected: stateright; building both).

Choices made without asking

• -workers auto stays. CPU-seconds were near flat from 2 to 24 workers, so a cap would slow a run without saving work.
• No off-heap fingerprint set or BAQueue: neither helped.
• The js/*/verify/ READMEs keep their plain commands; they are for people, and #8483 rewrites those lines.
• The skills' timings ("two minutes on 32 cores") are left as they are: they were not remeasured on that machine, and ci: model-check every TLA+ config nightly, and review resyncs a model #8483 edits the same lines.

Checks

• quest check: pass.
• just rs tla moq-net/verify/route/RouteHandoff.tla -config rs/moq-net/verify/route/CountToInfinity.cfg and just js tla room/verify/Room.tla: both break their open finding's rule (exit 12) as before, on Java 21 with a 3.6 GB heap, and leave no file behind.
• just check: not finished. A justfile change selects the whole Rust and JS suites; the run was cancelled after 25 minutes with check rs still waiting.
• Only RouteHandoff.cfg was compared state for state between the two TLC versions.

Public API: none. Wire: none.

Follow-ups

None beyond the two quests.

Models

Size: S
Implementer: Claude Code, claude-fable-5-2, high effort

(Written by Claude Fable 5 with high)

🤖 Generated with Claude Code