Reduce dependency on TLA runs for CI

[cjen1-msft]

It appears that there are either shallow or deep bugs in the TLA.
If the bug is shallow Simulation fails on it quickly.
If the bug is deep it is extremely expensive to wait for either Model Checking or Simulation to prove its absence.

Hence I think we should block CI only on the shallow bugs.
And rely on periodic costly deep checking for the proof of absence.

The shallow runs are cheaper and so should be fine to run on small github runners which also seem to be slightly more reliable and quick to spin-up.
They both only trigger on PRs which make changes to raft.h or the TLA directory.

[Copilot]

Pull request overview

This PR separates lightweight PR-gated TLA verification from expensive weekly verification.

Changes:

• Adds shallow simulation and trace-validation checks.
• Moves long and continuous verification to weekly schedules.
• Runs shallow checks on hosted runners.

Reviewed changes

Copilot reviewed 3 out of 3 changed files in this pull request and generated 4 comments.

File	Summary	Review notes
.github/workflows/tla-shallow.yml	Adds PR-gated shallow verification jobs.	Include the workflow itself in path filters and document the workflow and trigger behavior in README.md.
.github/workflows/long-verification.yml	Restricts deep verification to weekly schedules.	Update documentation describing PR, manual, and label-based triggers.
.github/workflows/ci-verification.yml	Restricts continuous verification to weekly schedules.	Update documentation so it no longer promises PR or manual checks.

Suppressed comments (3)

.github/workflows/tla-shallow.yml:99

• tests.sh forwards these arguments directly to ctest, whose --timeout option requires a numeric value. With --no-compress-output as the next token, this command exits during option parsing, so the raft scenarios never run and no traces are produced; pass an explicit timeout such as --timeout 360.

          ./tests.sh -VV --timeout --no-compress-output -T Test -L raft_scenario

.github/workflows/tla-shallow.yml:107

• Because traces/consensus already exists, mv ../build/consensus traces/ targets the existing traces/consensus directory and fails rather than placing the generated files there. Create only the parent traces directory before moving build/consensus, so the resulting path is the one consumed by the next command.

          mkdir -p traces/consensus
          mv ../build/consensus traces/

.github/workflows/tla-shallow.yml:39

• The job is capped at 10 minutes, but this simulation omits --max-seconds, so tlc.py uses its 1200-second default. A run lasting 10-20 minutes will be killed by the job before TLC reaches its configured timeout; set a limit compatible with the job (or increase the job timeout) so failures are reported and traces can be uploaded predictably.

          ./tlc.py --trace-name consistency-simulation sim --num 500 --depth 50 consistency/MultiNodeReads.tla || status=$?

---

💡 Configure MCP servers for context-aware, tailored reviews. Learn more in the docs.