Verify the session lifecycle (TLA+)

Many agents share one Home (~/.agent-tty by default). Each agent-tty command is its own process, and they all read and write the same session.json files with no lock. A test runs one order of those steps. This check runs every order of them in a small model of one session, and it reports any order that breaks a rule below.

The model is model/SessionLifecycle.tla. Each action in it is one indivisible step of the real code: one file read, the rename that makes a manifest write visible, one rm, one unlink, a process start or end, or a block of synchronous code with no await in it. Every action has a comment that names the code it stands for.

The tool is TLC, the TLA+ model checker, pinned to release 1.7.4 by sha256. The question here is "can these steps happen in a bad order", and a model checker answers that for every order. No verifier runs on this TypeScript code across processes.

The rules

TypeOK also runs in every run. When it breaks, the model is wrong, not the code.

Does your change touch this?

Yes, when the diff changes any of these:

• src/host/lifecycle.ts: allocateSession (and the order of its launch call and first manifest write), launchHost, isProcessAlive, the host proof (readSessionHost, psShowsSessionHost, isHostAlive, hostMatches, killHostBestEffort), cliRunsInsideProgramSession with ownLinuxSessionId, ownProcessGroupId, controllingTerminal and sharesControllingTerminal, reconcileSession, and destroySession with its local stopLeftoversThenRecordDestroyed and its helpers recordDestroyed, stopSessionProcesses, readSessionManifestOrThrow, waitForTerminalManifest, waitForProcessesToExit and killProcessBestEffort, and removeDeadHostSocket, which gc and destroySession call.
• src/host/programGroup.ts: the token capture (captureProgram, captureToken, readAutogroup, parseAutogroup, parseProcStat), the /proc reads (readProcFileIfExists, readLiveThreadState, readProcStat, readShownProcStat, isRefusedRead, readBootId), the record (writeProgramRecord, readProgramRecord, readProvenProgramGroup, readProgramGroup, provenProgramGroupRuns with its GC_JUDGEMENTS limit, judgeGroupForGc, judgeFrozenGroup, probeFindsGroup), procShowsOwnPidSpace, the verdict (judgeProgramGroup, readGroupMembers), and the kill and the probe (stopProgramGroup, isProgramGroupAlive, processGroupTarget, isProcessGroupAlive with groupHasLiveProcess and procHidesOtherUsers, killProcessGroupBestEffort, signalProcessGroup).
• src/host/hostMain.ts: waitForManifestFromCreate, isSessionCommandable, and in runHost the start-up statements (the manifest wait, the hostPid === process.pid check, the host.json write with captureHost and writeHostRecord, createSerialManifestWriter, EventLog.open, the create-failed marker check, createPty, setChildPid, captureProgram), hangUpProgram with its kill timer and the SHUTDOWN_KILL_GRACE_MS constant, startIdlePolling (the idle time-out), initiateShutdown, startShutdown, handlePtyExit with its wait for the program's group, pty.onExit, the SIGTERM handler, the resize and destroy handlers, and the last try block (the program.json write, the start-up manifest write and rpcServer.listen).
• src/host/manifestWriter.ts createSerialManifestWriter.
• src/cli/commands/gc.ts gcSessions and defaultDependencies, src/cli/commands/create.ts runCreateCommand with waitForReadyHost, and src/cli/commands/destroy.ts runDestroyCommand with rerunInNewSession.
• src/host/sessionState.ts setDimensions, requestDestroy, recordDestroyed and recordExit, src/host/eventLog.ts EventLog.open, src/host/rpcServer.ts listen and close, src/host/rpcClient.ts toTransportCliError (which socket errors read as HOST_UNREACHABLE).
• src/host/hostRecord.ts: captureHost, writeHostRecord, readHostRecord, pidExists, judgeHost, inPidNamespace, readTimeNamespace, inTimeNamespace, readMachineId, inHostPidSpace and sharesHostPids.
• src/storage/manifests.ts readValidatedJsonFile, replaceFileAtomic, replaceFileAtomicSync, writeValidatedJsonFileSync, writeManifest, writeDestroyMarker and writeCreateFailedMarker with writeEmptyMarker.
• The SESSION_STATUS_POLICIES table in src/protocol/sessionStatusPolicy.ts.
• Any new or removed call to writeManifest, persistManifest, replaceFileAtomic, writeValidatedJsonFile, writeTextFileAtomic, manifestPath, reconcileSession, writeProgramRecord or stopProgramGroup (also through an import alias), or a recursive rm (one with recursive: true, whatever its argument is named), anywhere in src/.
• This skill's model/SessionLifecycle.tla, scripts/facts.mjs and scripts/check.sh: an edit to them also needs a new confirmed coverage.json.

You do not have to judge this by hand. The check prints STALE when any of these changed since the sync commit.

CI runs the check in the lifecycle-model job. Its first share calls scripts/check.sh --drift-only, which compares the guard values and the covered code with coverage.json and needs no Java, and fails on STALE. The whole check runs only when coverage.json differs from the base of the pull request or merge group, in four jobs with CHECK_SHARD=<i>/4. Each job runs every fourth run that expects pass and every fourth of the rest, because the runs that expect pass explore the whole model and take most of the time.

Run it

From the repo root:

.agents/skills/verify-session-lifecycle/scripts/check.sh

It needs node, Java 11 or newer (java -version), and the network once: the first run downloads tla2tools.jar 1.7.4 into this skill's .cache/ folder (git ignores it) and checks its sha256. On a CI runner with 4 vCPUs and the default CHECK_JOBS of 4 it takes about an hour, so CI runs it in four shares. Ten runs explore more than 20 million distinct states each, so CHECK_JOBS=79 starts every run at once and takes about as long as the longest run. JAVA=/path/to/java picks another Java. TLA2TOOLS_JAR=/path/to/tla2tools.jar uses a jar you already have, which must be the same 1.7.4 build. CHECK_OUT=<folder> keeps the results in that folder (default: a new temp folder, printed at the end).

What it does:

1. scripts/facts.mjs reads the code with the TypeScript compiler. It finds the thirty-six guards that the rules depend on and the status sets of the policy table, and it hashes each covered function with comments and layout removed.
2. It writes one TLC config per run, with those facts as constants. A guard that is not in the code, in the expected place and order, reads FALSE, and the model then runs without it.
3. It runs TLC 79 times and prints one line per run.
4. It compares the guard values, the status sets, the hashes and the call sites with coverage.json.

Exit codes: 0 means every run gave the expected result and the covered code matches the sync record. 1 means at least one run gave an unexpected result; the line says UNEXPECTED. 3 means every result was as expected, but covered code changed since the sync commit; that is not a pass, so follow "When you change covered code on purpose". 2 means a tool could not run. When both 1 and 3 apply, the exit code is 1.

Read the result

At the sync commit, the expected results are:

Read current first. The witness and mutant runs use the same facts from the code, so a code change that breaks current can also turn them UNEXPECTED.

A guard reads FALSE when its condition text, its place or its order differs from what scripts/facts.mjs looks for, also after a refactor that kept the behavior. So when a run turns UNEXPECTED and the Facts: line shows a guard FALSE, first read the guard in the code. If it is still there and still does the same thing, update its pattern in scripts/facts.mjs (step 3 of "When you change covered code on purpose"). That is drift in the check, not a bug.

For every violated run, read the counterexample with the /statechart skill (the statechart skill of the pstack plugin). Each run has its own folder under the results folder. Give /statechart that folder's SessionLifecycle.tla as the spec and its SessionLifecycle.cfg as the config, and give it model/statechart-view.mjs from this skill as its view module. The view labels each state and step in the words of this SKILL.md. /statechart prints the shortest path to each broken rule as numbered steps. The check also writes the bare action names of each counterexample to actions.txt in the run folder.

Bug or modeling error

A counterexample is a bug only if every step can happen in the real code. Map each step to the code that its action comment names. Then replay the path against the real CLI. scripts/replay-hold.mjs holds one file-system call in one agent-tty process, so you can force the order that the trace shows. It changes timing only. Its header comment explains REPLAY_HOLD. Use an isolated run of the verify-agent-tty skill for every replay:

ENV_FILE=$(.agents/skills/verify-agent-tty/scripts/start-run.sh replay)
. "$ENV_FILE"
export NODE_NO_WARNINGS=1
HOLD="--import $PWD/.agents/skills/verify-session-lifecycle/scripts/replay-hold.mjs"

The model's "other command" can reconcile at any time. In the real code, gc and gc --dry-run always reconcile. list, inspect and the dashboard first read the manifest themselves and reconcile only a session whose status is active. So when a trace has that command reconcile a terminal manifest, replay it with gc --dry-run: list skips that session unless it races.

After a replay, run .agents/skills/verify-agent-tty/scripts/cleanup.sh "$ENV_FILE". It destroys the run's sessions, stops every process that carries the run's AGENT_TTY_HOME (also the live host of a session that a replay left failed, which list does not show), and only then removes the run's home and state folders.

If a step cannot happen in the code, the model is wrong: fix the model, and say what was wrong. If the replay shows the break, it is a bug: report it with the steps and the harm, and do not weaken a rule or the model to make the run pass.

Races the guards prevent

