🤖 tests: cover #5465 background-process cases in the TLA+ model

[ThomasK33]

Summary

This extends the background-process TLA+ model (formal/background-processes/) so that check.sh reports the three cases from #5465. It also adds a deterministic repro for the one that is a real defect. No product code changes.

Fixes #5465

Case	Model change	Config(s) and EXPECT	Outcome
1. Refused or failed migration, join > 5 s	BgCleanup: MRefused now unregisters the foreground entry and aborts; new MMigrateFail (an admitted migration whose record cannot be created takes the same path); new MJoin / MJoinTimeout (constant JoinTimeout)	MC_cleanup_refused_join_timeout, and MC_cleanup_failed_join_timeout (constant MigrationFails forces the admitted-then-failed path): NoLiveAfterDelete MigrationOwned violated	Defect. Repro added; fix tracked in #5522
2. Exec timeout after a migration	BgCleanup: FTimeout (constant ExecTimeout)	MC_cleanup_migration_timeout: all hold	Benign (reason below)
3. Crash between spawn and writeMeta	BgGateEvidence: spawn split into ADir → AChild → AMeta, plus ACrash (constant Crash), an exit marker, and the scan's meta-less rule	MC_gate_crash_before_meta, MC_gate_crash_devcontainer: hold. Mutant MC_mut_gate_metaless_trusted: violated	Safe on scanned roots (reason below). Liveness gap tracked in #5576

