[kixelated]

Problem

Two TLA+ legs of Nightly run 43250182795 failed without any rule regressing:

• TLA+ (route behind): error: no TLA+ config under: rs/moq-net/verify/route/BehindDear.cfg. test(net): model the picked route rule with a route per prefix #8541 deleted the config; the matrix still named it, and the route leg still excluded it.
• TLA+ (rest): EndedRelay.cfg broke NoSkipWhileHeld at depth 31 (exit 12). That is the open finding the verify-failover skill documents, but the config had no \* Open finding: line, so sh/tla.sh counted the expected break as a failure. Every other config in that leg passed or broke as marked.

Approach

• Drop the route behind leg and its exclusion from the route leg.
• sh/gh/nightly.test.py fails when a TLA+ leg or exclusion names a path that no longer exists. just gh test runs on every diff, so the next deleted config fails at the gate instead of overnight.
• Mark EndedRelay.cfg \* Open finding: NoSkipWhileHeld, as ci: model-check every TLA+ config nightly, and review resyncs a model #8483 did for the other open findings, so a fix that makes it pass is noticed.

Impact

None on public API or wire. Nightly runs one fewer TLA+ job.

Validation

• The new test fails against main's workflow (lists BehindDear.cfg twice) and passes on this branch.
• sh/tla.sh rs/moq-net/verify/failover/EndedRelay.cfg with a stub just exiting 12, the exit CI's TLC gave: exit 1 on main's config (error: ... exit 12), exit 0 with the marker. TLC was not rerun locally: the host's gate was saturated, and CI's run reproduces the skill's trace (depth 31, NoSkipWhileHeld).
• git ls-files on the route leg's pathspec lists Blind, Dead, Early, Lag, LagWide, Loop and Twice.

Caused by

• moq-dev/moq#8541 - deleted BehindDear.cfg without updating Nightly's TLA+ matrix.
• moq-dev/moq#8483 - introduced the \* Open finding: marker but missed EndedRelay.cfg, which test(net): model failover along a relay chain, and pin two fetch bugs it found #8482 had added earlier that day.

Alternatives

• Have sh/tla.sh skip a missing path instead of failing: a leg that silently checks nothing is worse.

Follow-ups

None.

Models

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

(Written by Claude Opus 5.5)

🤖 Generated with Claude Code

Review

Rewritten by quest review after each round.

• Head: 66e5149

• Base: origin/main at 9ea441e

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

• Session: 01a1d1b4-012f-72e1-b44d-13c78d488cf1, round 1

• Score: 9/10, The path check matches the current TLA+ matrix and the Open marker identifies a documented expected failure; source review found no actionable defects, with tests not run as instructed.

• Findings: none

[coderabbitai]

No actionable comments were generated in the recent review.

Walkthrough

The Nightly test checks that each configured TLA+ job path exists, including paths with a leading exclusion marker. The workflow comment documents this check. The failover configuration comments now identify NoSkipWhileHeld as an open finding and describe the ended-track relay scenario.

Merge Risk: Minimal · up to 66e51

This change drops a deleted TLA+ config from Nightly, adds a check that fails when a configured TLA+ path no longer exists, and marks the ended-relay finding as open. No actionable merge-blocking risk remains. The known limit that a marked config does not check which rule failed predates this PR and can be handled separately.

Pre-merge checks: 4

Check name	Status	Explanation
Title check		The title names the main change: Nightly's TLA+ legs drop a deleted config (BehindDear.cfg) and expect EndedRelay's open finding. The changeset removes the deleted config from the nightly matrix, adds…
Description check		The description explains the failing Nightly TLA+ legs, the removal of the deleted BehindDear.cfg leg, the new path check in sh/gh/nightly.test.py, and the Open finding marker added to EndedRelay.cfg.…
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: Nightly's TLA+ legs drop a deleted config (BehindDear.cfg) and expect EndedRelay's open finding. The changeset removes the deleted config from the nightly matrix, adds a path-existence test in sh/gh/nightly.test.py, and adds the Open finding marker to EndedRelay.cfg. The title is specific and matches these changes, though it is long at 82 characters.

Full details: Description check

Explanation

The description explains the failing Nightly TLA+ legs, the removal of the deleted BehindDear.cfg leg, the new path check in sh/gh/nightly.test.py, and the Open finding marker added to EndedRelay.cfg. It also gives validation steps and related PRs. It matches the changeset closely.

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: 2c26e513-8975-4dd2-95ad-b28ca90b3d1c

Commits

Reviewing files that changed from the base of the PR and between 9ea441e and 66e5149.

Files selected for processing: 3

• .github/workflows/nightly.yml
• rs/moq-net/verify/failover/EndedRelay.cfg
• sh/gh/nightly.test.py

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

[pullfrog]

✅ No new issues found.

Reviewed changes: the full 3-file diff, plus a check that the new test's regex matches the tla: job in nightly.yml.

• Nightly matrix: drops the route behind leg and the BehindDear.cfg exclusion from the route leg, matching #8541's deletion.
• EndedRelay.cfg: adds the \* Open finding: NoSkipWhileHeld marker, so sh/tla.sh expects the break.
• test_every_tla_leg_path_exists: fails when a TLA+ leg or exclusion names a path that no longer exists. The tla: job is followed by other jobs, so the ^ tla:\n(.*?)^ \S match works, and assertIsNotNone and assertTrue(paths) guard against the regex silently matching nothing.

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

[pullfrog]

✅ No new issues found.

Reviewed changes: the delta since the prior Pullfrog review, which is a merge of main into the branch.

• Merge of main: the matrix comment in nightly.yml was reworded by the merge, and sh/gh/nightly.test.py gained a self-hosted exemption in an unrelated test. The PR's own changes (dropping route behind, the EndedRelay.cfg open-finding marker, test_every_tla_leg_path_exists) are unchanged.

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