Each of these broke the rules in earlier code. The guard named in each heading closes it, and its mutant run shows the race again when the guard is gone. Each replay drives the real CLI. On the current code, each one must show the safe result in its last comment.

CreateRecordsHostPid and HostWaitsForManifest: a starting session read as dead (R1, R2, R5, R6)

Without the guard, allocateSession wrote a manifest with hostPid: null, and the host recorded its pid only later. A reconcileSession in that window (from gc, gc --dry-run, list, inspect, destroy or the dashboard) read the null pid as a dead host, wrote failed, host-death and unlinked the socket, and gc then removed the folder of the starting session. create failed with HOST_UNREACHABLE. With the dashboard open, that hit 4 of 20 create calls.

Now allocateSession calls launch first and writes the first manifest with the returned pid, and runCreateCommand starts the host only through that callback. Because the host can start before that write lands, waitForManifestFromCreate polls for the manifest for as long as the create process lives (launchHost passes its pid as the second argument of _host), and the host then checks that the manifest names its own pid.

LOG=$(mktemp)
REPLAY_LOG=$LOG REPLAY_HOLD='_host:rename:/session.json:1:4000' NODE_OPTIONS="$HOLD" \
  node --import tsx src/cli/main.ts create --json -- sleep 30 &
until grep -q hold "$LOG"; do sleep 0.1; done   # the host holds its start-up write
node --import tsx src/cli/main.ts gc --json      # skips it: "session host is still alive"
wait                                             # create succeeds

ReconcileRereads: a reconcile writes over an exit that it did not read (R4)

Without the guard, reconcileSession built its failed record from the manifest it read before its isProcessAlive check. When the program exited and the host wrote exited and ended in between, the reconcile replaced the exit record, and a program that exited 0 read as failed.

Now reconcileSession reads the manifest again after it finds the host dead, returns when that copy is terminal, and reconciles from that copy. A dead host cannot write again. After its group wait, reconcileSession reads the manifest once more, returns when it is gone or terminal, and builds its record from that copy, so a destroy --force that recorded destroyed during the wait stays destroyed. The guard also reads TRUE when the record comes from that later copy.

node --import tsx src/cli/main.ts create --json -- sh -c 'sleep 5'
REPLAY_HOLD='list:readFile:/session.json:2:8000' NODE_OPTIONS="$HOLD" \
  node --import tsx src/cli/main.ts list --json
cat "$AGENT_TTY_HOME"/sessions/*/session.json   # stays exited, exitCode 0

HostSerializesWrites: a late host write replaces the exit record (R3, R4)

Without the guard, the host's start-up, resize, destroying and exit writes ran as independent async writes. A start-up write could land after the exit write of a program that exited at once, and the manifest said running again.

Now every host write of session.json goes through one createSerialManifestWriter. Writes run in call order, and each takes its snapshot when its turn starts, so the last write holds the latest state.

REPLAY_HOLD='_host:rename:/session.json:1:1500' NODE_OPTIONS="$HOLD" \
  node --import tsx src/cli/main.ts create --json -- true
sleep 2; node --import tsx src/cli/main.ts list --all --json   # status: exited

HostStopsAfterTerminalWrite: a terminal manifest before the host's last write (R1, R7)

Without the guard, a SIGTERM or a destroy request that came while another host write was in flight queued the "destroying" write behind it. When the program ended before that write's turn, the write took the "destroyed" snapshot and landed while the exit write of handlePtyExit was still queued. gc then removed the folder of a host that still wrote to it, and the exit write failed on the removed folder.

Now createSerialManifestWriter writes nothing after it wrote a terminal record, so the terminal write is the host's last write.

LOG=$(mktemp)
REPLAY_LOG=$LOG REPLAY_HOLD='_host:rename:/session.json:1:3000,_host:rename:/session.json:3:6000' \
  NODE_OPTIONS="$HOLD" node --import tsx src/cli/main.ts create --json -- sleep 30 &
until grep -q hold "$LOG"; do sleep 0.1; done   # the host holds its start-up write
kill -TERM "$(node -e 'console.log(require(process.argv[1]).hostPid)' "$AGENT_TTY_HOME"/sessions/*/session.json)"
sleep 4; node --import tsx src/cli/main.ts gc --json
wait; grep -c hold "$LOG"                        # 1: the host made no exit write after "destroyed"

DestroyRecordsDestroyed: a destroyed session that reads failed (R9)

Without the guard, destroy --force killed the host and the program and then called reconcileSession, which read the dead host as a crash. The session read failed, "host process died unexpectedly", and only a second destroy made it destroyed. A plain destroy of a session whose host had crashed did the same. The force path also waited for the socket file, which only the dead host could remove, so it always took 5 seconds.

Now every successful return of destroySession comes right after recordDestroyed, which writes destroyed from a manifest that no host write can follow and unlinks the socket. The force path stops the two processes, reads the manifest again, and stops a child that only that read names. recordDestroyed keeps the exit code (DestroyKeepsExitCode).

DestroyRecordsDestroyed is one fact for all the return paths of destroySession. When one path loses its recordDestroyed, the fact reads FALSE and the model drops recordDestroyed from every path. So the counterexample of mutant-DestroyRecordsDestroyed can go through a path that still records destroyed in the code.

id=$(node --import tsx src/cli/main.ts create --json -- sleep 30 | node -e 'let s="";process.stdin.on("data",(d)=>(s+=d)).on("end",()=>console.log(JSON.parse(s).result.sessionId))')
node --import tsx src/cli/main.ts destroy "$id" --force --json   # returns in about 1 second
node --import tsx src/cli/main.ts inspect "$id" --json           # status: destroyed

ManifestWriteNeedsFolder: a late write brings a removed folder back (R10)

Without the guard, writeManifest went through writeTextFileAtomic, which runs mkdir before every write. A manifest write that landed after gc removed the session folder created the folder again, holding only session.json. destroy and reconcileSession both did that, and list --all showed the stub session until the next gc.

Now writeManifest writes the temp file and renames it with no mkdir, so a write into a removed folder fails with SESSION_NOT_FOUND. reconcileSession then returns. destroy reports SESSION_NOT_FOUND, as it does when its reads find no manifest. A host write fails too. A failed start-up or exit write ends the host, and a failed resize write fails only that RPC.

id=$(node --import tsx src/cli/main.ts create --json -- sleep 300 | node -e 'let s="";process.stdin.on("data",(d)=>(s+=d)).on("end",()=>console.log(JSON.parse(s).result.sessionId))')
LOG=$(mktemp)
REPLAY_LOG=$LOG REPLAY_HOLD='destroy:readFile:/session.json:2:3000' NODE_OPTIONS="$HOLD" \
  node --import tsx src/cli/main.ts destroy "$id" --force --json &
until grep -q hold "$LOG"; do sleep 0.1; done   # destroy holds its read after the kill
node --import tsx src/cli/main.ts gc --json      # removes the session folder
wait                                             # destroy prints SESSION_NOT_FOUND
ls "$AGENT_TTY_HOME/sessions"                    # empty: the folder stays removed

KillsProgramGroup: a process of the program outlives destroy (R11)

Without the guard, the host's shutdown sent SIGHUP to the program and waited, and every kill went to the program's pid. A program that ignores SIGHUP kept running, so a plain destroy ended with HOST_TIMEOUT and the session stayed destroying. A process that the program started, such as sleep 300 & in a shell that ignores SIGHUP, outlived destroy, destroy --force and a reconcile after a host crash, and the session read destroyed or failed.

node-pty starts the program as a session leader, so the program's pid is also its process group id, and the program cannot leave that group. Now every kill goes to the group, through stopProgramGroup in src/host/programGroup.ts. Its helper killProcessGroupBestEffort sends SIGKILL to the negated id. It throws on an id that is not an integer above 1, so it never calls process.kill(0) or process.kill(-1). handlePtyExit kills the group when the program ends during a destroy. stopSessionProcesses kills the group, and waitForProcessesToExit waits until isProgramGroupAlive reads false. reconcileSession kills the group that its re-read names. The model found that last case: a reconcile whose first read came before the host's start-up write killed the program of that copy, which named none, and wrote failed with childPid: null, so nothing could stop the program later.

The kill timer of hangUpProgram, which initiateShutdown and the idle time-out call, kills the group SHUTDOWN_KILL_GRACE_MS (2 seconds) after SIGHUP. So a plain destroy ends within its wait of about 5 seconds, and a program that ignores SIGHUP no longer outlives its idle time-out. When the program exits on that SIGHUP before the timer fires, handlePtyExit clears the timer and kills the group itself, so a process that the program started and that ignores SIGHUP does not outlive the idle time-out either. nvim takes about 1 second to exit on SIGHUP. No rule depends on the timer, because the model has no clock.

KillsProgramGroup is one fact for the helpers in programGroup.ts and three kill sites: the kill in handlePtyExit, the kill and the wait in stopSessionProcesses, and the kill in reconcileSession. When one of them loses its group kill, the fact reads FALSE and the model drops the group kill from all three sites, and every waitForProcessesToExit reads the group gone, as the pid wait before it did. So the counterexample of mutant-KillsProgramGroup can go through a site that still kills the group in the code. The kill timer is not part of the fact. No rule depends on it, because it only bounds how long destroy takes: without its action the model still passes every rule. The kill in handlePtyExit after an idle hang-up is not part of the fact either. No rule depends on it: it goes through stopProgramGroup like every kill, and a process that outlives it is one that the program left, which the model keeps after a normal exit anyway. So a change to the timer shows only STALE (on runHost(parts), or on SHUTDOWN_KILL_GRACE_MS).