Case 1: defect (#5522)

When a migration is refused (the workspace is sealed) or fails, tools/bash.ts:

• unregisters the foreground entry (~:1479);
• aborts the command (~:1569);
• joins its exit for at most FAILED_MIGRATION_EXIT_JOIN_MS = 5 s (~:1578).

If the join does not see the exit, nothing tracks the command any more: there is no manager entry and no record. The removal that waited on the migration then deletes its checkout. TLC's shortest trace for NoLiveAfterDelete:

1. The removal seals the workspace.
2. The migration is refused.
3. MJoinTimeout fires while the command is still alive.
4. MEnd runs, then cleanup drains, then RDelete deletes the checkout.

One backend is enough to reach this. It needs a kill that takes effect late: a command stuck in uninterruptible I/O, or a remote exec whose close arrives late.

The repros are in backgroundProcessesFormalRepro.test.ts: "a refused migration does not leave its command running untracked" (the seal refuses the migration) and "a failed migration does not leave its command running untracked" (the migration is admitted, and migrateToBackground fails with ENOSPC). Each checks which path its tool error came from. Both use a LocalRuntime subclass that delivers the abort only after the test releases it. After the tool returns "terminated because it could not be tracked", the command's PID is still alive. Each repro then starts the cleanup a removal runs (cleanup(ws, { failClosedAfterDrainTimeout: true })). The target assertion is that this cleanup has not finished 500 ms later (still waiting, or failed closed), because a removal deletes the checkout once it returns. Today it fails: the cleanup has already finished (expect(early === "finished").toBe(false) gets Expected: false, Received: true). The target maps to the model's NoLiveAfterDelete, so the #5522 fix turns these repros into plain tests without changing what it checks.

The control test, with an effective kill, passes. Both repros fail at the same target before the fix. The fix belongs in a separate PR (#5522), as the brief requires.

Case 2: benign

The foreground exec's timer (LocalBaseRuntime ~:369-377, RemoteRuntime ~:266) keeps running after a migration and can kill the command. This is safe:

• timeout_secs is the documented maximum lifetime of a background command ("For background: max lifetime before auto-termination", toolDefinitions.ts). The migrated command keeps its original call's bound.
• The kill ends the same exec stream whose exitCode the migrated handle observes and writes as exit_code (backgroundProcessExecutor.ts ~:739-743). The exit is therefore recorded, not lost.

In the model, FTimeout is FExit restricted to the migrated phases, so the state count equals MC_cleanup_migration_remove's (106). The config pins the case. Whether a migration should lift the foreground timeout is a UX question, not a safety one.

Case 3: safe on scanned roots, with a liveness gap

spawnProcess creates the record directory with output.log and clears exit_code (backgroundProcessExecutor.ts :242-268) before it starts the child (:294). writeMeta comes later (backgroundProcessManager.ts ~:1867). After a crash in between:

• A's turn lease goes stale.
• recordRootHoldsOrphan treats a directory that has neither meta.json nor exit_code as a live orphan and fails closed (~:2877-2890). This is already tested in backgroundProcessManager.test.ts ("fails closed on unreadable records without an exit marker").
• The wrapper's trap writes the marker when the process exits.

I re-checked this against current main (eea905d): backgroundProcessManager.ts, backgroundProcessExecutor.ts and their tests are unchanged since 486f156, so the cited lines are what ships today. (Open PR #5521 would make the process group decide instead of the exit marker. It is paused, and it can rebase onto this model.)

A crash before the child starts leaves a markerless directory that no process will ever settle. The structural mutation gate runs the orphan scan for user removal too, so that workspace's removal is refused until someone deletes the directory. That is safe but a liveness gap, which these safety-only configs do not check. It existed before this PR and is tracked in #5576. Remote roots are still unscanned, as in the existing MC_gate_ssh_spawn and MC_gate_docker_spawn configs (#4889). The mutant that skips meta-less directories is caught, so the model can see this class of bug.

Model faithfulness for existing configs

• Every existing config gets the new constants set to FALSE.
• Every existing EXPECT verdict is unchanged. check.sh exits 0, and FORMAL_FAST=1 also passes.
• In the gate model, the record evidence with a meta.json is ~marker /\ alive, which matches the old record /\ alive. A's lease still covers the spawn until AEnd, so the step split changes no verdict when Crash = FALSE.

Validation

• formal/background-processes/check.sh (full run) exits 0, and every new config matches its EXPECT entry.
• The whole of src/node/services/backgroundProcessesFormalRepro.test.ts passed 3 times in a row (14 tests each) on Bun 1.3.12.
• make static-check passes.
• Overlap: open PR 🤖 fix: only a supervisor inside the group signals a background process group #5521 also edits formal/background-processes/ and this repro file. It is paused, so this PR goes first and 🤖 fix: only a supervisor inside the group signals a background process group #5521 rebases onto it.

---

Generated with xum • Model: anthropic:claude-opus-5-5 • Thinking: high • Cost: $32.91

[chatgpt-codex-connector]

Codex Review Summary

This comment shows the latest Codex review activity on this pull request.

Review	Status	Commit	Review trigger
📝 Code Review	✅ Completed 2026-10-03T20:11:34.534066Z	6aabf6b	New commits
🔒 Security Review	✅ Completed 2026-10-03T20:10:45.515400Z	6aabf6b	New commits

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review" or "@codex security review".

Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings.

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: f475f5e634

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: ca6c233b29

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

[ThomasK33]

Readiness record for head 6aabf6b:

• CI: all checks pass on this head (29 pass, 4 skipped), including the Formal background-processes job. Unresolved review threads: 0.
• Local: formal/background-processes/check.sh full and FORMAL_FAST=1 exit 0. backgroundProcessesFormalRepro.test.ts 15 pass on Bun 1.3.12. make static-check passes.
• Review budget: 3 normal and 3 security automatic reviews (6 assessments). Findings per round: 3, 2, 0 (strictly shrinking), and the security reviews found nothing. The final independent check is the 7th assessment, under the coordinator's +2 extension (overrun from automatic runs, findings strictly shrinking).
• Dispositions: the FTimeout-equals-FExit finding was rejected with a reason. The failed-migration path, its forced config and the fail-closed target were fixed. The case-3 crash liveness gap is tracked in 🤖 bug: a crash before a background command's child starts leaves a record that refuses workspace removal #5576.
• Final independent check (clean-context agent): "ready with tracked follow-ups". No blocker. The follow-ups are 🤖 bug: a refused or failed background migration can leave its command running untracked #5522 (fix in stacked 🤖 fix: keep a refused or failed migration pending until its command exits #5579) and 🤖 bug: a crash before a background command's child starts leaves a record that refuses workspace removal #5576.
• Decision: ready. Merging with squash, pinned to this head.

---

Generated with xum • Model: anthropic:claude-opus-5-5 • Thinking: high • Cost: $32.91