[kixelated]

Result: still no Rust TLA+ checker qualifies, so the tla recipes stay on TLC alone. This reruns moq-dev/moq#8600's comparison after moq-dev/moq#8628 replaced SumOver with the Community Modules' FoldSet. Every config a checker finishes still gives TLC's verdict and distinct-state count. On the route model, though, none costs fewer core-seconds than TLC, and two still cannot run it at all. #8628 also made TLC about 5x cheaper on route, so the bar a checker has to clear is now higher.

This finishes quest/m0/tla-native-recheck.md without adopting a checker, an outcome its Goal provides for, and deletes the quest file. Nothing else linked it.

Result

The three candidates are at the same revisions #8600 tested; none has pushed since. tlaplusplus (865cf7a) was left out: it is also unchanged, and what disqualified it (exit 1 instead of 12, Rust Debug traces) has nothing to do with SumOver.

checker	revision	route model after #8628
tlx	93dca5c9c29a	Agrees on Ring.cfg (426,409 states) at 14x TLC's CPU (2,630 against 183 core-s). On RouteHandoff.cfg it runs out of memory at the 16 GB cap after 2,186 core-s, at 290,842 of TLC's 407,240 states (TLC: 182 core-s). It has a native FoldSet, so the fold was not what made it slow.
tla-mc	c8fce23493bb	Rejects every route config: tla-mc: unknown operator choose. FoldSet expands to Folds.tla's MapThenFoldSet(op(_,_), base, f(_), choose(_), S), which applies its operator parameter choose. This is the same bug #8600 hit with SumOver's f, now inside a library module.
tla-rs	c9b885abb93a	Runs out of memory at the 16 GB address-space cap (11.5 GB RSS) within 12 to 25 s, on every route and resume config.

Each cell is distinct states (or verdict) / core-seconds (user+sys) / peak RSS in GB, at 4 workers:

config	TLC 1.8.0	tlx	tla-mc	tla-rs
route/RouteHandoff.cfg	407,240 / 182 / 4.5	out of memory (290,842 states, 2,186 s, 12.7)	rejects the spec	out of memory in 45 core-s
route/Ring.cfg	426,409 / 183 / 4.4	426,409 / 2,630 / 9.0	rejects the spec	out of memory in 52 core-s
route/Lag.cfg	1,299,405 / 681 / 4.5	not run	rejects the spec	out of memory in 47 core-s
route/Loop.cfg	breaks RequestsLoopFree / 432 / 4.5	not run	rejects the spec	out of memory in 42 core-s
route/Early.cfg	4,178,590 / 2,085 / 4.5	not run	rejects the spec	out of memory in 50 core-s
route/LagWide.cfg	4,194,747 / 2,288 / 4.5	not run	rejects the spec	out of memory in 71 core-s
resume/ThreeRoutes.cfg	7,053,230 / 340 / 3.0	7,053,230 / 88 / 0.8	7,053,230 / 162 / 1.2	out of memory in 74 core-s
resume/ResumeReader.cfg	14,334,670 / 984 / 4.5	14,334,670 / 220 / 1.3	14,334,670 / 417 / 2.2	out of memory in 94 core-s

TLC's distinct-state counts are the same as #8600's on every config, so #8628 changed the cost and not the state space. Its CPU fell from 912, 1,027, 3,004, 1,874, 7,584, and 12,313 core-s on the route configs to the numbers above. Part of the drop is the move from 8 workers to 4, but most of it is FoldSet.

Why the sweep stops here

The Goal asks for fewer core-seconds than TLC on both the route and resume models. The route model is now 5,850 of the 7,175 core-s these eight configs cost TLC, and no candidate qualifies on it:

