[andrewpark-scaleai]

What and why

The task-instance store promises that a write from a rolled-back or superseded attempt never lands, and that replaying the live journal reproduces the stored context. The unit tests check a few hand-picked orders of those writes. This adds a TLA+ model of the store calls and the scheduler that makes them. TLC checks every order within a small bound: one retry, a cancelled step whose write lands late, and a second process that re-registers the run.

• tst/formal/step_journal/StepJournal.tla names the code that each action stands for. check.sh fetches TLC 1.7.4, checks its sha256, and runs the baseline or the mutation suite.
• The AGENTS.md beside the model says which code it covers, how to read a counterexample, and how to update the model.
• The root AGENTS.md lists tst/formal/ as a by-hand tier.

The model describes the code with the seed_context fence from #490. Without that fence, takeover.cfg fails.

No CI job runs the check. It needs Java and one download from GitHub, and the baseline takes about 30 seconds, so CI wiring is left for a separate decision. The guide lists what the model does not cover, such as context contents, store failures and other task shapes.

How it was tested

• tst/formal/step_journal/check.sh: single and takeover hold, at 4,697 and 3,104,845 distinct states.
• check.sh mutations: each of the 9 mutations that removes a guard breaks the invariants it names. NoCasGenerationCheck holds as expected, because every re-register also increments attempt_epoch.
• With the cfg substitution broken, or with no java on PATH, check.sh exits 2 with a message that names the problem.

Confidence Score: 5/5

The PR appears safe to merge; no actionable new issues remain.

Summary

Adds a manually run TLA+ model of the step journal’s epoch fences and replay behavior.

• The step journal now has a hand-run model check for retries and run takeovers.

Review used the full PR diff because the ancestry and merge-base checks did not pass. TLC was not run during this review.

Diagram

%%{init: {'theme': 'neutral'}}%%
flowchart TD
  A[Register run and capture epoch] --> B[Write seed and journal row]
  B --> C[Run steps]
  C --> D[Write journal row]
  D --> E{Epoch and generation still match?}
  E -->|Yes| F[Save completion]
  E -->|No| G[Reject completion and remove its row]
  C --> H[Retry]
  H --> I[Undo steps and advance epoch]
  I --> C
  J[Second process registers run] --> K[Advance epoch and generation]

Loading

_{Reviews (3) · Last reviewed commit: "fix(formal): fail check.sh one on a TLC ..." · Reviewed by Greptile}