[kixelated]

Checkpoint for quest/m1/route-inductive.md: the inductive invariant stalls because Apalache cannot check even one step of the route model. This PR records why and hands back the decision on how to continue.

Summary

• rs/moq-net/verify/route/RouteHandoff.tla carries Apalache type annotations, and its RECURSIVE operators and recursive functions are now Apalache folds (ApaFoldSet, ApaFoldSeqLeft), so one file serves both tools. IsPath checks a path's shape directly instead of enumerating every loop-free path. Each takes a function that returns one message, and the request walk and Chased are now folds of one step each.
• nix/apalache.nix packages Apalache 0.63.0 (nixpkgs has none) on JDK 21 under legacyPackages, outside the dev shell. share/tla holds its Apalache.tla.
• just rs tla now runs TLC from the spec's directory with -DTLA-Library pointing at that library, because TLC reads the property only for a spec named without a directory. The new just rs apalache <command> <spec> runs Apalache with its output in a temporary directory.
• The quest records the measurements and the open decision.

Apalache 0.63 could not finish one step with SimplePaths as the only invariant, given 16 GB of heap:

Check	Mesh	Result
One step from Init, all 7 transitions	publisher and 3 relays	out of heap after 26 minutes
One Deliver on one session, from any typed state	publisher and 3 relays	out of heap after 6 minutes
The same, --smt-encoding=arrays	publisher and 3 relays	still in its optimizer pass after 85 minutes
The same	publisher and 2 relays, the smallest mesh with a loop	past 19 GB in 8 minutes, killed

Every step runs Update, which rebuilds a node's whole state, so the solver encodes every route path, view, sent record, and reader event for every step. That state does not fit, even before an invariant is added.

Waiting

• moq-dev/moq: paused 2026-11-12 by the maintainer, who doesn't want more JVM model checking (Apalache or TLC) here. The last agent was OOM-killed on fedora while running one. Resume once moq-dev/moq#8600 reports whether a Rust TLA+ checker agrees with TLC; check by reading that PR's results. The maintainer picked A (split the model) earlier on 2026-11-12. Its first four commits, plus a merge of main, are pushed as 86bdb5719, and the claims model's checks have not finished.

Choices made without asking

• Apalache 0.63.0, the newest release, packaged from its release tarball (checksum checked against the release's sha256sum.txt).
• TLC gets the folds from Apalache's own Apalache.tla through TLA-Library. I chose that over vendoring a copy beside the spec, which sh/tla.sh would take for a second spec.
• The probes' generator modules (typed symbolic states built with Gen) stay out of the tree; the quest describes them. A second .tla in the route directory breaks sh/tla.sh, and they have no consumer until the decision above.

Checks

• just rs apalache typecheck moq-net/verify/route/RouteHandoff.tla: passes.
• just test tla rs/moq-net/verify/route: every config gives its expected result, and Loop.cfg still breaks RequestsLoopFree. The exhaustive configs find exactly the distinct states the skill lists: RouteHandoff 407,240; Early 4,178,590; Ring 426,409; Lag 1,299,405; LagWide 4,194,747.
• just check and quest check: pass.
• Other rs/ specs: not rerun. They take the new tla recipe but extend no Apalache module.

Observed, not fixed here

• Nightly's TLA+ (route behind) leg names rs/moq-net/verify/route/BehindDear.cfg, which moq-dev/moq#8541 deleted, so the leg fails. A separate PR fixes it.
• Nightly's TLA+ (rest) leg fails on rs/moq-net/verify/failover/EndedRelay.cfg (TLC exit 12, a broken rule) in today's run. No open PR addresses it.

Public API: none. Wire: none.

Follow-ups

None yet; the decision above may add the loop-rules quest.

Models

Size: L
Implementer: Claude Code, Opus 5.5, high effort

🤖 Generated with Claude Code

(Written by Claude Opus 5.5 with high)

[kixelated]

Closing, as the maintainer decided on 2026-11-13: #8600 and #8669 found no Rust TLA+ checker that qualifies, and the maintainer doesn't want more JVM model checking here, so TLC stays the only checker. The route-inductive quest is dropped in a separate quest-only PR.

(Written by Claude Opus 5.5)