• tla-mc and tla-rs cannot finish any route config.
• tlx took 14x TLC's CPU on Ring.cfg, the one route config it finished. In the first 9 minutes of RouteHandoff.cfg it found about 30,000 distinct states per minute on 4 workers, against TLC's roughly 625,000 per minute. A full Early.cfg or LagWide.cfg run would take tlx about 7 CPU-hours at its Ring.cfg rate (162 states per core-second, against TLC's 1,800 to 2,300), and probably more than 16 GB.

Adoption needs agreement on every exhaustive config, and on route there is no candidate left to check against TLC. The failover, reconnect, subscribe, and JS configs, which #8600 found every finishing checker agreed on, were therefore not rerun.

On resume, tlx (3.9x to 4.5x cheaper) and tla-mc (2.1x to 2.4x cheaper) would still qualify, as they did in #8600. Adopting either for everything except route would leave 80% of TLC's cost on TLC and add a second engine to Nightly, so neither is adopted.

Upstream bugs, for the maintainer to report

None were filed. The quest asks for them to be reported to the maintainer instead.

• tla-mc: unknown operator choose. An operator parameter applied inside an operator's body (LET x == choose(s) in the Community Modules' Folds.tla, line 25) is not resolved. The same bug blocked chore(quest): no Rust TLA+ checker agrees with TLC on the route model #8600 (Sum(f(_)) == SumOver(ns, f)). It also prints counterexamples without each step's action, as chore(quest): no Rust TLA+ checker agrees with TLC on the route model #8600 found.
• tla-rs: exceeds a 16 GB address-space cap within 12 to 25 s on every route and resume config, where TLC needs 3 to 4.5 GB.
• tlx: on RouteHandoff.tla it holds about 44 KB per distinct state and checks states about 20x slower than TLC.

Choices made without asking

• tlaplusplus not rerun. Its revision is unchanged, and it failed chore(quest): no Rust TLA+ checker agrees with TLC on the route model #8600 on its exit code and trace format, which this rerun cannot change.
• 4 workers for every engine. That is what sh/tlc.py uses since perf(verify): TLC runs cost fewer core-seconds and share the host #8628 (chore(quest): no Rust TLA+ checker agrees with TLC on the route model #8600 used 8). TLC used the recipe's own flags and heap: -Xmx4g, the pinned Community Modules jar, and -checkpoint 0 -cleanup -noGenerateSpecTE.
• tla-mc and tla-rs read the Community Modules' .tla sources from the same release as TLC's jar (202311011627, CommunityModules 00d3635), through -lib and -library. tlx uses its bundled modules. tla-mc and tla-rs have no native FoldSet, so they evaluate its TLA+ definition.
• tlx not run on the remaining four route configs. At its measured rate each would take several CPU-hours, and the outcome could not change.
• No follow-up quest. All three candidates are tied to upstream fixes the maintainer may or may not report. A periodic recheck would cost several CPU-hours per round and has no trigger, so I dropped it. A future quest can rebuild the harness from the flake below.

Validation

• Each checker was built with crane from its pinned revision inside the Nix sandbox, on the nixpkgs, crane, and rust-overlay revisions in this repository's flake.lock. tlx used its pinned 1.93.0 toolchain; the others used latest stable. Each check, including TLC's, ran as its own sandboxed runCommand derivation over a copy of the spec's directory, under GNU time -v → prlimit --as=16G → timeout 7200 → the engine. Runs went one at a time through quest gate. Nothing of the candidates' ran outside the sandbox.
• Smoke test before the sweep: on Publish.cfg and FailoverRedirect.cfg all four engines gave the same distinct-state counts and verdicts. FailoverRedirect.cfg now passes on main; its open finding is gone, unlike in chore(quest): no Rust TLA+ checker agrees with TLC on the route model #8600.
• TLC's Loop.cfg trace names each step's action (State 2: <Deliver line 523, ... of module RouteHandoff>), as the verify skills' replay steps need.
• A host restart (the T3 server) killed the first sweep after the RouteHandoff and Ring runs. The rest ran from a systemd-run --user unit. No run was repeated or merged across the two sweeps.
• The harness is scratch and is not committed:

flake.nix and run.sh

