tla: model-check verifier-challenge gaps (#429 fail-open, #431 scan coverage) - #454

Process completed with exit code 1.

2 TLA+ check(s) failed (2 live bug(s) block merge). See the result table in the job summary.

OPEN BUG (blocks merge): Issue #431 residual: MAX_PREKICKOFF_SUCCESSORS_PER_SCAN=32 depth cap leaves deeper decoy chains uncovered. Repro: cd node/tla && java -jar ~/.local/share/tlaplus/tla2tools.jar -config KickoffScanCoverageResidual.cfg KickoffScanCoverage.tla

OPEN BUG (blocks merge): Issue #429: verifier KickoffSent fail-open (SPV lag skips Challenge, never retried). Repro: cd node/tla && java -jar ~/.local/share/tlaplus/tla2tools.jar -config VerifierKickoffFailOpen.cfg VerifierKickoffFailOpen.tla

Node.js 20 is deprecated. The following actions target Node.js 20 but are being forced to run on Node.js 24: actions/setup-java@v4. For more information see: https://github.blog/changelog/2025-09-19-deprecation-of-node-20-on-github-actions-runners/