# Proof audit, pass 1

Findings first:

1. **The required current-revision runtime proof is missing.** The description of [#32524](https://git.cafe/pingdotgg/t3code/pull/32524) records before at [e455200077](https://git.cafe/pingdotgg/t3code/commit/e455200077ce60806a01c8f28435b58860dcfc74) and after at [d630aded41](https://git.cafe/pingdotgg/t3code/commit/d630aded41). The reviewed head is [120c6e82b7](https://git.cafe/pingdotgg/t3code/commit/120c6e82b7afca3cbdafbd3b54ba2837edc8799b), and its current merge-base with origin/main is [d313b2aff3](https://git.cafe/pingdotgg/t3code/commit/d313b2aff31991ab94c8ac80cdc38a54dd575604). The later code changes the close arguments from a whole-thread close to individual host/device closes and moves the state check inside that loop. The old transcript remains useful historical evidence, but proves no runtime row at the current head. Re-run F1 before at the current merge-base and after at the reviewed head.
2. **The newly introduced decision branches have adequate focused unit coverage.** At the reviewed head I ran all 38 tests in ThreadSettlementService.test.ts successfully, plus the 11 selected tests in DeviceService.test.ts under `agent session release on close`. Those cover the per-device arguments, empty sessions, release failure isolation, re-engagement, existing close semantics and retryable SSH session state. Do not require real-device race injection or separate UI captures for those branches.
3. **Keep the claim precise.** On a Simlock host, another thread could open the same leased device before this fix too, as the PR description acknowledges. Its B-open line does not prove that a local agent-device claim was blocked before and unblocked after. F1 proves actual server cleanup and session removal; the existing DeviceService tests prove the local agent-session release protocol, isolation and no shutdown. A failed release can leave that session held, with a warning; this change promises to continue with other devices and the settle script, not automatic recovery of the failed device.

This is a proof audit, not a new implementation or a full merge-readiness review. No worktree files, PR state or comments were changed. No server or device lease was started. Only the report is uploaded; raw forge responses remain local. Runtime model identifiers and credentials are omitted.

## Scope and paths derived from the code

The complete PR diff against origin/main has two files, 22 production lines and 160 test lines added. The local branch named main is stale; comparing against it would incorrectly include unrelated changes. The forge's base and origin/main agree on the merge-base above.

Production references at the reviewed head:

- [ThreadSettlementService.ts](https://git.cafe/pingdotgg/t3code/blob/120c6e82b7afca3cbdafbd3b54ba2837edc8799b/apps/server/src/orchestration-v2/ThreadSettlementService.ts#L602): only `processEvent(thread.settled)` calls `cleanUpSettledThread`. The activated domain-event stream processes cleanup serially. Initial startup and later sweeps decide new settlements; startup does not replay cleanup for every already-settled thread.
- [Orchestrator.ts](https://git.cafe/pingdotgg/t3code/blob/120c6e82b7afca3cbdafbd3b54ba2837edc8799b/apps/server/src/orchestration-v2/Orchestrator.ts#L13489): `thread.auto-settle` checks its snapshot and becomes the ordinary settle mutation, which emits `thread.settled`.
- [ThreadManagementService.ts](https://git.cafe/pingdotgg/t3code/blob/120c6e82b7afca3cbdafbd3b54ba2837edc8799b/apps/server/src/orchestration-v2/ThreadManagementService.ts#L1118): an agent settling another/idle thread dispatches settle immediately; its own active thread waits for run completion, then dispatches guarded settle. [The MCP organize handler](https://git.cafe/pingdotgg/t3code/blob/120c6e82b7afca3cbdafbd3b54ba2837edc8799b/apps/server/src/mcp/toolkits/thread/handlers.ts#L335) uses this service.
- [ws.ts](https://git.cafe/pingdotgg/t3code/blob/120c6e82b7afca3cbdafbd3b54ba2837edc8799b/apps/server/src/ws.ts#L2054): manual client commands enter the same orchestrator. Web, desktop and mobile therefore share this cleanup. No UI, provider adapter, wire contract or client-origin branch is changed. Local and remotely connected clients execute it in the device-owning server environment. Archive/delete do not call this cleanup.
- [DeviceService.ts](https://git.cafe/pingdotgg/t3code/blob/120c6e82b7afca3cbdafbd3b54ba2837edc8799b/apps/server/src/device/DeviceService.ts#L899): close selects by thread plus explicit host and device, acquires its lifecycle lock, releases the agent session when the host supports it, and publishes removal. `shutdown` is omitted, so peer sessions and device power are retained. An unavailable SSH host returns an error and retains its session for retry. Pool host leases can be shared independently of these per-thread sessions.
- [server.ts](https://git.cafe/pingdotgg/t3code/blob/120c6e82b7afca3cbdafbd3b54ba2837edc8799b/apps/server/src/server.ts#L586): the existing worker now requires the same DeviceService supplied in the server's shared runtime dependencies. A real RPC transcript is the proof that mocks cannot supply for that assembled runtime.

Changed input dimensions are the current `settledOverride`; the thread-filtered session array (empty, one, multiple); each `(hostId, deviceId)` pair; close success/error; and state changes while terminal/device cleanup yields. Session platform and openedAt are not read by this new loop. Android/iOS, physical/simulator, local/SSH/Simlock affect the existing device adapter, not settlement's branch logic. Exact thread/host/device selection prevents other threads and same-named devices on another host being selected.

Order and conditions: read current thread → stop unless settled → close terminals → snapshot sessions → sequentially re-read thread before each close → skip if re-engaged, otherwise close and log any typed close error → inspect original worktree path → stop for null/missing path → re-read current thread → stop if re-engaged → require a valid settledAt and no previous successful script start for that timestamp → start settle script and detach its completion. A failed script start permits a later re-emitted settlement to retry. Device close is not gated by worktree existence or script deduplication. A release already in flight is allowed to finish after re-engagement; subsequent releases are skipped. No automatic device reopen is added on unsettle.

Unexpected projection/filesystem/terminal failures and defects reach the cleanup's outer warning handler; interruption remains interruption. The per-device catch applies to `devices.close`, not to the projection read. No new retry policy or guarantee for database failures is claimed. The existing bot suggestion about transient projection read retries is outside the release-error guarantee, rather than proof that ordinary device errors stop the loop.

## Fixture matrix

All named settlement tests below are in [ThreadSettlementService.test.ts](https://git.cafe/pingdotgg/t3code/blob/120c6e82b7afca3cbdafbd3b54ba2837edc8799b/apps/server/src/orchestration-v2/ThreadSettlementService.test.ts). Device tests are in [DeviceService.test.ts](https://git.cafe/pingdotgg/t3code/blob/120c6e82b7afca3cbdafbd3b54ba2837edc8799b/apps/server/src/device/DeviceService.test.ts). COVERED means enough proof for this small change; it does not mean a live transcript exists for that row. Composed proof explicitly combines the loop test with existing close-service tests.

| ID / fixture | Data and observable outcome | Diff affected? | Unit proof (exact test names) | Real-server seed / evidence form | Existing transcript and status |
| --- | --- | --- | --- | --- | --- |
| F1 Healthy single-device settle | Idle A owns one healthy device session; no worktree. Settle A; A's session disappears, device stays booted, B can open it. | Yes: real dependency, event consumption and exact close call. | `releases a settled thread's devices without shutting them down` proves the selected close arguments and omission of shutdown; mocks cannot prove the assembled server actually invokes the real service. | **Required transcript.** Isolated server at merge-base, then head; same RPC driver creates project/A/B, configures one Simlock host, opens a leased Pixel 9 for A, observes its session, dispatches `thread.settle`, awaits stored `thread.settled` and cleanup completion/device-state update, lists sessions and boot state, opens B. Use a pool lease per device-pool skill; no live userdata. | Old before retains A and has zero close child spans; old after removes A and opens B. Historical F1 support only: wrong before revision and after predates this loop. **MISSING current merge-base/head pair.** |
| F2 Empty sessions | Settled A has `sessions=[]`, valid own worktree and configured settle action. No device close/lifecycle lock; script still starts. | Yes: empty iteration bypasses close. | `leaves the device service alone for a settled thread without devices`. | RPC-create A without opening a device; valid fixture worktree and a settle script that emits a marker; settle and inspect script start/marker. Not necessary to block a real host startup: avoiding close is what avoids its lock. | No old capture. **COVERED by unit**; no new runtime required. |
| F3 Several healthy devices | A has two distinct `(hostId, deviceId)` sessions. Both selected and released, with per-device state reads. | Yes: loop rather than whole-thread close. | Composed proof: `releases the other devices and runs the settle script when one release fails` asserts two exact close calls and successful second iteration; F1's test covers success; DeviceService's `releases only the caller's session, keeps the device booted, and is idempotent` covers successful removal. There is no dedicated two-success settlement assertion. | Can lease two devices through the pool, open both over RPC and settle A; record both sessions disappearing. This is an optional extension of F1, not a second mandatory capture. Host/device matching is determined by the explicit close arguments, not device display names. | No old multi-device evidence. **COVERED by composed unit proof.** |
| F4 Earlier release fails | A has unreachable SSH device first, healthy device second, valid worktree. Failure is logged; second release and settle script proceed; failed session may remain. | Yes: per-device catch and continuation. | `releases the other devices and runs the settle script when one release fails`; DeviceService's `retains an SSH record during reconnect and releases it on retry`. | Possible only with a dedicated controllable SSH host plus another leased device. Open both via RPC, disconnect only the fixture host, settle and record remaining failed session, removed healthy session, warning and script marker. Plain pool sessions cannot model SSH reconnect. Deterministic error injection is already covered by the named unit. | Not in old transcript. **COVERED by unit**; no forced host outage required. |
| F5 Re-engaged before cleanup starts | Event payload says settled; current projection is active (or has no settled override). No terminal/device cleanup. | Existing guard protects the new calls. | `keeps the terminals of a thread re-engaged before the event ran` checks terminal skip; device skip follows the earlier return. | Settle then unsettle over RPC is possible but cannot reliably order the event consumer without an internal barrier. Use the named unit's current projection/event fixture. | Not in old transcript. **COVERED by unit and guard placement.** |
| F6 Re-engaged during terminal close | A starts settled, becomes active while terminal cleanup yields; devices are retained and no settle script starts. | Yes: recheck before first device. | `skips the settle script for a thread re-engaged while its shells close` has the added explicit zero-device-close assertion. | Real RPC terminal/settle/unsettle commands can exercise it probabilistically, but no public RPC gates terminal close at the needed point. Named unit controls the exact milestone. | Not in old transcript. **COVERED by unit.** |
| F7 Re-engaged during first device release | Two A sessions; first close is held, A becomes active, first completes; second is retained. | Yes: per-iteration state check. | `keeps the remaining devices of a thread re-engaged during an earlier release` uses Deferred barriers and asserts only the first close. | Ordinary pool/RPC calls cannot deterministically hold an in-flight release at its internal boundary. A controlled host could, but the named unit is the correct proof. Do not require a real paid agent turn. | Earlier whole-thread close could not demonstrate this. **COVERED by unit.** |
| F8 Valid own worktree | Settled A with an existing own worktree and valid settledAt. Device cleanup precedes script execution in that worktree. | New device work runs before unchanged script path. | `runs the settle script in the thread's own worktree`; F4 additionally proves a device close failure does not prevent the script. | RPC-create A in a prepared fixture worktree with a settle script marker; open a leased device if extending F1; settle and inspect marker. | No script evidence in old transcript. **COVERED by unit.** |
| F9 Missing worktree | A's non-null worktree path no longer exists. Devices still reach release, script skips. Null/shared-checkout path is already F1. | New release sits before unchanged filesystem gate. | `runs the settle script in the thread's own worktree` includes shared, missing and valid paths and asserts only the valid script runs. F1 proves release with a null worktree; code order establishes release before the missing-path gate. | RPC-create A referring to a disposable fixture worktree, remove only that fixture directory before settle, optionally open a leased device. Not necessary for a second runtime capture. | No worktree shape stated in old transcript. **COVERED by existing worktree test plus code order.** |
| F10 Repeated settlement / script retry | Same settledAt emitted twice: script starts once. If first script start fails, a later emission retries. Device closes can be repeated safely. Null/invalid settledAt also skips script after device cleanup. | Device loop precedes existing timestamp/deduplication checks; existing script decisions unchanged. | `runs the settle script once when a settlement is re-emitted`; `retries the settle script on a re-emitted settlement after a failed start`; DeviceService's idempotence test. Null/invalid settledAt guard inspected, no dedicated test in this file. | Re-dispatch settle with a fresh command id for the same settled thread; count script markers. Configure a failing first script launch only in a fixture if needed. Cannot seed invalid typed persisted state through supported RPC; no corrupted-DB fixture required for unchanged script guard. | Not in old transcript. **COVERED for affected behavior; unchanged invalid-data guard inspected.** |
| F11 Settlement origins | Manual; auto after inactivity/PR completion; agent settling idle/other thread; own active agent defers until run completes. Every successful mutation emits the same event. | New cleanup consumes all origins, no origin switch. | Settlement tests `skips settings and PR decisions for recent branchless threads`, `settles a merged pull request stored only in the thread links`, `reevaluates immediately after a pull request merge` cover automatic dispatch. All cleanup cases inject `thread.settled`. Separate existing runtimeLayer test `settles a thread its own agent settled once the turn completes` was inspected, not run. | Manual RPC in F1 is sufficient real runtime proof after tracing convergence. Auto can use aged fixture activity or a controlled merge and settings. Agent deferral cannot be invoked faithfully by sending `thread.settle` alone; use the existing service/runtime test, not a fake claim that raw RPC reproduces the MCP caller context. | Old transcript is manual only. **COVERED by path convergence and named tests**; no separate device capture per client, provider or settlement origin. |
| F12 Local claim and peer isolation | A and another thread have records for the same device. Close A without shutdown: only A's agent-session close is sent, peer remains, device stays booted; missing session/idempotent retry tolerated. Simlock shared host lease stays open. | Existing close behavior invoked by new code. | DeviceService tests `releases only the caller's session, keeps the device booted, and is idempotent`, `accepts a missing agent session, shutdown=%s`; existing `leaves a session its host leases to every thread open when one thread closes` was inspected, not run in the selected group. | Pool-leased F1 proves session cleanup but cannot reproduce exclusive local daemon ownership. Exact local before/after claim contention requires a dedicated local/SSH agent-device host; not achievable by merely adding another thread to the same shared pool lease. Existing protocol tests are sufficient for this unchanged boundary. | B opening in the old after capture is compatible with both before and after on Simlock, so it does not prove exclusive claim transfer. **COVERED by existing device boundary tests; limitation disclosed.** |

## Minimal new capture contract

Only F1 needs new evidence. One driver against both revisions is enough; the optional two-device variant also strengthens F3. The output must identify the actual source commits, use isolated data, record its RPC commands and observed results, show the committed settle event, and confirm cleanup completed rather than inferring it from the command receipt. Before: A remains listed once cleanup has finished and no DeviceService.close child span exists. After: A disappears and the successful close span identifies A's host/device; device remains booted; B opens the same device. Subscribe to stored/device events before dispatch so the driver cannot miss the completion. A bounded observation deadline may fail the driver; a fixed sleep alone is not proof of completion.

Use inspect-only `device.list` for passive reads where appropriate so discovery does not itself alter the observed state. Redact auth values, pairing URLs and runtime model identifiers from the published transcript. Close B's fixture session and release the pool lease when finished, without inferring that a non-shutdown thread close returned a shared pool lease. Capture work belongs to the lead's next pass; this read-only audit did not attempt it.

Verification run at the reviewed head: `vp test run apps/server/src/orchestration-v2/ThreadSettlementService.test.ts` — 38 passed. `vp test run apps/server/src/device/DeviceService.test.ts -t 'agent session release on close'` — 11 passed, 52 excluded by name filter. No repo-wide checks. The PR's reported earlier failing-before tests were not independently re-run on the merge-base in this audit. GitCafe metadata/checks/reviews were read; they do not replace runtime evidence.

FRICTION: none

VERDICT: INSUFFICIENT F1 current merge-base/head real-server RPC transcript