LOG=$(mktemp)
REPLAY_LOG=$LOG REPLAY_HOLD='_host:rename:/session.json:1:4000' NODE_OPTIONS="$HOLD" \
  node --import tsx src/cli/main.ts create --json -- sh -c 'trap "" TERM HUP; sleep 300 & wait' &
until grep -q 'hold rename' "$LOG"; do sleep 0.1; done   # the host holds its start-up write
REPLAY_LOG=$LOG REPLAY_HOLD='list:readFile:/session.json:2:6000' NODE_OPTIONS="$HOLD" \
  node --import tsx src/cli/main.ts list --json &          # its reconcile reads create's copy
until grep -q 'release rename' "$LOG"; do sleep 0.1; done
m=$(ls "$AGENT_TTY_HOME"/sessions/*/session.json)
pgid=$(node -e 'console.log(require(process.argv[1]).childPid)' "$m")
echo "pgid=$pgid"                                         # a number: with null the check below proves nothing
kill -KILL "$(node -e 'console.log(require(process.argv[1]).hostPid)' "$m")"
wait; ps -eo pgid=,args= | awk -v g="$pgid" '$1 == g'   # prints nothing: the group is gone

ProbeCountsDeniedGroup: a group of another user's processes reads gone (R11)

kill(-pgid) fails with EPERM when every process left in the program's group belongs to another user, such as the root child of sudo cmd &. Before this guard, both group helpers threw that error. The host died in its kill timer or in handlePtyExit, and destroy, destroy --force and the reconcile after a host crash printed a raw Node stack. The kill can ignore EPERM as it ignores ESRCH, but the probe must not. A probe that reads EPERM as gone lets every wait for the group pass while that process runs, and the session reads destroyed.

Now, on EPERM, isProcessGroupAlive reads the group alive unless two scans of /proc in a row each show only zombies of it (Linux only, see Scope). A group with no process in view also reads alive, because hidepid hides the processes of other users. killProcessGroupBestEffort returns on EPERM. This probe decides for a group without a token. With a token, isProgramGroupAlive reads the group alive while a live member in view carries the token, and a process of another user in the program's session carries it too. When /proc shows no live member, as when hidepid hides that process, the token check asks this probe. mutant-ProbeCountsDeniedGroup-no-token breaks R11 on the path without a token. So destroy --force ends with HOST_TIMEOUT and records nothing while such a process runs. test/fixtures/eperm-group-kill.ts makes every group signal fail with EPERM and deliver nothing, which stands for such a group.

EPERM="--import=$PWD/test/fixtures/eperm-group-kill.ts"
id=$(NODE_OPTIONS="$EPERM" node --import tsx src/cli/main.ts create --json -- sh -c 'trap "" TERM HUP; exec sleep 300' | node -e 'let s="";process.stdin.on("data",(d)=>(s+=d)).on("end",()=>console.log(JSON.parse(s).result.sessionId))')
m="$AGENT_TTY_HOME/sessions/$id/session.json"
NODE_OPTIONS="$EPERM" node --import tsx src/cli/main.ts destroy "$id" --force --json   # HOST_TIMEOUT after about 5 seconds
node -e 'const m=require(process.argv[1]);console.log(m.status, m.childPid)' "$m"      # running and the pid: not destroyed

HostWaitsForGroup: the host records destroyed while the group runs (R11)

Without the guard, handlePtyExit recorded destroyed right after its group kill. A kill that returns 0 does not show that the group is gone: with sudo cmd & the group holds sudo, which we may signal, and its root child, which survives. The session read destroyed while that child ran.

Now the async block of handlePtyExit calls recordDestroyed only after waitForProcessesToExit(null, program) read the group gone. When that wait gives up after about 5 seconds, the host writes its record as it is, destroying without the exit code, and still shuts down. A later reconcile retries the kill. WitnessForeignOutlivesDestroy shows that the model reaches this end.

EPERM="--import=$PWD/test/fixtures/eperm-group-kill.ts"
id=$(NODE_OPTIONS="$EPERM" node --import tsx src/cli/main.ts create --json -- sh -c '(trap "" HUP; exec sleep 300) & wait' | node -e 'let s="";process.stdin.on("data",(d)=>(s+=d)).on("end",()=>console.log(JSON.parse(s).result.sessionId))')
m="$AGENT_TTY_HOME/sessions/$id/session.json"
host=$(node -e 'console.log(require(process.argv[1]).hostPid)' "$m")
NODE_OPTIONS="$EPERM" node --import tsx src/cli/main.ts destroy "$id" --json   # HOST_TIMEOUT
while kill -0 "$host" 2>/dev/null; do sleep 0.2; done                         # the host gives up and ends
node -e 'const m=require(process.argv[1]);console.log(m.status, m.childPid)' "$m"   # destroying and the pid

ReconcileWaitsForGroup: a reconcile forgets a group that still runs (R13)

Without the guard, reconcileSession wrote its record right after its group kill, with childPid: null. When a process of another user survived the kill, the session read failed after a host crash, and nothing could find that process again. A later destroy then recorded destroyed while it ran.

Now reconcileSession returns with no write and no unlink while waitForProcessesToExit(null, group) reads the group alive, for about 5 seconds. childPid stays, so a later reconcile retries the kill.

EPERM="--import=$PWD/test/fixtures/eperm-group-kill.ts"
id=$(NODE_OPTIONS="$EPERM" node --import tsx src/cli/main.ts create --json -- sh -c 'trap "" TERM HUP; exec sleep 300' | node -e 'let s="";process.stdin.on("data",(d)=>(s+=d)).on("end",()=>console.log(JSON.parse(s).result.sessionId))')
m="$AGENT_TTY_HOME/sessions/$id/session.json"
kill -KILL "$(node -e 'console.log(require(process.argv[1]).hostPid)' "$m")"
NODE_OPTIONS="$EPERM" node --import tsx src/cli/main.ts gc --dry-run --json   # after about 5 seconds: "session host is still alive"
node -e 'const m=require(process.argv[1]);console.log(m.status, m.childPid)' "$m"   # running and the pid: childPid kept

ReRunsInNewSession: a destroy inside the program's session dies before it reports (R14)

Without the guard, a destroy that the program ran (sh -c 'agent-tty destroy "$AGENT_TTY_SESSION_ID"'), or that someone typed into the program's interactive shell, ran inside the program's session, and its own stop ended it. With --force it died in the SIGKILL of its own group, and the host then recorded exited. A plain destroy died from the hang-up when the program's leader exited. Either way it printed nothing.

Now runDestroyCommand first asks cliRunsInsideProgramSession. When the CLI runs inside, rerunInNewSession runs the same command detached, in a new session and without AGENT_TTY_SESSION_ID, and exits with that copy's exit code. It forwards SIGINT and SIGTERM to the copy, which the terminal cannot reach in its new session, and a copy that a signal ended exits 128 plus the signal's number. The copy gets AGENT_TTY_DESTROY_RERUN=1, so it skips the check and never starts a copy of its own, whatever ps shows. launchHost and resolvePtyEnv drop that variable, so the host and the session's program never inherit it, and allocateSession leaves it out of the manifest's env. It does the destroy from outside and prints the result. On Linux the check also compares the CLI's session id, from /proc/self/stat, with childPid. That covers a job of an interactive shell, which runs in a process group of its own. When /proc/self/stat cannot be read, as in a chroot without /proc, or shows session id 0, as in a PID namespace whose session leader runs outside it, the check reads the CLI as inside, so it re-runs, and the copy skips the check. Off Linux the check compares the process group and the controlling terminal that /bin/ps shows for the CLI and the program, and a shared terminal also covers that job. Every value but an empty one, ??, ?, - and console counts as a terminal, such as ttys001, pts/3 or the BSD pty ttypa, so two processes without a terminal never match. A wrong match costs one re-run, since the copy skips the check. In the model, a destroy inside the session dies at the first step that ends the program's leader, kills its group or closes its PTY, unless it re-ran.

out=$(mktemp)
id=$(node --import tsx src/cli/main.ts create --json -- sh -c 'sleep 2; "$@" destroy "$AGENT_TTY_SESSION_ID" --force --json > "$0"; sleep 300' "$out" node --import tsx src/cli/main.ts | node -e 'let s="";process.stdin.on("data",(d)=>(s+=d)).on("end",()=>console.log(JSON.parse(s).result.sessionId))')
sleep 6; cat "$out"                                                                                  # ok: true, destroyed: true
node -e 'console.log(require(process.argv[1]).status)' "$AGENT_TTY_HOME/sessions/$id/session.json"   # destroyed

InsideCheckReadsEnv: a destroy before the host's start-up write looks outside (R14)

The model found this race. The program gets AGENT_TTY_SESSION_ID at spawn, but its pid reaches the manifest only with the host's start-up write. Without the guard, a destroy that the program ran before that write read childPid: null, so the check said that it ran outside, and it did not re-run. With --force it killed the host, the closed PTY hung up the program's group, and the CLI died before it printed. The session then read failed.

Now cliRunsInsideProgramSession returns true when AGENT_TTY_SESSION_ID equals the session id, before it reads the manifest. The id comparison stays, for a program whose create --env overrode the variable. The re-run copy does not get the variable, and it skips the check. A needless re-run is harmless, because the check only routes the CLI and never decides a kill. The hold below applies to the host only, though the inner CLI inherits it.

out=$(mktemp)
REPLAY_HOLD='_host:rename:/session.json:1:4000' NODE_OPTIONS="$HOLD" \
  node --import tsx src/cli/main.ts create --json -- sh -c '"$@" destroy "$AGENT_TTY_SESSION_ID" --force --json > "$0"' "$out" node --import tsx src/cli/main.ts
# create fails with HOST_UNREACHABLE: the destroy ended its host during the held write
cat "$out"                                                                                  # ok: true, destroyed: true
node -e 'console.log(require(process.argv[1]).status)' "$AGENT_TTY_HOME"/sessions/*/session.json   # destroyed

RecordsProgramSync: a host death in its start-up write leaves a program that no file names (R16)

Without the guard, the program's pid reached a file only with the host's start-up manifest write, the first await after the spawn. When the host died in that write, no file named the program, and a program that ignores SIGHUP kept running. destroy --force then recorded the session destroyed while the program ran. That is case 2 of coder/agent-tty#203.

Now runHost reads the program's session token with captureProgram right after setChildPid, and writes program.json with renameSync as the first statement of its last try, before await persistManifest(). No statement between createPty and that write awaits, so no event handler of the host runs in between. A host that dies in its start-up write leaves program.json, and destroy --force and a reconcile kill the group that it proves. A host death inside that synchronous block still leaves the program unnamed, and R16 exempts it. Scope gives the length of that window.

LOG=$(mktemp)
REPLAY_LOG=$LOG REPLAY_HOLD='_host:rename:/session.json:1:30000' NODE_OPTIONS="$HOLD" \
  node --import tsx src/cli/main.ts create --json -- sh -c 'trap "" HUP; sleep 300 & wait' &
until grep -q 'hold rename' "$LOG"; do sleep 0.1; done   # the host holds its start-up write
d=$(dirname "$(ls "$AGENT_TTY_HOME"/sessions/*/session.json)")
pgid=$(node -e 'console.log(require(process.argv[1]).pid)' "$d/program.json")   # session.json has childPid: null
kill -KILL "$(node -e 'console.log(require(process.argv[1]).hostPid)' "$d/session.json")"
wait                                                     # create fails: its host died
node --import tsx src/cli/main.ts destroy "$(basename "$d")" --force --json   # ok: true
ps -eo pgid=,args= | awk -v g="$pgid" '$1 == g'          # prints nothing: the group is gone

ProvesGroupOwnership: a kill reaches a group that took the program's group id (R15)

Without the guard, every kill trusted the number that a manifest named. Once every process of the program's group had ended, the kernel could give that id to a new session leader, such as the program of another session. A reconcile of a stale manifest, or destroy --force, then sent SIGKILL to that unrelated group. That is case 5 of coder/agent-tty#203. The model also found the host's own window: the kill timer ends the group, node-pty reaps the program, and another group can take the id before handlePtyExit kills the group again.

Now every group kill goes through stopProgramGroup. With a record that has a token, it reads the process table, finds a live member of the group whose session id is the program's pid and whose autogroup and boot id are the recorded ones, reads that member again, and kills the group, in one synchronous block. When the read finds no live member, it reads the process table once more, because a member can fork and end after the read listed /proc. setsid() gives each new session a new autogroup id from a counter that does not repeat within a boot, and fork() passes it on, so a group that took the id later has another autogroup. Such a group gets no kill, and isProgramGroupAlive reads it gone, so the wait after the kill passes. killProcessGroupBestEffort and processGroupTarget have no callers outside stopProgramGroup and the probe. The replay rewrites the files of a destroyed session so that they name an unrelated session leader, which is what a reused id looks like.

id=$(node --import tsx src/cli/main.ts create --json -- sh -c 'exec sleep 300' | node -e 'let s="";process.stdin.on("data",(d)=>(s+=d)).on("end",()=>console.log(JSON.parse(s).result.sessionId))')
node --import tsx src/cli/main.ts destroy "$id" --json
d="$AGENT_TTY_HOME/sessions/$id"
other=$(sh -c 'setsid sleep 300 </dev/null >/dev/null 2>&1 & echo $!')
until [ "$(ps -o sid= -p "$other" | tr -d ' ')" = "$other" ]; do sleep 0.01; done
node -e '
  const fs = require("node:fs");
  const [dir, pid] = [process.argv[1], Number(process.argv[2])];
  const edit = (file, change) => fs.writeFileSync(`${dir}/${file}`, JSON.stringify(change(JSON.parse(fs.readFileSync(`${dir}/${file}`, "utf8")))));
  edit("program.json", (record) => ({ ...record, pid }));
  edit("session.json", (manifest) => ({ ...manifest, status: "running", hostPid: null, childPid: pid }));
' "$d" "$other"
node --import tsx src/cli/main.ts inspect "$id" --json   # status: failed
ps -o pid=,args= -p "$other"                             # sleep 300 still runs
kill "$other"

DestroyStopsLeftovers: a process that an exited program left outlives destroy (R16)

Without the guard, destroySession recorded a terminal session destroyed with no kill, because such a manifest can be days old, and its group id can name an unrelated group by then. A process that the program started and that ignored the hang-up of the program's exit, such as sleep 300 & after trap "" HUP, kept running after destroy, and list hid it. That is case 1 of coder/agent-tty#203 (coder/agent-tty#204).

Now every terminal path of destroySession goes through stopLeftoversThenRecordDestroyed. It reads program.json with readProvenProgramGroup, kills the group that the record proves, waits for it like destroy --force, and only then records destroyed. A record without a token, or no record, proves nothing, so such a session is recorded destroyed with no kill, as before. The guard also reads readProvenProgramGroup and hasToken, so a change that makes them return no record for a record with a token turns it FALSE.

id=$(node --import tsx src/cli/main.ts create --json -- sh -c 'trap "" HUP; sleep 300 & exit 0' | node -e 'let s="";process.stdin.on("data",(d)=>(s+=d)).on("end",()=>console.log(JSON.parse(s).result.sessionId))')
d="$AGENT_TTY_HOME/sessions/$id"
pgid=$(node -e 'console.log(require(process.argv[1]).pid)' "$d/program.json")
until [ "$(node -e 'console.log(require(process.argv[1]).status)' "$d/session.json")" = exited ]; do sleep 0.1; done
ps -eo pgid=,args= | awk -v g="$pgid" '$1 == g'          # sleep 300 runs in the program's group
node --import tsx src/cli/main.ts destroy "$id" --json   # ok: true
ps -eo pgid=,args= | awk -v g="$pgid" '$1 == g'          # prints nothing: the leftover is gone

CreateStopsOnGiveUp: a create that gave up leaves its session running (R17)

Without the guard, runCreateCommand gave up after 50 failed inspect calls, about 6 seconds, and reported HOST_UNREACHABLE (exit 6) without stopping anything. A host that started slowly, on a loaded machine or after a pause, then listened later, and the session ran although create had failed (coder/agent-tty#209). The reconcileSession call and the HOST_TIMEOUT error after the loop never ran, because the last attempt rethrew its error, and the reconcile would have skipped a live host anyway.

Now every error of the readiness wait (waitForReadyHost), the last failed attempt included, makes runCreateCommand call host.stop(), which sends the host SIGTERM through the ChildProcess handle that launchHost returns. It then rethrows the error with details.sessionId added, so the error code does not change. The handle sends nothing once the host has exited, so a reused pid never gets the signal. The host stops its program and records destroyed once the group is gone, as for any SIGTERM. create writes nothing itself: before the host's start-up write names the program, and without a token, no file names a group that a CLI could prove, so a forced destroy from create would record destroyed while the program runs. runHost registers its SIGTERM handler before it waits for the manifest, and facts.mjs checks that order. A SIGTERM before the spawn makes it return without spawning, and one after the spawn waits for the synchronous start-up block, so the default action can no longer end the host between the spawn and program.json. In the model, the give-up sends that SIGTERM, which HostGetsSigterm takes. The replay holds the host's start-up write past the readiness loop.

LOG=$(mktemp)
REPLAY_LOG=$LOG REPLAY_HOLD='_host:rename:/session.json:1:9000' NODE_OPTIONS="$HOLD" \
  node --import tsx src/cli/main.ts create --json -- sh -c 'trap "" HUP; exec sleep 300'   # exit 6, HOST_UNREACHABLE
sleep 8; node --import tsx src/cli/main.ts list --all --json                                # the session is destroyed

HostChecksCreateFailed: on Windows, a host that the manifest does not name yet serves a failed create (R17)

On Windows, SIGTERM ends the host at once, so the host cannot stop its program. create therefore sends it only once the manifest names the program, and before the host's start-up write it sent nothing: a host that started late listened later and served the session, the coder/agent-tty#209 bug in its most likely case (coder/agent-tty#264).

Now the catch of the readiness wait first writes an empty marker, <session>/create-failed, with writeCreateFailedMarker, and only then reads the manifest for the platform rule. runHost checks for the marker right before its SIGTERM check, before the spawn, and returns without a program when it finds it. It checks again right after its start-up write lands, before it listens, and then calls initiateShutdown, which stops the program and records destroyed. The host's write comes before its check, and create's marker write comes before its read, so either the host finds the marker or create reads the program's pid and sends the SIGTERM. create writes the marker on every platform, and off Windows the SIGTERM also stops the host, so mutant-HostChecksCreateFailed passes and only mutant-HostChecksCreateFailed-win32 breaks R17. In the model, CreateGivesUp writes the marker, and with Win32 CreateStopsHostOnWindows reads the manifest and ends a named host as a crash. HostOpensLogAndSpawns and HostChecksMarker are the two checks. The integration test a create that gives up on Windows, where SIGTERM ends the host at once runs the Windows path on Linux: a preload makes create read win32 and turns its SIGTERM into a SIGKILL.

FallbackNeedsFolder: a childPid that gc's removal left stale gets the kill (R15)

The model found this race. Without a token, readProgramGroup falls back to the childPid of the manifest copy that the caller read before it, as before program.json existed. When gc removed the session folder between that read and the program.json read, the record read missing too, and the kill used a childPid whose group could have ended and whose id could name an unrelated group by then.

Now that fallback carries the session folder, and stopProgramGroup kills it, and isProgramGroupAlive probes it, only while the folder exists, checked in the same synchronous block. A session with a record names its childPid only after the record, so a record that is missing from a folder that still exists marks a session that never had one. The replay holds the manifest read of destroy --force while the program exits and gc removes the folder, and a preload logs every group kill.

KILLS=$(mktemp)
LOGGER=$(mktemp --suffix=.mjs)
echo "import { appendFileSync } from 'node:fs'; const kill = process.kill.bind(process); process.kill = (pid, signal) => { if (pid < -1) appendFileSync(process.env.KILLS, pid + ' ' + signal + '\n'); return kill(pid, signal); };" >"$LOGGER"
id=$(node --import tsx src/cli/main.ts create --json -- sh -c 'sleep 2' | node -e 'let s="";process.stdin.on("data",(d)=>(s+=d)).on("end",()=>console.log(JSON.parse(s).result.sessionId))')
LOG=$(mktemp)
KILLS=$KILLS REPLAY_LOG=$LOG REPLAY_HOLD='destroy:readFile:/session.json:2:6000' NODE_OPTIONS="$HOLD --import=$LOGGER" \
  node --import tsx src/cli/main.ts destroy "$id" --force --json &
until grep -q 'hold readFile' "$LOG"; do sleep 0.1; done   # destroy holds the running copy
until grep -q '"exited"' "$AGENT_TTY_HOME/sessions/$id/session.json"; do sleep 0.1; done
node --import tsx src/cli/main.ts gc --json              # removes the session folder
wait                                                     # destroy prints SESSION_NOT_FOUND
cat "$KILLS"                                             # prints nothing: no group kill

ReconcileRepairsDestroyed: a reconcile writes failed over a destroyed that destroy reported (R18)

A reconcile that found the host dead read the manifest a last time, waited for the program's group and then wrote failed from that copy. A destroy --force that wrote destroyed in between printed destroyed: true, and then the reconcile's write replaced its record, so the session read failed (coder/agent-tty#217). R9 only checks what destroy wrote or read, and R3 lets one terminal status follow another, so no rule caught it.

Now recordDestroyed writes an empty marker, <session>/destroyed, with writeDestroyMarker right before its destroyed write. Like the manifest write, the marker write never creates the session folder. After its own write, in the same try, reconcileSession checks for the marker and, when it finds one and its own write was not destroyed, writes destroyed from the same copy, with hostPid and childPid null and no failure. Only a destroy writes the marker, right before its write, so a reconcile write that lands after the marker can have replaced that record. The replay holds the rename of the reconcile in list while destroy --force runs.

id=$(node --import tsx src/cli/main.ts create --json -- sh -c 'exec cat' | node -e 'let s="";process.stdin.on("data",(d)=>(s+=d)).on("end",()=>console.log(JSON.parse(s).result.sessionId))')
kill -KILL "$(node -e 'console.log(require(process.argv[1]).hostPid)' "$AGENT_TTY_HOME/sessions/$id/session.json")"
LOG=$(mktemp)
REPLAY_LOG=$LOG REPLAY_HOLD='list:rename:/session.json:1:4000' NODE_OPTIONS="$HOLD" node --import tsx src/cli/main.ts list --json >/dev/null &
until grep -q 'hold rename' "$LOG"; do sleep 0.1; done
node --import tsx src/cli/main.ts destroy "$id" --force --json   # ok: true, destroyed: true
wait
node -e 'console.log(require(process.argv[1]).status)' "$AGENT_TTY_HOME/sessions/$id/session.json"   # destroyed

ReconcileRepairsMarked: a marked session that a killed reconcile left failed

ReconcileRepairsDestroyed repairs a destroyed record in the reconcile that replaced it, right after its own write. A reconcile process that was killed between that write and the repair left failed, after destroy had printed destroyed: true, and every later reconcile skipped the terminal manifest (coder/agent-tty#265). A destroy of an ended session that failed after its marker write left the marker next to exited or failed the same way.

Now reconcileSession first checks a terminal manifest other than destroyed for the marker. When the marker is there, writeMarkedDestroyed writes destroyed from that copy, with hostPid and childPid null, the exit code kept and no failure fields, and the reconcile unlinks the socket, which a destroy whose write failed left, and the old socket of an older host, and returns. Only a destroy writes the marker, after it stopped the session and right before its destroyed write, so the marker means that destroy chose destroyed. scanHome skips a session with the marker, so home list and the dashboard picker do not count it while its manifest reads failed. The replay holds the repair write of the reconcile in list and kills that process:

id=$(node --import tsx src/cli/main.ts create --json -- sh -c 'exec cat' | node -e 'let s="";process.stdin.on("data",(d)=>(s+=d)).on("end",()=>console.log(JSON.parse(s).result.sessionId))')
kill -KILL "$(node -e 'console.log(require(process.argv[1]).hostPid)' "$AGENT_TTY_HOME/sessions/$id/session.json")"
LOG=$(mktemp)
REPLAY_LOG=$LOG REPLAY_HOLD='list:rename:/session.json:1:4000,list:rename:/session.json:2:60000' NODE_OPTIONS="$HOLD" node --import tsx src/cli/main.ts list --json >/dev/null &
until grep -q 'hold rename' "$LOG"; do sleep 0.1; done
node --import tsx src/cli/main.ts destroy "$id" --force --json   # ok: true, destroyed: true
until [ "$(grep -c 'hold rename' "$LOG")" -ge 2 ]; do sleep 0.1; done
kill -KILL $!                                                     # the reconcile dies before its repair
node --import tsx src/cli/main.ts list --all --json               # the session reads destroyed

TokenNamesProgram: a token that no member of the group carries (R16)

node-pty returns before the program calls setsid(), so the first reads of the program often show the host's own session and autogroup. Without the guard, captureToken could keep an autogroup that it read before the program's setsid(), while its next read of the program's stat already showed the new session. The record then held the host's autogroup. No member of the program's group carries that id, so every kill through the record killed nothing and every wait through it read the group gone. destroy then recorded destroyed while a process of the program's group ran.

Now captureToken reads the program's stat, then its autogroup, then its stat again. It keeps the autogroup only when the second read shows the program as the leader of its own session, with the same start time and the host as its parent, and when the autogroup differs from the host's own. In the model, without the guard every kill through the record kills nothing, and every wait through it reads the group gone. The unit test "records no token while the child shows the host's autogroup" in test/unit/host/programGroup.test.ts shows the code side: a child whose autogroup reads as the host's gets no token.

UnsharedGroupReadsUnknown: destroy from another pid space records destroyed while a leftover runs (R16)

A CLI without /proc, with an empty /proc, in another pid namespace or on another machine than the host sees none of the program's processes: its scan lists none, and its probe kill(-pgid, 0) ends ESRCH, or reaches a group of its own pid space that carries another autogroup. Without the guard, such a group with a token read gone, so destroy of an exited session recorded destroyed while a process that the program left still ran (Codex on coder/agent-tty#274).

Now readProgramGroup and readProvenProgramGroup return the unshared group when sharesHostPids reads false: host.json names another pid namespace or machine, this process cannot read /proc/self/ns/pid, or its /proc/self names another pid, as a /proc of another pid namespace does. It reads alive, so the wait times out with HOST_TIMEOUT, and it gets no kill and no SIGSTOP. A record with a token but no host.json gives the unshared group too, because nothing names the host's pid space. Only an agent-tty version between program.json and host.json, which no release holds, wrote such a session: the host now records a token only when it wrote host.json (RecordsProgramSync reads that statement). A session without a token and without host.json, as from a release before them, keeps the old answer. stopLeftoversThenRecordDestroyed trusts a destroyed record of such a session without the wait, because only a process that saw the group wrote it, after a wait that read the group gone. So a plain destroy of a live session still ends ok, which WitnessUnsharedDestroyCompletes checks. The guard reads all of these statements and sharesHostPids.

id=$(node --import tsx src/cli/main.ts create --json -- sh -c 'trap "" HUP; sleep 300 & exit 0' | node -e 'let s="";process.stdin.on("data",(d)=>(s+=d)).on("end",()=>console.log(JSON.parse(s).result.sessionId))')
d="$AGENT_TTY_HOME/sessions/$id"
until [ "$(node -e 'console.log(require(process.argv[1]).status)' "$d/session.json")" = exited ]; do sleep 0.1; done
AGENT_TTY_TEST_OTHER_PIDS=1 NODE_OPTIONS=--import=./test/fixtures/no-proc.ts node --import tsx src/cli/main.ts destroy "$id" --json   # before: ok: true; now: HOST_TIMEOUT
node -e 'console.log(require(process.argv[1]).status)' "$d/session.json"                                                            # before: destroyed; now: exited

GcKeepsLiveGroup: gc removes the record of a process that the program left (R20)

Without the guard, gcSessions removed the folder of every collectable session. A program that exits on its own can leave a process in its group, such as sleep 300 & after trap "" HUP, and the host does not kill at a normal exit. The rm deleted program.json with the folder, and that record is the only proof that the process is the program's, so no later command could stop it.

Now gcSessions calls provenProgramGroupRuns after its other checks and before the rm. It judges the group that readProvenProgramGroup gives, as the waits of destroy do, and gc skips the session with the reason "the session's program group still runs (destroy ends it)" while it proves the group, also under --dry-run: a live member carries the token. A read that throws skips the session too, with the error as the reason. A member of a fork chain can end between its stat and its autogroup read (unknown), or show up only after the judge's scans, so judgeGroupForGc reads such a judgement as inconclusive, and gc judges again, at most ten times. gc does not check a destroyed session, because destroy records destroyed only after a wait that read the group gone. A record without a token proves nothing, so gc removes such a session as before. gc never keeps a session that no command can remove: a group that gc cannot check proves nothing, and gc removes its session as before. That covers another pid space, where the group reads unshared (as after a container restart that keeps the home, when host.json names a pid namespace that no longer exists), and a /proc that refuses the boot id or the autogroup of a live member (unknown). So R20 holds only for a gc in the host's pid space, and witness-WitnessUnsharedGcRemovesLeftover-otherspace shows that a gc in another one removes an exited session while a process that the program left runs. gc judges without a SIGSTOP first, so a fork chain that no scan shows reads gone to the judge. So provenProgramGroupRuns also counts the group as running while the probe kill(-pgid, 0) finds its id and no scan shows a member, live or zombie (GcProbesUnseenGroup). Under a PID 1 that never reaps, the chain also leaves zombies in view, so the scans show only zombies while its live member escapes them. Then judgeFrozenGroup sends SIGSTOP, as stopProgramGroup does, judges the stopped group, whose stopped member stays in view, and sends SIGCONT in a finally (GcFreezesUnseenGroup). Another gc or a destroy can send SIGCONT before that judgement, so a frozen group that still reads gone is judged again with another SIGSTOP, and only GC_JUDGEMENTS such judgements read it ended. The model has one gc, so it leaves that race out. It sends SIGSTOP only where /proc shows its own pid space. mutant-GcFreezesUnseenGroup-unseen-zombies must violate R20, and "gc keeps an exited session while a fork chain runs behind its zombies" in test/integration/non-reaping-init.test.ts covers it. An unrelated group that took the id is in view and reads unproven, so it does not keep the session. mutant-GcProbesUnseenGroup-unseen must violate R20. The integration tests "gc keeps an exited session while a process that the program left runs" and "... while a fork chain that the program left runs" in test/integration/lifecycle.test.ts cover both, and "gc removes an exited session whose host.json names another pid namespace" covers the restart.

id=$(node --import tsx src/cli/main.ts create --json -- sh -c 'trap "" HUP; sleep 300 & exit 0' | node -e 'let s="";process.stdin.on("data",(d)=>(s+=d)).on("end",()=>console.log(JSON.parse(s).result.sessionId))')
d="$AGENT_TTY_HOME/sessions/$id"
until [ "$(node -e 'console.log(require(process.argv[1]).status)' "$d/session.json")" = exited ]; do sleep 0.1; done
node --import tsx src/cli/main.ts gc --json      # skipped: the session's program group still runs
node --import tsx src/cli/main.ts destroy "$id" --json
node --import tsx src/cli/main.ts gc --json      # removes the session

CreateRecordsHost: a CLI in another pid space reads a starting host dead (R2)

A CLI in another pid namespace finds no process with the host's pid, so judgeHost reads the host dead unless host.json names it. The host wrote host.json only once it had read its manifest. A list, inspect or gc in another pid namespace that read the session between create's first manifest write and that record recorded a live host failed, and gc could then remove its folder.

Now allocateSession reads the launched host with captureHost and writes host.json with writeHostRecord right after the launch, before the first manifest names the host. The host writes the record again when it starts. A capture that fails (no /proc, or off Linux) writes nothing, and then only the host writes the record. In the model, CliHostAlive is the CLI's view of the host: in another pid space a host that host.json names reads alive, and one that it does not name reads dead. mutant-CreateRecordsHost-otherspace must violate R2. witness-WitnessUnrecordedHostMeetsKill runs without the guard, because a live host that host.json does not name is out of the model's reach with it.

ReusedIdReadsGone: a wait that never ends while an unrelated group holds the id

isProgramGroupAlive reads a group with a token alive while the check finds a live member with the token (owned), while it cannot run (unknown), and while it finds no live member and the probe of the id reads alive. A group whose live members carry another autogroup (unproven) reads gone. Without the guard, a group that took the program's id after the program's group ended read alive. destroy of the exited session then waited until it ended with HOST_TIMEOUT, and every reconcile waited and wrote nothing, until that unrelated group ended.

No rule breaks then, because the model has no rule for a wait that never ends. So the ghost passedReused records a wait of destroy through program.json that read the group gone while an unrelated group held its id, and WitnessWaitPassesReusedId must reach that state. Without the guard the wait never passes in that state, so mutant-ReusedIdReadsGone expects pass.

ProvesHostPid: destroy --force kills a process that took the host's pid (R19)

destroy --force sent SIGKILL to the number in session.json's hostPid, and reconcile read that number with kill(pid, 0). After the host died, another process could get its pid. Reconcile then read that process as the live host, and destroy --force killed it. A crashed host that stayed a zombie under an init that never reaps also read alive, so list kept the session running and destroy --force ended with HOST_TIMEOUT (coder/agent-tty#218).

Now the host writes host.json with writeHostRecord right after it read its manifest: its pid, the boot id and its start time from /proc/self/stat. judgeHost reads the host dead only on proof (no process has the pid, a zombie has it, or another boot or start time), alive when the boot id and the start time match the record, and unknown when it cannot read /proc or the record. killHostBestEffort kills only when hostMatches proves the host. The test below points session.json and host.json at a process that is not the host, as a reused pid would: the record keeps the start time of the host that died.

id=$(node --import tsx src/cli/main.ts create --json -- sh -c 'exec cat' | node -e 'let s="";process.stdin.on("data",(d)=>(s+=d)).on("end",()=>console.log(JSON.parse(s).result.sessionId))')
d=$AGENT_TTY_HOME/sessions/$id
kill -KILL "$(node -e 'console.log(require(process.argv[1]).hostPid)' "$d/session.json")"
setsid sleep 300 </dev/null >/dev/null 2>&1 & other=$!
node -e 'const fs=require("fs");for(const [f,k] of [["session.json","hostPid"],["host.json","pid"]]){const p=process.argv[1]+"/"+f;const m=JSON.parse(fs.readFileSync(p));m[k]=Number(process.argv[2]);fs.writeFileSync(p,JSON.stringify(m))}' "$d" "$other"
node --import tsx src/cli/main.ts destroy "$id" --force --json   # ok: true, destroyed: true
kill -0 "$other" && echo alive                                     # alive

FreezesUnseenGroup: a fork chain outlives destroy (R11)

With a token, a kill needs a live member of the group in view, and a wait reads the group gone once no scan shows one. A program whose processes each fork their successor and end within about 2 ms, a fork chain, is almost never in view: by the time a scan reads a pid that its /proc listing showed, that process has ended, and the listing missed its successor. stopProgramGroup then killed nothing, the wait after it read the group gone, and destroy recorded destroyed while the chain ran (coder/agent-tty#244).

Now stopProgramGroup sends a group that judgeLiveGroup reads gone SIGSTOP and judges it again, until the loop's attempts run out. Each judgement that reads gone sends SIGSTOP again, so a member that a SIGCONT from elsewhere resumed stops again. When /proc/self does not name this process's pid, /proc belongs to another pid namespace, so procShowsOwnPidSpace reads false and no SIGSTOP goes out: the group id can name the CLI's own group there. The kernel delivers a group signal also to a child that a member forks during the delivery, so the whole chain stops, and a stopped process stays in view. The next judge finds a stopped member with the token, and the group gets the kill. A frozen group that gets no kill, because its members carry another autogroup, only zombies are left, or a scan throws, gets SIGCONT from a finally block. In the model, the constant Unseen hides every process of the program from the scans: without the guard the kill through the token kills nothing, and the wait reads the group gone. current-unseen checks every rule with Unseen, and mutant-FreezesUnseenGroup-unseen must violate R11. The integration test "destroy ends a fork chain that no scan of /proc shows" in test/integration/lifecycle.test.ts runs test/fixtures/fork-chain.py in a session.

id=$(node --import tsx src/cli/main.ts create --json -- sh -c "python3 test/fixtures/fork-chain.py 30 0.002 $PWD/beat & wait" | node -e 'let s="";process.stdin.on("data",(d)=>(s+=d)).on("end",()=>console.log(JSON.parse(s).result.sessionId))')
sleep 1; node --import tsx src/cli/main.ts destroy "$id" --json   # ok: true, destroyed: true
a=$(cat beat); sleep 1; [ "$a" = "$(cat beat)" ] && echo ended    # ended

When you change covered code on purpose

1. Read the diff of every item that STALE lists, and the commits that the check prints. For a change that is not committed yet, read git diff.
2. Decide for each change: it does not alter what an action describes (formatting, a renamed local, an unrelated branch), or the model must change (a step split in two, a guard moved, a new writer of session.json, a new reconcile caller with a different flow), or the promise changed on purpose (cite the evidence: the doc comment, CONTEXT.md, the tests, the commit message).
3. Update the model from the code, not from the result. One indivisible step in the code stays one action, and its comment names the code. If a guard moved, update its pattern in scripts/facts.mjs.
4. Run the check. For a new or changed guard, break it once in a scratch edit of the real code (delete it, or move it after the write it guards) and confirm that a run turns UNEXPECTED. Then drop the scratch edit.
5. When the model describes the code again, run scripts/check.sh --update-coverage and commit coverage.json with the model change. That commit becomes the sync commit.

To add a guard, give it a constant in the model, make the actions run with and without it, read it in scripts/facts.mjs, add it to GUARDS in scripts/check.sh, and add its mutant run with the rule it protects.

To bring the check back in line after changes that skipped it, use /maintain-formal-verification-skill (a pstack plugin skill).

Scope

The model checks every order of these steps for one session: one create that can give up on its host, its host, one gc pass over that session (not --dry-run), one other command that reconciles twice, one resize, one destroy (with or without --force, from outside or from inside the program's session), one SIGTERM to the host, a program exit at any time, a process of another user in the program's group that starts and ends at any time, a process that the program leaves when it exits on its own, the host's host.json and program.json writes, an unrelated group that takes the program's group id once the whole group has ended, an unrelated process that takes the host's pid once the host has ended, the kill timer of the host's shutdown, and a host crash at any time. With a token the model has 29,309,460 distinct states, and without one 29,186,546. The check prints both counts.

It assumes:

• isHostAlive reads the host dead only on proof, through judgeHost: no process has hostPid (kill(pid, 0) gives ESRCH), /proc/<hostPid>/stat shows a zombie, or host.json names another boot id or another start time than that process has. A missing or unreadable host.json (a create and a host that could not read /proc, or an agent-tty version without it), a /proc that is not mounted or refuses the read, and a CLI in another pid namespace or on another machine than the ones that host.json names leave the host unknown, which reads alive and gets no kill. A CLI in another time namespace, where /proc adds another boottime offset to the start time, reads a host that a process still runs as unknown too. For a CLI in another pid namespace or on another machine, readProgramGroup without a token names no group either (sharesHostPids), so the childPid fallback gets no kill, and the unknown host keeps the session from a terminal write. create writes host.json right after it launched the host, and the host writes it again right after it read its manifest, with no await between. So on Linux with /proc, isHostAlive is true exactly while the host lives, as the model's hostAlive is, also for a host whose command line --title replaced. destroy --force sends SIGKILL to hostPid only when hostMatches proves the host: on Linux the boot id and start time match host.json, off Linux /bin/ps -o command= shows _host <session id>. A pid has one start time per boot, so a process that took the pid never matches (R19, coder/agent-tty#218). The check and the kill are separate system calls, the same window as for the program's group. Off Linux isHostAlive is kill(pid, 0), so a zombie host or a process that took the pid reads alive: list keeps such a session running, and destroy --force kills nothing and ends with HOST_TIMEOUT. On Windows the check never passes, so destroy --force never kills the host there. The model's host record (hrec) is written when create launches the host and in the host's manifest read, and the model lets an unrelated process take the pid of an ended host at any step (HostPidReused). It has no zombies.
• The kernel does not reuse a pid while a process group with that id exists, so a kill of the program's group id reaches only that group while a process of it runs. Once the whole group has ended, a new process can get that id and lead an unrelated group (case 5 of coder/agent-tty#203). The model lets that happen at any step after the group ended. With a token, stopProgramGroup kills only right after it read a live member that carries the token again, and the model takes that check and the kill as one step. No API holds a process group the way a pidfd holds one process, so a gap stays between the check and the kill(2): from the start of the member's re-read to the kill call it took p50 24 µs, p99 69 µs and at most 81 µs over 300 kills at a load average of 43. A group that takes the id inside that gap needs every member to exit, the pid counter to wrap onto the id, and the new process to lead a group, all within those microseconds.
• The program runs from the spawn on, but program.json names it only after captureProgram read its token and writeProgramRecord renamed the file, in the same synchronous block. A host death inside that block leaves a program that no file names, and R16 exempts it (case 2 of coder/agent-tty#203). Over 150 sequential create calls on Linux, from the return of node-pty's spawn to the renamed program.json, at 1-minute load averages of 38 to 83, that took a median of 2.8 ms, a 90th percentile of 4.3 ms and at most 66 ms. A scratch build of runHost timed it with performance.now(). captureProgram took a median of 1.3 ms and at most 7.3 ms of that, so the long tail lies in the rest of the block and the write. node-pty returns before the child has called setsid(), so the capture polls for at most 250 ms until the child leads its own session.
• OtherPidSpace changes only how destroy, list and gc see the program's group. Their view of the host stays as in the shared pid space. CliHostAlive gives their view of the host: judgeHost reads a host that host.json names in another pid space as unknown, also after the host ended, so they never record it failed, and hostMatches never proves it, so destroy --force kills no host there. Without host.json they probe the pid in their own pid space, where no process has it, and read the host dead. create writes host.json before the first manifest names the host, so only a capture that failed, which the model leaves out, leaves that window open.
• current describes Linux with autogroups, where the capture finds the token. The model reads every autogroup and the boot id. When /proc refuses the boot id, or shows no autogroup id for a live member in the program's session (a refused read, or an empty or malformed file), judgeProgramGroup gives unknown: no kill, and isProgramGroupAlive reads the group alive, so destroy ends with HOST_TIMEOUT and a reconcile writes nothing, as while a process of another user runs. A CLI that cannot list /proc at all, as in a chroot, sees no member. judgeProgramGroup then gives gone, so nothing gets the kill, and the probe of the group decides whether it reads alive. The model leaves those refused reads out. Without a token, readProgramGroup falls back to the childPid of the manifest, as before program.json existed: on macOS and Windows, on a kernel without CONFIG_SCHED_AUTOGROUP, when the capture read no autogroup or no boot id, and for a session that an older agent-tty created. There a reconcile and destroy --force kill that childPid as it is, destroy of a terminal session kills nothing, and a kill can still reach an unrelated group that took the id. current-no-token checks that fallback: the constant Token is FALSE there, so program.json names no group, and the host kills and probes the program's pid as it is. R15 and R16 do not hold on that path, so the run checks R1 to R14. The fallback kills only while the session folder exists. gc's real rm deletes file by file, so while it runs the folder can exist after program.json is gone, and a fallback kill in that moment can use a childPid that gc's removal made stale.
• A program.json that does not parse, or that another version wrote, proves nothing: it gets no kill, and reconcile and destroy do not throw. A missing one gets the childPid fallback above.
• A manifest write is atomic, because writeManifest renames a temp file. A write that fails counts as a host crash or a failed command. That covers a host write into a removed folder, which only a state that already breaks R1 reaches.
• The host waits for its manifest while the create process lives, so it gives up only when create dies before that write. That counts as a host crash, which R6 does not cover.
• gc's rm(sessionDirectory, { recursive: true, force: true, maxRetries: 3, retryDelay: 10 }) is one step, though the real rm deletes file by file. R1 already forbids removing a session whose host can still write, so for the host the order of the deleted files does not matter. A reconcile or destroy write can land during the real rm, after it listed the folder, and make its last rmdir fail with ENOTEMPTY. The rm then runs again, up to 3 times, after waits of 10, 20 and 30 ms, and deletes the late session.json (coder/agent-tty#202). A write after the last rmdir fails, because writeManifest runs no mkdir. The folder stays only when a write lands in each of the 4 runs, and the next gc then removes it.
• removeDeadHostSocket judges the host once, from the copy of gc's last read or of destroy's first read. The model joins that judge to the read and the unlink to gc's rm, and reads hostAlive for judgeHost. judgeHost reads a dead host alive only when its pid now names another process, and no rule depends on the socket of a dead host. A run without the judge, which unlinks at every gc removal and every destroy of a destroyed session, also holds every rule, so the judge has no guard. The model has one host version, so the old socket path of an older host is outside it.
• Steps that only lead to the same outcome are joined: gc's readdir and stat (both only skip), the host's EventLog.open and createPty (synchronous after the open), and recordExit with the exit event append (no other process sees them).
• A program can outlive its host: the PTY closes with the host and sends the program SIGHUP, which a program can ignore. The model keeps such a program running until a kill of its group ends it, the worst case for R11. A SIGKILL of the group ends every process of our user in it at once.
• A process of another user can run in the program's group, such as the root child of sudo cmd &. Our SIGKILL does not reach it, and once only such processes are left, kill(-pgid) fails with EPERM. isProcessGroupAlive reads EPERM as alive unless /proc shows only zombies of the group, and killProcessGroupBestEffort ignores it. While such a process runs, three things take about 5 seconds, the length of waitForProcessesToExit. The host waits that long after the program's exit, then leaves the manifest destroying and ends. destroy and destroy --force end with HOST_TIMEOUT. Every reconcile of the session (list, inspect, gc, the dashboard) waits that long and writes nothing. The model lets each wait give up at any poll that reads the group alive. With a token, the model lets such a process carry the token in view. Where /proc hides or refuses it, the token check reads it through isProcessGroupAlive, which reads it alive in the same states while ProbeCountsDeniedGroup holds.
• A killed process stays a zombie until its parent, or init once its parent has died, reaps it, and kill(-pgid, 0) still finds a zombie. On Linux, isProcessGroupAlive then reads /proc/<pid>/stat of every process and reads the group gone when two scans in a row each show processes of it and only zombies, because a process can fork and end while one scan runs. When a scan shows no process of the group, the probe decides: EPERM reads alive and a found group reads gone. So a group whose last processes are never reaped, as under a container's PID 1 without an init, reads gone. A process whose main thread called pthread_exit while another thread runs also shows Z there, so readProcStat reads /proc/<pid>/task of every process that shows Z and gives it the state of a thread that is not a zombie. Such a process counts as live in the scan and in the token check, where it can carry the token. On macOS it does not scan, so a zombie still reads alive until launchd reaps it. The model has no zombies: a killed process ends at once. A process that /proc refuses to show, as hidepid=1 (EPERM) or a security module (EACCES) does for other users, reads alive. With hidepid=2 or hidepid=4 (invisible and ptraceable on newer kernels), /proc can leave such a process out of its listing, so the probe reads the last /proc line of /proc/self/mountinfo, skips the scan and reads a group with a zombie alive, as on macOS. With a token, neither a zombie nor a process that /proc refuses to show witnesses the token. When no live member is in view, isProgramGroupAlive reads the group as isProcessGroupAlive does, with the zombie scan, the refused reads and the same hidepid check. So under any of those hidepid modes, a group that a process of another user took after the program's group ended reads alive, and destroy ends with HOST_TIMEOUT until that process ends.
• A destroy that lands between reconcile's last read and its write is still overwritten with failed, for the time until that reconcile finds the destroy marker and writes destroyed again (ReconcileRepairsDestroyed). A list or gc that reads in that time sees failed, a terminal status, so gc can remove the folder as it would remove a destroyed one. A reconcile whose process dies in that time leaves failed until the next reconcile reads it: that read finds the marker and writes destroyed (ReconcileRepairsMarked). home list and the dashboard count a session with the marker as destroyed, also in that time. The model has no crash of a reconciling process, so it checks that the repair at the read breaks no rule, not that it heals the crash.
• The idle time-out calls the same hangUpProgram as initiateShutdown: SIGHUP, then the group kill after SHUTDOWN_KILL_GRACE_MS. When the program exits on that SIGHUP, handlePtyExit kills the group too, so a process that ignores SIGHUP does not outlive the idle time-out. An idle time-out still ends exited. When the check cannot run (unknown), the idle kill sends nothing, and the session ends exited with that process running, as after a program that exits on its own and leaves a process (coder/agent-tty#222). The model leaves both group kills out: they go through stopProgramGroup like every kill, and a process that outlives them is one that the program left, which the model keeps after a normal exit anyway.
• Windows has no process groups, so there processGroupTarget gives the program's pid, and every kill reaches only that process. destroy never re-runs on Windows. There SIGTERM ends the host at once, so a create that gives up sends it only once the manifest names the program, and the next reconcile records failed and ends the program. Before that write, the host finds the create-failed marker (HostChecksCreateFailed). current-win32 checks this with a SIGTERM that is a host crash and without a token, and keeps the process groups of Linux. A marker write that fails, for example on a full disk, leaves a host that the manifest does not name yet serving on Windows. The model has no such failure.
• A host stopped with SIGSTOP, or with a blocked event loop, takes the SIGTERM of a create that gave up only when it runs again. Until then its program runs and the session reads running, which R17 allows because the SIGTERM is still on its way. A plain destroy fails because the host does not answer, and only destroy --force ends such a session sooner.
• A destroy that the program runs, or that someone types into the program's interactive shell, runs inside the program's session, and rerunInNewSession runs it again in a new session. The model lets such a destroy start while the program's leader runs, and assumes that it kept AGENT_TTY_SESSION_ID, which every process of the program inherits at spawn. A destroy whose environment lost the variable, or whose create --env overrode it, is seen through the id comparison only. On Linux that compares the CLI's session id with childPid, so it misses such a destroy only before the host's start-up write. Other POSIX systems compare the process group and the controlling terminal, through /bin/ps. A terminal is the controlling terminal of one session and of every process in it, so that also finds a job of an interactive shell, which runs in a group of its own. A process without a controlling terminal is seen only through the group.
• The program's processes stay in its process group. A process that leaves the group (setsid, or the job control of an interactive shell) is out of reach of the group kill, and it is no witness for the token either. That is case 4 of coder/agent-tty#203, a documented limit with no code change.
• A process that the program left when it exited on its own stays in the program's group and session, so it carries the token. destroy of the terminal session kills it through program.json (case 1 of coder/agent-tty#203, coder/agent-tty#204). Nothing else stops it: the host does not kill at a normal exit, and gc removes program.json with the folder, so a process that a session removed by gc left stays unproven. The model drops a process of another user at a normal exit.
• The destroy RPC is one step: the host's handler does the work. destroySession's own reconcileSession calls are the reconciles of the other command, so destroy itself only reads after them. A poll that reads an active status is either retried later or is the last of its 50 tries.
• Only the "destroying" write of initiateShutdown can wait for its turn while the in-memory status changes, so only it keeps its snapshot in the model. The start-up, resize and exit writes carry a status that cannot change before their turn.
• A group id that an unrelated group took after the program's group ended, whose processes no scan shows either, gets a SIGSTOP and a SIGCONT from the freeze, and no kill. The model has no such group.

It leaves out: a second destroy or a second SIGTERM (the SIGTERM of a create that gives up is the model's one SIGTERM), a SIGTERM before the host registers its handler (a crash covers it), a destroy RPC that fails for a reason other than an unreachable host (it writes nothing), gc --stale-only and --older-than (they only skip more), gc --dry-run (the other command covers its reconcile), the rm in create's error path and in doctor, the Home registry, the socket directory (removeSocketDirectoryIfEmpty and the host's listen retry), the artifact commands (snapshot, screenshot, record export, see the next paragraph), the contents of the event log and of the renderer, a program that exits before the capture read its token (its record has none), a destroy inside the program's session that starts after the program's leader ended or that dies before its check, the time between SIGHUP and the kill timer and the length of every wait (the model has no clock), and the socket liveness probe in rpcServer.listen. A pass covers the model, not the whole product.

The artifact commands never create the session folder (coder/agent-tty#198). ensureArtifactsDir creates only artifacts/ in an existing session folder and reports SESSION_NOT_FOUND when gc removed it, and their file writes create no folder. Unit tests remove the folder before ensureArtifactsDir, the artifact manifest write, the snapshot write, the screenshot write and its rename, and the video copy. The asciicast write uses the same write as the snapshot, and its unit test checks only its createParentFolders: false option.

Coverage record

The sync commit is the last commit that changed coverage.json. check.sh prints it, and git log -1 --format=%h -- .agents/skills/verify-session-lifecycle/coverage.json shows it too. In that commit, someone read the covered code above and confirmed that the model describes it. coverage.json holds the value of each guard and status set that scripts/facts.mjs read, the hash of each covered function, of the model and of the two check scripts, and the list of call sites at that commit. The check compares them with the code on every run. The guards come from the source text with its comments, and the hashes leave comments out. So a new comment inside a guarded block can turn a guard FALSE while every hash stays the same, and the check then prints fact <guard> changed: was true, now false.

Change coverage.json (with check.sh --update-coverage) only in the same commit as a confirmed model, or after you have confirmed that the model still describes the changed code. Because the sync commit comes from git, a squash merge keeps it correct.

Files

• model/SessionLifecycle.tla: the model and the rules.
• model/statechart-view.mjs: plain-word labels for /statechart.
• scripts/check.sh: the one command.
• scripts/facts.mjs: reads the guards, the policy sets, the hashes and the call sites from the code.
• scripts/replay-hold.mjs: holds one file-system call to replay a trace against the real CLI.
• coverage.json: the sync record that check.sh compares with.