[mstephenholl]

Why

orch uses <store>/.orch.lock to keep two processes from writing the plan store (units.tsv, ledger.tsv, gates.md, frontier.json, the inbox) at once. Creating the lock is atomic, but taking over a stale one is not. Upstream reports a race there (cursor#730) and has a fix open (cursor#733), but its test admits it can't reproduce the cross-process case. A model checker can explore every interleaving.

What changes

A project-local skill, verify-orch-store-lock, in .agents/skills/, symlinked from .claude/skills/ so that Codex and Claude Code both find it:

• StoreLock.tla models acquireLock, takeOver, holderIsDead, and the release closure in poteto-mode/scripts/orch/store.ts. Each action is one filesystem call or process.kill, and writeFile goes to the inode the process opened, not to whatever is at the path now.
• MutualExclusion is the property: at most one live process is between acquireLock returning and close().
• StoreLockNoCrash.cfg runs three processes that never die. StoreLock.cfg runs three processes, one of which may die at any step.
• check.sh runs both with TLC from TLA+ v1.7.4, which it downloads once to ~/.cache/tla2tools/ and checks by SHA-256. It runs one worker, so a counterexample is the shortest one and the same on every run. Both configurations take about 8 seconds together.
• SKILL.md records the covered code and the sync commit, how the model maps to the code, the expected results, how to tell a bug from a modeling error, how to update the model when the code changes, and what the model leaves out.
• merge-upstream.py keeps project skills. It deletes every tracked path outside KEEP, so the next upstream sync would have removed this skill. KEEP_DIRS now includes .agents/skills/ and .claude/skills/, and the port README lists them. Upstream tracks nothing under either.

Findings

• Stale-lock takeover lets two processes hold the lock. StoreLock.cfg fails in 16 states. p1 takes the lock and dies. p2 and p3 both read p1 from the lock file. p2 takes over and starts work. p3 then confirms that p1 is dead, unlinks the file at the path, which is now p2's live lock, and also starts work. This is pstack orch: stale-lock takeover can be lost (unlink-then-create TOCTOU); frontier SHAs use local branches cursor/plugins#730. The fork's store.ts is identical to upstream's, so the fix should arrive through the sync. The skill says how to update the model when it does.
• A crash between open and writeFile blocks the store. It leaves an empty lock that every later process reads as "unknown", which holderIsDead never treats as dead. Every orch run then refuses until someone passes --force. TLC confirmed it with an extra invariant. The skill lists this under what it doesn't cover, because it's a liveness question, not MutualExclusion.

Proof

• On the current code, StoreLockNoCrash.cfg passes (739 states). StoreLock.cfg fails only with the trace above, the same on repeated runs.
• The check catches a break in the real code. I followed the skill on a scratch change to create() in store.ts, open(path, "wx") changed to open(path, "w"). The skill's git diff against the sync commit flagged the hunk. I updated the model to match, and StoreLockNoCrash.cfg failed in 5 states with two processes working at once. I then dropped the change in both places, and the results were back to the ones above.
• The crash configuration can pass. In a scratch copy, a compare-and-swap takeover, which unlinks only if the file still holds the dead pid that was read, passes StoreLock.cfg (1954 states). So the failure comes from the unconditional unlink, not from the crash model.
• All 252 unit tests pass, including test_the_next_sync_deletes_nothing_this_repository_tracks, which caught the KEEP gap. check.py reports 0 problems, and bash -n check.sh passes. CI runs shellcheck on it.