verify-ws-connection: server-stop rule row, replay cleanup, Close deadline and reply window #601

Follow-ups for the verify-ws-connection skill (#474). The user chose to merge #474 at head 9547534 and track these items here.

1. Server stop and the disconnect rule. ServerStops in model/WsConnection.tla clears listed without counting a report, so DeadClientDropped holds on its ~serverUp branch while on_disconnect never runs. The model matches the code: stop_server skips on_disconnect on purpose ([FEATURE] Close diff handled by remote control #248). The rule table row in SKILL.md does not say so. Fix: state the server-stop exemption in that row. Codex thread: feat(skills): add verify-ws-connection, a TLA+ model of the WebSocket connection lifecycle #474 (comment)
2. Orphaned child Neovim after a failed replay. When a replay that calls spawn_claude raises before claude.kill(), the child Neovim keeps running its ten-minute vim.wait. Fix: kill every spawned peer on exit of the parent runner and close the process handle. Codex thread: feat(skills): add verify-ws-connection, a TLA+ model of the WebSocket connection lifecycle #474 (comment)
3. Close-frame deadline. The model has no transition for the close_client deadline, which drops the queued Close frame of a Claude that makes no progress for one keepalive window. StatusCloseDelivered is narrowed to a Claude that keeps reading. Fix: model the deadline as a transition. Codex thread: feat(skills): add verify-ws-connection, a TLA+ model of the WebSocket connection lifecycle #474 (comment)
4. Full reply window. NoFalseTimeout covers a Claude that answers each ping before the next tick. A later pong that is within the advertised bound is not modeled. Fix: let pings stay outstanding across ticks in the model. Codex thread: feat(skills): add verify-ws-connection, a TLA+ model of the WebSocket connection lifecycle #474 (comment)

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