{
  # Scratch harness for quest/m0/tla-native-recheck.md: builds each checker
  # from a pinned revision and runs one check per sandboxed derivation.
  inputs = {
    nixpkgs.url = "github:NixOS/nixpkgs/d357a2b54f0b6dc4aeb4e993190a52cf151b6f24";
    crane.url = "github:ipetkov/crane/e675a36b7377bebe41d548388a2501cbb16d380d";
    rust-overlay = {
      url = "github:oxalica/rust-overlay/c85ccd343087c57da6021cafa1647142ad03e32e";
      inputs.nixpkgs.follows = "nixpkgs";
    };
    tlx = {
      url = "github:Medfin-AI/tlx/93dca5c9c29a708a92a6a82efa1ab85e8e6d32fb";
      flake = false;
    };
    tla-mc = {
      url = "github:ddalton/tla-mc/c8fce23493bb78fcd5405faf7b0653855db620ee";
      flake = false;
    };
    tla-rs = {
      url = "github:bbcvc/tla-rs/c9b885abb93aa5e84d0e7134d79b9b8f12a62fd7";
      flake = false;
    };
    # The Community Modules release sh/tlc.py puts on TLC's classpath.
    community = {
      url = "github:tlaplus/CommunityModules/00d3635549456a3f3dd47455faf03d484472d7f7";
      flake = false;
    };
  };

  outputs =
    {
      nixpkgs,
      crane,
      rust-overlay,
      tlx,
      tla-mc,
      tla-rs,
      community,
      ...
    }:
    let
      system = "x86_64-linux";
      pkgs = import nixpkgs {
        inherit system;
        overlays = [ (import rust-overlay) ];
      };
      build =
        {
          src,
          toolchain,
          pname,
          extra ? { },
        }:
        let
          lib = (crane.mkLib pkgs).overrideToolchain toolchain;
          args = {
            inherit src pname;
            version = "0";
            strictDeps = true;
            doCheck = false;
          }
          // extra;
        in
        lib.buildPackage (args // { cargoArtifacts = lib.buildDepsOnly args; });
      stable = pkgs.rust-bin.stable.latest.minimal;
      checkers = {
        tlx = build {
          src = tlx;
          pname = "tlx";
          toolchain = pkgs.rust-bin.stable."1.93.0".minimal;
          extra.cargoExtraArgs = "--locked -p tlx-cli";
        };
        tla-mc = build {
          src = tla-mc;
          pname = "tla-mc";
          toolchain = stable;
        };
        tla-rs = build {
          src = tla-rs;
          pname = "tla-rs";
          toolchain = stable;
          extra.cargoExtraArgs = "--locked -p tla-tools";
        };
      };
      jar = pkgs.fetchurl {
        url = "https://github.com/tlaplus/CommunityModules/releases/download/202311011627/CommunityModules-deps-202311011627.jar";
        hash = "sha256-Ca3VmiMGYV/SODGw+cI8ENQOvPZj/5TdLZOtwSz5o9s=";
      };
      lib = "${community}/modules";
      workers = "4";
      commands = {
        tlc = "${pkgs.jre}/bin/java -Xmx4g -XX:+UseParallelGC -cp ${pkgs.tlaplus18}/share/java/tla2tools.jar:${jar} tlc2.TLC -workers ${workers} -checkpoint 0 -cleanup -noGenerateSpecTE -metadir $TMPDIR/meta";
        tlx = "${checkers.tlx}/bin/tlx check";
        tla-mc = "${checkers.tla-mc}/bin/tla-mc -workers ${workers} -lib ${lib}";
        tla-rs = "${checkers.tla-rs}/bin/tla-rs -workers ${workers} -library ${lib} -noGenerateSpecTE";
      };
      # tlx takes its options after the spec.
      invoke =
        engine: spec: cfg:
        if engine == "tlx" then
          "${commands.tlx} ${spec} -config ${cfg} -workers ${workers}"
        else
          "${commands.${engine}} -config ${cfg} ${spec}";
    in
    {
      packages.${system} = checkers;
      # One check: `dir` is the spec's directory, copied into the store.
      check =
        {
          engine,
          dir,
          spec,
          cfg,
          limit ? 7200,
          nonce ? "",
        }:
        pkgs.runCommand "check-${engine}-${cfg}"
          {
            nativeBuildInputs = [
              pkgs.time
              pkgs.util-linux
              pkgs.coreutils
            ];
            src = dir;
            inherit nonce;
          }
          ''
            mkdir -p $out work
            cp -r $src/. work/
            chmod -R u+w work
            cd work
            status=0
            command time -v -o $out/time prlimit --as=17179869184 -- timeout ${toString limit} ${invoke engine spec cfg} > $out/log 2>&1 || status=$?
            echo $status > $out/status
          '';
    };
}

#!/usr/bin/env bash
# Run one check in the Nix sandbox: run.sh <engine> <cfg path from repo root> [limit seconds]
set -euo pipefail
bench=$(cd "$(dirname "$0")" && pwd)
root=$(cd "$bench/../.." && pwd)
engine=$1 cfg=$2 limit=${3:-7200}
dir=$root/$(dirname "$cfg")
name=$(basename "$cfg")
specs=()
for s in "$dir"/*.tla; do [[ "$s" == *_TTrace_* ]] || specs+=("$(basename "$s")"); done
if [ ${#specs[@]} -gt 1 ]; then
    all=("${specs[@]}"); specs=()
    for s in "${all[@]}"; do [[ "$name" != "${s%.tla}"* ]] || specs+=("$s"); done
fi
[ ${#specs[@]} -eq 1 ] || { echo "no single spec for $cfg" >&2; exit 1; }
out=$bench/results/$engine/${cfg%.cfg}
rm -rf "$out"; mkdir -p "$(dirname "$out")"
store=$(quest gate nix build --impure --no-link --print-out-paths --expr "
  (builtins.getFlake \"path:$bench\").check {
    engine = \"$engine\";
    dir = builtins.path { path = $dir; name = \"spec\"; };
    spec = \"${specs[0]}\";
    cfg = \"$name\";
    limit = $limit;
    nonce = \"$(date +%s%N)\";
  }")
cp -rL "$store" "$out"; chmod -R u+w "$out"
echo "$engine $cfg: exit $(cat "$out/status"), $(grep -E 'User time|System time|Maximum resident|Elapsed' "$out/time" | awk -F': ' '{printf "%s ", $2}')"

Impact

Public API: none. Wire: none. Quest tree only.

Caused by

None: this measures checkers and fixes no bug.

Follow-ups

None.

Models

Size: M
Implementer: Claude Code, claude-opus-5-5, unknown effort

(Written by Claude Opus 5.5)

Review

Rewritten by quest review after each round.

• Head: 94a797d

• Base: origin/main at 6034f66

• Reviewer: Codex, gpt-6.1-sol, high effort

• Session: 01a1d71e-3b76-7de0-8ccf-6efb223c62ad, round 1

• Score: 10/10, The diff only deletes a quest plan, with no runtime, API, wire, or test changes and no remaining references to the deleted file.

• Rounds: 1; findings 0: fixed 0, refuted 0, open 0

• Findings: none

[coderabbitai]

No actionable comments were generated in the recent review.

Walkthrough

The pull request deletes the document describing a proposed comparison of native TLA+ checkers with TLC. The document also recorded comparison requirements, resource limits, and the m0 decision.

Merge Risk: Minimal · up to 94a79

This change removes a planning document for the native TLA+ checker comparison. It has no runtime or user-facing impact, and the TLA+ recipes remain TLC-only. It is safe to merge.

Pre-merge checks: 4

Check name	Status	Explanation
Title check		The title names the main change, a rerun finding that no Rust TLA+ checker beats TLC on the route model after FoldSet. The diff deletes quest/m0/tla-native-recheck.md, which records that rerun and its…
Description check		The description matches the changeset. It explains the rerun of the TLA+ checker comparison, the results per checker and config, the decision to keep the tla recipes on TLC, and the deletion of the qu…
Linked Issues check		Check skipped because no linked issues were found for this pull request.
Out of Scope Changes check		Check skipped because no linked issues were found for this pull request.

Full details: Title check

Explanation

The title names the main change, a rerun finding that no Rust TLA+ checker beats TLC on the route model after FoldSet. The diff deletes quest/m0/tla-native-recheck.md, which records that rerun and its rejection outcome. The title is specific and matches the changeset, though it describes the finding more than the file deletion.

Full details: Description check

Explanation

The description matches the changeset. It explains the rerun of the TLA+ checker comparison, the results per checker and config, the decision to keep the tla recipes on TLC, and the deletion of the quest file. It also covers validation and the scope of impact.

Finishing Touches

Simplify code

• Commit to this branch
• Create a new PR

• Autofix · Keep fixing CodeRabbit findings and required CI, and resolving merge conflicts

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

Share

• X
• Mastodon
• Reddit
• LinkedIn

Recent review info

Run configuration

• Source mode: Auto
• Repository: Unavailable
• Branch: Unavailable
• File: No configuration file from this repository applied
• Commit: Unavailable
• Layers: Organization UI
• Review profile: CHILL
• Plan: Advanced
• Run ID: fd67e24c-cef2-48fc-a1c7-eda906dc2ca1

Commits

Reviewing files that changed from the base of the PR and between d6195e8 and 94a797d.

Files selected for processing: 1

• quest/m0/tla-native-recheck.md

Files with no reviewable changes: 1

• quest/m0/tla-native-recheck.md

Included review availability: This review used your included allowance. Your plan provides up to 4 included reviews per hour; 0 remain after this review.

[pullfrog]

✅ No new issues found.

Reviewed changes: the single-file diff, checked against the rest of the checkout for dangling references.

• Quest file deleted: quest/m0/tla-native-recheck.md is removed. The quest's outcome (no Rust TLA+ checker beats TLC) is recorded in the PR description. A repo-wide grep finds no other references to the file.

  ^{｜ View workflow run ｜ Using claude-sonnet-5-5 ｜ 𝕏}