feat(skills): add verify-ws-connection, a TLA+ model of the WebSocket connection lifecycle by ThomasK33 · Pull Request #474 · coder/claudecode.nvim

ThomasK33 · 2026-11-10T17:15:32Z

Adds .agents/skills/verify-ws-connection: a TLA+ model of one WebSocket connection between Claude and the plugin, checked with TLC against guards that check.sh reads from the Lua source. It is the second verify-* skill on the shared harness (scripts/tla/check-lib.sh, #450), after verify-diff-lifecycle.

It describes the keepalive as #488 merged it (d63c9b3, with the fix for the fresh clock at the tick). On the code of #479 it reads STALE, and its facts for the new design read FALSE.

What it checks

Six rules, from the TCP accept through the handshake, requests, Close frames, keepalive pings and server stop:

Rule	Plain sentence
`NoRequestAfterEnd`	A request from Claude runs only after its 101 reply was written, and never after the plugin started to close the connection or saw it end.
`DisconnectReportedOnce`	`on_disconnect` runs at most once per client.
`StatusCloseDelivered`	A Close frame for a protocol error (1002, 1003, 1007, 1009) or a server stop (1001) is written before the plugin closes the socket, as long as Claude keeps reading. A Claude whose queue makes no progress for one keepalive window loses the frame to the deadline of `close_client`, which closes the socket (not modeled).
`NoFalseTimeout`	A Claude that answers each ping before the next tick is never dropped by the ping timer, whatever blocks Neovim or sleeps the machine. A tick reads a fresh clock, only pings and stamps the oldest unanswered ping. The check that drops a client runs after a poll that read the sockets, judges nothing when its poll comes more than 1.5 intervals after its tick, and any bytes read from the client clear the stamp. A Claude that stopped once is not covered. A pong that comes later than one interval is not covered either: when a callback blocks inside the poll phase and refreshes the loop time, the poll can miss it, and the check closes that client once its ping is 2.5 intervals old (the verifier's probe on Neovim 0.12.3 dropped a peer that answered 2.4, 1.4 and 0.4 intervals late. Main does the same.) A real Claude answers a ping at once. The rule holds for any limit above `interval * 1.5`, the window in which a check still judges: a limit of 1.2 intervals passes the model, and real Neovim drops a Claude that answered within 100 ms when a read callback blocks about 1.3 intervals in the poll after the tick. The code keeps 2.5.
`DeadClientDropped`	A client whose Claude hung up or stopped answering, or whose connection the plugin started to close, eventually leaves `server.clients` with its `on_disconnect`.
`DroppedSocketCloses`	Once a client left `server.clients`, or the server stopped, its socket eventually closes, as long as Claude reads again.

covered.lock hashes the five files the model describes (server/client.lua, tcp.lua, handshake.lua, server/init.lua, init.lua) and the blocks inside them, so a change there reads STALE until someone confirms the model still fits. The model describes the keepalive judgement only. The stall rule of #467 (judge_stall) and the deadline of a Close frame are not modeled, and SKILL.md says what a user sees for each.

Bugs this model found

Its first run broke three rules on the code as it was. Each one was replayed with real sockets and fixed in #455. Reviews of this PR then found four more false timeouts that the first model could not see. #479 and #488 (three rounds of it) fixed them:

NoFalseTimeout: a main loop blocked during the handshake got a Claude that answers every ping dropped with 1011 before any ping reached it. Since fix(server): judge a silent Claude only after reading its socket #488 a client has no stamp until a tick pings it, so no block can time it out.
DeadClientDropped: after a protocol error while Claude's window was full, the client stayed in server.clients (and is_claude_connected() stayed true) until Claude read again.
DroppedSocketCloses: a stop between Claude's Close frame and the scheduled on_close left the plugin's socket in CLOSE_WAIT.
NoFalseTimeout, again (fix(server): do not drop a live Claude on a late keepalive tick #479): a tick that Neovim ran late after a block of 1.0 to 1.5 intervals can run before the plugin reads Claude's pong, and found the last pong 2.3 intervals old. libuv runs timers before it reads sockets: with libuv 1.44, which Neovim 0.8 bundles, after a block in any callback, and with newer libuv after a block in a check or I/O callback, not after one in vim.schedule or a timer callback.
NoFalseTimeout, a third time (fix(server): judge a silent Claude only after reading its socket #488): libuv 1.44 runs the timers at the end of a pass of the main loop and again at the start of the next, with Neovim's vim.schedule callbacks between. Two ticks ran with no read between them, and fix(server): do not drop a live Claude on a late keepalive tick #479 dropped a Claude that answered every ping. No counter of ticks fixes that, so a tick now only pings and a libuv check handle, which runs after the poll, does the dropping.
NoFalseTimeout, a fourth time (the review of fix(server): judge a silent Claude only after reading its socket #488): the check ran on a poll that did not reach Claude's answer. A pong waits behind more unread data than the socket holds (any bytes from the client now clear the stamp), or the machine sleeps between a tick and its poll (the check judges nothing after a block longer than 1.5 intervals). Each of the two guards alone leaves one path open. The model has both, and a replay for each.
NoFalseTimeout, a fifth time (Codex's review of fix(server): judge a silent Claude only after reading its socket #488): the tick read vim.loop.now() before it called update_time(). libuv runs all timers of a pass with the loop time of the start of the pass, so after a sleep or a block of more than 1.5 intervals in an earlier timer callback of the same pass the tick saw no gap, kept the old stamps, and the check dropped a Claude that had no time to answer. The tick now updates the loop time first. There is no replay for it (a replay cannot make a timer callback run before the ping timer inside one pass), so the unit test of fix(server): judge a silent Claude only after reading its socket #488 and the model pin it: with ClockFreshAtTick off, NoFalseTimeout breaks.

The model in this PR describes the fixed code (18 guards, all read TRUE).

Round 7 (the one extra review round that the maintainer allowed)

This push carries the prepared fixes for the last findings of the two verifiers of 77bb6e2, and merges of main. The model (model/) and the EXPECT map are the same as in 77bb6e2.

The limit that the promise holds for. NoFalseTimeout holds for any limit above interval * 1.5, not for one interval or more. A limit of 1.2 intervals passes the model, and real Neovim drops a Claude that answered within 100 ms when a read callback blocks about 1.3 intervals in the poll after the tick. SKILL.md says so now. The code keeps 2.5.
Which test catches which clock mutation. SKILL.md named the wrong test for one of them. Deleting update_time(), or moving it after local elapsed without reading now again, turns red only "ages a ping from when it was sent...". Moving it after the wake test and reading now again turns red only "takes a tick for a wake...". I ran both mutations.
The README and the comment of start_ping_timer say that the first check that finds the oldest unanswered ping interval * 2.5 old closes a silent Claude, and that a block inside the poll phase refreshes the loop time.
check.sh: the record pattern lists write(client, and handle:close(), so a change to one of those lines reads STALE. The DispatchGuard fact needs the end of its if right after on_message. The StopWaitsForCloseWrite fact rejects release_socket, abandon_close_frame and drop_client in stop_server. Five wording fixes in SKILL.md, and a note that the sleep case of the bytes-only contrast on Neovim 0.8.3 depends on timing.
Merges of main (the last one is fix(diff): save a line the user types into a CRLF proposal with CRLF #577). The server README keeps this PR's keepalive paragraph and takes main's new bullets. After the first two merges three locks read STALE and are recorded again: verify-diff-lifecycle and verify-mention-queue (the hash of tcp.lua, which differs from main only in the comment of start_ping_timer), and verify-ws-connection (tcp.lua, and M.start and M.stop in server/init.lua, where main's fix(server): log Authenticated after the token check and run git once per lookup #539 changed a log line in on_open and fix(diff): answer every openDiff call that is open when Neovim exits #558 answers in-flight requests before stop_server). The second merge made the ws lock stale once more: main's fix(queue): keep the readiness wait for a send with broadcast debouncing off #541 changed M._broadcast_at_mention in init.lua, which the model does not cover, and the covered blocks have the same hashes. The model still fits: those answers are ordinary writes to a connected client, the case the model has. The last two merges (fix(terminal): keep a native start single when an autocmd interrupts it #544 and fix(diff): save a line the user types into a CRLF proposal with CRLF #577, terminal and diff files only) needed no new record.

What changed since the first version of this PR

The model follows fix(server): judge a silent Claude only after reading its socket #488: the facts DropsOnSecondOverdueTick, AliveTickClearsOverdue, PongResetsAge, WakeResetsPong and UpgradeStartsKeepalive are gone. JudgesAfterRead, ClockFreshAtTick, StampKeepsOldestPing, BytesClearStamp, GapSkip and WakeClearsStamp replace them. The environment steps are StaleLoopTime, PollMissesPong and SleepInWindow. A stale tick (an earlier callback of the pass blocked or slept) is a wake that only a tick with a fresh clock sees.
NoFalseTimeout no longer counts awake time. The first model added one tick of awake time on a late tick, so its own sentence ("a block does not count as awake time") was false, and a drop at a late tick while a pong waited unread passed. The rule now asks whether a Claude that never stopped answering was dropped, and the ticks run at any point between reads. A variant that judges at the tick (JudgesAfterRead off) breaks it in 12 states.
The text of SKILL.md is fixed: the libuv wording, the timings, the exit codes of --hash-only, the numbering of the update steps, the order of the /statechart steps (the kept directory is deleted after the view is handed over), the sentence about --mutants (RejectClosesSocket is caught only together with UnlistedDisconnectReleases), and each item that is not modeled now says what a user sees. That includes a client that sends bytes and never reads (fix(server): drop a client that answers pings but never reads #467 handles that stall) and a client that writes data but never answers a ping, which fix(server): judge a silent Claude only after reading its socket #488 keeps by design.

What this PR changes outside the skill

server/README.md and the comment of start_ping_timer described the silent close and the promise wrongly. A silent Claude is closed by the first check that finds its oldest unanswered ping interval * 2.5 old: 90 s after the ping when ticks come on time. One late tick delays it, because a late tick moves the ticks after it back. Two late ticks in a row, or a poll that a block delays after a tick, bring it as early as 75 s (2.6 intervals in the probes, never earlier). A tick more than interval * 1.5 after the tick before it is a wake and restarts the count, so a block of more than half an interval just before a tick is enough, not only one of 1.5 intervals. The promise of no false close is now for a Claude that answers each ping before the next tick, as the model checks it, and the README says what a pong later than one interval costs under a block in the poll phase.
A comment in connection_lifecycle_spec.lua still named the pong rule and pong_overdue, which fix(server): judge a silent Claude only after reading its socket #488 removed. It names the keepalive and the stall rule now.
The comment-only edits to client.lua, tcp.lua and the spec that this PR carried for the design of fix(server): do not drop a live Claude on a late keepalive tick #479 are gone, because fix(server): judge a silent Claude only after reading its socket #488 replaced that code.
DEVELOPMENT.md: the two paragraphs about covered.lock name every verify-* lock, not only that of verify-diff-lifecycle (unchanged in this push).

Proof

check.sh on this branch (checked on the head before the last merge): all 18 facts TRUE and RESULT: PASS. main 262,285 states, live-NoFalseTimeout 256,264, live-DeadClientDropped 11,701, live-DroppedSocketCloses 11,701. It took 256 s and 271 s in two runs at a host load average of 14 to 40, and 2 to 6 min in other runs. The check.sh of the other four skills (verify-diff-lifecycle, verify-mention-queue, verify-selection-tracking, verify-terminal-lifecycle) all pass too, and all five locks match the code (--hash-only).
check.sh --mutants (one TLC worker): I ran it uninterrupted on the head of this push, before the last three merges of main (they change no covered block of this skill): 18 rows, every guard caught, exit 0, 5,753 s at a load average of 14 to 40. Both verifiers of 77bb6e2 had run it uninterrupted too (Opus: 4761 s, gpt: 4814 s, 18 rows each). git diff 77bb6e2 HEAD -- .agents/skills/verify-ws-connection/model is empty and the EXPECT map is the same in all three runs. The new and changed guards are caught by NoFalseTimeout (JudgesAfterRead, ClockFreshAtTick, BytesClearStamp, GapSkip, WakeClearsStamp) and DeadClientDropped (KeepaliveReaps, StampKeepsOldestPing). RejectClosesSocket alone is caught by no rule, because _disconnect_client also closes the socket of a client that left the server, so it is removed together with UnlistedDisconnectReleases.
A design check outside check.sh for the fresh clock: with the ClockFreshAtTick fact forced FALSE, main passes (264,485 states) and live-NoFalseTimeout breaks. So the fact is needed, and the model shows why.
A design check outside check.sh: with a clear of the stamp on a PONG only, in place of the any-bytes clear (the design before the any-bytes rule of fix(server): judge a silent Claude only after reading its socket #488), NoFalseTimeout breaks through PollAndCheckPartial, the poll that reads only the first frame. So BytesClearStamp is needed, and the model shows why. The verifier's run of that variant found 83,746 states. The count depends on how the variant is cut, so I give no count of my own.
Fact fidelity: both verifiers removed each guard in the Lua and every one of the 18 facts flipped to FALSE (26 direct removals in Opus's run). Eight mutants that no fact saw now flip one: five in tcp.lua (no table.insert(pinged, client), no ping sent, judge_silence called at the tick, fn run at once in after_next_poll, the end of the gap if moved above the call), and three guard moves from the last round (the end of the DispatchGuard if above on_message, and abandon_close_frame with release_socket, or drop_client, in the stop_server loop). I reran the verifier's 42 mutations on the new check.sh: none is blind.
scripts/tla/test-check-lib.sh: COUNT cases=44 failed=0 skipped=0.
Replays (real Neovim, real sockets), run again on the head before the last three merges of main, on Neovim 0.12.3 and on 0.8.3: gap-during-handshake 3 of 3, short-block-after-ping 3 of 3, two-blocks-before-read 3 of 3, blocks-before-the-poll 3 of 3, protocol-close-window-full 5 of 5, stop-before-on-close 4 of 4. protocol-close-window-full.lua changed for the merged code: it uses an interval of 500 ms and checks the open socket after half a keepalive window, because the deadline of close_client (merged on main since the replay was written) closes a socket whose Close frame makes no progress for one window, so it no longer stays open for ever while Claude does not read. The first three of the older replays keep 1 of 3, 3 of 5 and 2 of 4 on main before fix(server): drop dead clients promptly and never time out a live Claude #455 (3d4332c). short-block-after-ping keeps 2 of 3 on main before fix(server): do not drop a live Claude on a late keepalive tick #479 (b65d266). two-blocks-before-read keeps 1 of 3 on the code of fix(server): do not drop a live Claude on a late keepalive tick #479 on Neovim 0.8.3. blocks-before-the-poll keeps 0 of 3 on the first push of fix(server): judge a silent Claude only after reading its socket #488 (f3576ea) and with no clear of the stamp at all. With the gap skip and a clear on a PONG only it keeps big-message and sleep and breaks two-blocks. With the any-bytes clear and no gap skip it keeps big-message and two-blocks and breaks sleep. All on both Neovim versions. Both verifiers reproduced the contrast numbers of the other replays. The sleep run of the bytes-only build on Neovim 0.8.3 depends on timing: it kept all three once and two of three in five repeats. The last two replays run Claude in a second Neovim, because an in-process Claude answers only when the blocked loop runs again.
The full busted suite with CI's flags (--coverage -v --shuffle) on this branch: seeds 424242 and 9 on the head before the last two merges of main, each 1858 successes, 0 failures, 34 pending. Seed 424242 on a929777 (merged with main at fix(terminal): keep a native start single when an autocmd interrupts it #544) 1887 successes, 0 failures, 34 pending. The last merge (fix(diff): save a line the user types into a CRLF proposal with CRLF #577, diff.lua and its spec) I did not run again as a whole suite. luacheck (with --no-unused-args --no-max-line-length) reports 0 warnings in 196 files. treefmt (stylua, prettier, shfmt, shellcheck) reports no change on the 16 files this PR touches. Every covered.lock matches the code (--hash-only) on the head of this push, and the full check.sh of verify-diff-lifecycle and verify-terminal-lifecycle pass on a929777.

Run it

.agents/skills/verify-ws-connection/check.sh              # 2 to 6 min
.agents/skills/verify-ws-connection/check.sh --mutants    # about 80 min at a load average of 14, after you edit the model or a fact
.agents/skills/verify-ws-connection/check.sh --hash-only  # no TLC: compares covered.lock with the code
NVIM=/path/to/nvim .agents/skills/verify-ws-connection/replays/run.sh blocks-before-the-poll.lua

CI's covered-lock job already runs every .agents/skills/verify-*/check.sh. SKILL.md has the rules, how to read a result, how to update the model, and its bounds.

Generated with xum • Model: anthropic:claude-sonnet-5-5 • Thinking: xhigh

… connection lifecycle (prep)

ThomasK33 · 2026-11-10T17:15:39Z

@codex review

ThomasK33 · 2026-11-10T17:15:42Z

@codex security review

chatgpt-codex-connector · 2026-11-10T17:15:58Z

Codex Review Summary: ✅ Completed

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

Review	Status	Commit	Review trigger
📝 Code Review	✅ Completed 2026-11-12T20:43:02.528895Z	`9547534`	Manual request
🔒 Security Review	✅ Completed 2026-11-12T20:40:40.505308Z	`9547534`	Manual request

ℹ️ About Codex in GitHub

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

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

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

chatgpt-codex-connector · 2026-11-10T17:19:02Z

🛡️ Codex Security Review

Security review completed. No security issues were found in this pull request.

Reviewed commit: 431b9c5d36

View security finding report

Only the user who started this review can view the report in Codex.

ℹ️ About Codex security reviews in GitHub

This is an experimental Codex feature. Security reviews are triggered when:

You comment "@codex security review"
A regular code review gets triggered (for example, "@codex review" or when a PR is opened), and you’re opted in so security review runs alongside code review

Once complete, Codex will leave suggestions, or a comment if no findings are found.

chatgpt-codex-connector

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 431b9c5d36

ℹ️ About Codex in GitHub

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

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

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

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

…osts without procfs - run.sh starts a replay with -c and dofile, not -l, which needs Neovim 0.9. Paths pass through the environment. A replay that raises ends the run with cq!. I ran all three replays on Neovim 0.8.3 and 0.12.3. - harness.tcp_state returns nil when /proc/net/tcp is missing, and stop-before-on-close.lua then prints SKIPPED for its kernel-state check instead of raising. The is_closing() check still decides.

…ection

#454 added an on_open callback that the 101 write callback calls once the client is connected, and that only schedules process_mention_queue. It changed process_data, M.start of server/init.lua, _handle_new_connection and M.stop of init.lua (clear_mention_queue after the server stop). None reaches a client's state, its socket, server.clients, the ping timer or the server stop, and every fact still reads TRUE, so the model needs no change.

ThomasK33 · 2026-11-10T18:16:46Z

@codex review

ThomasK33 · 2026-11-10T18:16:49Z

@codex security review

chatgpt-codex-connector · 2026-11-10T18:20:14Z

🛡️ Codex Security Review

Security review completed. No security issues were found in this pull request.

Reviewed commit: 87e2e8fc9c

View security finding report

Only the user who started this review can view the report in Codex.

ℹ️ About Codex security reviews in GitHub

This is an experimental Codex feature. Security reviews are triggered when:

You comment "@codex security review"
A regular code review gets triggered (for example, "@codex review" or when a PR is opened), and you’re opted in so security review runs alongside code review

Once complete, Codex will leave suggestions, or a comment if no findings are found.

chatgpt-codex-connector

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 87e2e8fc9c

ℹ️ About Codex in GitHub

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

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

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

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

…e glob)

…ection

#479 said that libuv runs timers before it reads sockets, which is too general. A tick that Neovim runs late can run before the socket read after any block on Neovim 0.8. On newer Neovim it does so only after a block inside a libuv callback that runs after the poll phase (a check callback), and not after a block in vim.schedule, which reads the socket first (checked on 0.12.3 and 0.8.3). Fix the sentence in the pong_overdue comment, the server README and the unit test, and wrap two lines to 120 columns.

#479 changed the ping timer: the first tick that finds no pong for two intervals pings again and sets client.pong_overdue, and only the second drops the client. The model now has the step the first version could not see. - TimerTicksLate (LateTickAfterPing): a tick delayed by 1.0 to 1.5 intervals, below the wake threshold, with Claude's pong still unread. TickOne takes a mode ("normal", "late" or "wake"). A block does not count as awake time. - The variable overdue is client.pong_overdue. The facts DropsOnSecondOverdueTick and AliveTickClearsOverdue are caught by NoFalseTimeout, which needs two delayed ticks (MaxSleeps = 2). - SKILL.md: the NoFalseTimeout sentence says "second tick in a row", the bug list has a fourth entry (fixed in #479), and the stale "baseline" sentence of --mutants is gone. - New replay short-block-after-ping.lua: a 1.3-interval block in a check callback, right after a ping. BROKEN on b65d266, KEPT on main.

…ection covered.lock files The diff-lifecycle record changes only for client.lua and tcp.lua, whose edits are comments. The ws record also covers the new fail-safe branch of the ping timer that #479 added, which the model now describes.

…ection

ThomasK33 · 2026-11-10T21:42:20Z

@codex review

ThomasK33 · 2026-11-10T21:42:22Z

@codex security review

chatgpt-codex-connector · 2026-11-10T21:45:57Z

🛡️ Codex Security Review

Security review completed. No security issues were found in this pull request.

Reviewed commit: f3b607ba6d

View security finding report

Only the user who started this review can view the report in Codex.

ℹ️ About Codex security reviews in GitHub

This is an experimental Codex feature. Security reviews are triggered when:

You comment "@codex security review"
A regular code review gets triggered (for example, "@codex review" or when a PR is opened), and you’re opted in so security review runs alongside code review

Once complete, Codex will leave suggestions, or a comment if no findings are found.

chatgpt-codex-connector

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: f3b607ba6d

ℹ️ About Codex in GitHub

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

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

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

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

…-view.ts - unit-tests failed its "Check formatting" step: prettier wants TimerTicksLate on two lines in model/statechart-view.ts. - Review finding: is_client_alive needs now - last_pong below two intervals, so a last pong exactly two intervals old is not alive. The loop time has a resolution of 1 ms, and a pong read in the same millisecond as the tick before it makes the second tick after it find exactly that. TimerTicksExact (ExactBoundaryTick) lets that tick find the client overdue. The model has the same 176314 states, so the boundary case adds no new state, and every guard is still caught by --mutants.

ThomasK33 · 2026-11-10T22:08:04Z

@codex review

ThomasK33 · 2026-11-10T22:08:06Z

@codex security review

chatgpt-codex-connector · 2026-11-10T22:11:29Z

Codex Review: Didn't find any major issues. Keep it up!

Reviewed commit: 80cd407552

ℹ️ About Codex in GitHub

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

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

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

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

…osts under a block A silent Claude closes after the first tick that finds its oldest unanswered ping 2.5 intervals old: 90 s on time. A late tick moves the later ticks back, so one late tick delays the close. Two late ticks in a row, or a poll that a block delays after a tick, bring it to 2.5 intervals (2.6 in the probes) at the earliest. A gap of more than 1.5 intervals between two ticks is a wake and restarts the count, so a block of more than half an interval just before a tick is enough, not only one of 1.5 intervals. The promise of no false close is for a Claude that answers each ping before the next tick: a later pong can wait unread behind a callback that blocks inside the poll phase and refreshes the loop time. The diff-lifecycle lock follows the comment.

…t the replay notes NoFalseTimeout is promised for a Claude that answers each ping before the next tick. StatusCloseDelivered names the Close deadline. The clock fix is pinned by two tests, not one. The replay table says which guard each blocks-before-the-poll run needs, which replays use the in-process Claude, and the stall rule, deadline and never-reads items say what a user sees. Five mutants of tcp.lua that no fact saw (no pinged insert, no ping, judge_silence at the tick, fn run at once, the end of the gap if moved up) now flip KeepaliveReaps, JudgesAfterRead or GapSkip. gap-during-handshake no longer says that the 101 write callback starts a keepalive window, and check.sh gives the real run times.

…merging main again The merge changed client.lua (connected_at is set in the 101 write callback, and write reports a write that libuv refuses at once) and init.lua (the mention queue). No guard that the model reads changed: all 18 facts still read TRUE and check.sh passes.

ThomasK33 · 2026-11-11T18:35:31Z

@codex review

ThomasK33 · 2026-11-11T18:35:33Z

@codex security review

chatgpt-codex-connector · 2026-11-11T18:38:23Z

Codex Review: Didn't find any major issues. Nice work!

Reviewed commit: 77bb6e2954

ℹ️ About Codex in GitHub

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

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

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

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

chatgpt-codex-connector · 2026-11-11T18:39:11Z

🛡️ Codex Security Review

Security review completed. No security issues were found in this pull request.

Reviewed commit: 77bb6e2954

View security finding report

Only the user who started this review can view the report in Codex.

ℹ️ About Codex security reviews in GitHub

This is an experimental Codex feature. Security reviews are triggered when:

You comment "@codex security review"
A regular code review gets triggered (for example, "@codex review" or when a PR is opened), and you’re opted in so security review runs alongside code review

Once complete, Codex will leave suggestions, or a comment if no findings are found.

…and tighten three facts NoFalseTimeout holds for any limit above interval * 1.5, the window in which a check still judges, not for one interval or more: a limit of 1.2 passes the model, and real Neovim drops a Claude that answered in 30 to 100 ms when a read callback blocks about 1.3 intervals in the poll after the tick and refreshes the loop time. The clock fix is pinned by two tests with different mutations: deleting update_time or moving it after `local now` turns 'ages a ping' red, and only a move after the wake test with a new read of now turns 'takes a tick for a wake' red. The silent close is by the first check that finds the ping 2.5 intervals old, not after a tick. tcp.lua says that a pong can wait unread when the callback also refreshes the loop time. DispatchGuard now needs the end of its if right after on_message, and StopWaitsForCloseWrite rejects release_socket, abandon_close_frame and drop_client in stop_server: the two guard moves that no fact saw. The record pattern lists write(client, ...) calls and handle:close() lines. SKILL.md fixes the harm cell, the stop_server and wake wording and the not-a-fact sentence. Both covered.lock files follow.

…oll depends on timing

…er#488) ## Result Neovim 0.8 no longer drops a Claude that answers every ping. A block of the main loop, of any length and in any callback, does not close a Claude that writes something within 75 s (`interval * 2.5`) of each ping. A Claude that sends nothing is still closed 3 intervals (90 s by default) after its first unanswered ping, when no block longer than 1.5 intervals gets in the way. **This push also merges main with coder#467** (a client that answers pings but never reads), which rewrote the same ping tick. Its stall rule stays, and both rules hold (see "With coder#467"). ## Problem coder#479 made the ping timer drop a client only at the second tick that finds no pong. On Neovim 0.8 (libuv 1.44.2) that is still a race. `uv_run(UV_RUN_ONCE)` runs timers at the start of a pass and again at the end, after the check handles. Neovim runs `vim.schedule` callbacks between two `uv_run` calls. So a tick at the end of a pass, a block in `vim.schedule`, and a tick at the start of the next pass run with no socket read between them. Claude's pong waits in the socket for both ticks. Trace on main, Neovim 0.8.3, a separate-process Claude that answers every ping at once (interval 200 ms): ``` TICK since_pong=191 overdue=nil ping sent B1: 260 ms block in a check callback TICK since_pong=453 overdue=true timers run again at the end of the pass, pong still unread B2: 260 ms block in vim.schedule on_disconnect(client_1, 1006, "Connection timeout") dropped at the next tick ``` A counter cannot fix this. Any number of ticks can run before a read, so the tick must not judge at all. ## Change - A tick pings each connected client and never drops one. It stamps `client.ping_unanswered_since` with the oldest ping sent since bytes were last read from the client. It calls `vim.loop.update_time()` before it reads the clock for the wake test, the stamp and the gap: libuv caches the loop time when a pass starts and runs the timers of the pass with it, and a timer callback that ran before the tick in the pass can have blocked since, or the machine can have slept in it. A stale time hid a wake in the earlier pushes of this PR (Codex round 3). - Each tick that pinged a client starts a one-shot libuv check handle. libuv runs it after the poll phase that reads the sockets, so every byte that reached a socket before the loop time of the check was read. The check drops a client whose oldest ping is `interval * 2.5` old. - **Any bytes clear the stamp.** The read callback clears it, not only a PONG. A pong can wait behind more unread data than the socket holds (Claude writes while Neovim is blocked, and one poll reads only the first part), so the poll after a block does not always reach the pong. Claude shows it is alive by writing anything. - **The check judges only if its loop time is at most `interval * 1.5` after its tick.** A machine that sleeps between a tick and its poll stops Neovim and Claude together: no bytes arrive, and the ping looks as old as the sleep. A tick treats a gap above 1.5 intervals as a wake. The check now does too, and the next tick starts the count over. A block longer than 1.5 intervals therefore restarts the count. - A wake from sleep (a tick gap above `interval * 1.5`) clears the stamps. - Removed: `client.pong_overdue`, `client.is_client_alive` (its only caller was the old tick), and the reset of `last_pong` in the 101 write callback (a client that no tick pinged has no stamp, so the main loop cannot time it out). - `vim.schedule` is not a safe place to judge: Neovim can run it before the read. The check handle is. ## With coder#467 coder#467 landed on main while this PR was in review. It rewrote the ping tick (a pong rule with a second chance, `pong_overdue`, `is_client_alive`) and added a write-queue stall rule with its own check and idle handles. This branch keeps that rule and puts the keepalive of this PR next to it: - The stall rule is unchanged: a client that answered and whose write queue made no progress at two ticks in a row is closed after the next poll ("Write queue stalled", Close 1011 "Not reading"). The 61 tests of main's lifecycle spec: 56 pass under their names, and 5 were rewritten for the stamp and renamed (the `pong_overdue` second chance, the late-tick tests, and the wake and drain tests that spoke of flags). - "Answered" now means that no ping of the client waited for `interval * 2` (it was "a pong within `interval * 2`"). Only an answered client is judged for a stall. A silent client is closed by the keepalive judgement ("Connection timeout", Close 1011 "Keepalive timeout") at the same tick as before, whatever its write queue shows. - A tick that pinged a client arms **one** check and idle pair (`after_next_poll`, from coder#467) that runs both judgements after the poll. It was one pair for each stalled client. `stop_server` closes it as before. - `pong_overdue` and `is_client_alive` are gone, because the stamp replaces them. The tests that named them are rewritten for the stamp (a silent client with a stalled queue is closed by the keepalive, a late pong does not save a stalled queue, a wake restarts both windows). Three confirmation tests no longer expect "no handle" at a tick without a stall, because a tick that pinged always arms the pair. The wake-threshold test from coder#495 ("a tick 1 ms above the wake threshold") expected no handle after a wake tick for the same reason: it now runs the poll after the tick and checks that the client is kept and `on_disconnect` did not run. Two helper counts changed (`forget_handles`). - A real-socket probe of the stall rule (Claude sends unprompted pongs and never reads, 8 MB queued, interval 300 ms): main and this branch both close it with "Write queue stalled" 2.6 intervals after the message, on Neovim 0.8.3 and 0.12.3. - A client that writes data and reads what the plugin writes, but never answers a ping, is kept. Main closes it 3 intervals after its first ping. ## Behavior - A block of the main loop, of any length and in any callback, does not close a Claude that writes something within `interval * 2.5` of each ping. A tick never closes a client, a check judges only after a poll within `interval * 1.5` of its tick, and any bytes clear the stamp. - **A client that writes data and reads what the plugin writes, but never answers a ping, is no longer closed by the keepalive.** It is alive, and the plugin does not judge what it writes. Main closes it 3 intervals after its first ping. The stall rule of coder#467 still closes it if it stops reading, but only once the kernel's socket buffers are full and libuv's write queue backs up: until then every write completes, and an empty queue counts as progress. So a client that stops reading and keeps sending is closed later than main closed it when it also never answered a ping. The README says so. - A Claude that sends nothing is closed at the first read of its socket after the third tick that follows its first unanswered ping (90 s by default). Main closes it at 2 to 3 intervals after its first ping in the verifier's runs and at 3.0 in mine. - A block delays the close of a silent Claude to the first read after the block ends. A block longer than 1.5 intervals also restarts the count, so a run of such blocks can postpone the close. - The info line `Closed client_<n>: no reply for <s>s` counts from the oldest ping sent since bytes were last read. ## Tests `tests/unit/server/connection_lifecycle_spec.lua` models the loop as libuv runs it: a loop time cached at the start of a pass, a poll that reads the sockets, and check handles that run after it. These fail on the code of coder#479 (main): two late ticks with no read between them (the trace above), 20 late ticks in a row, a silent Claude is dropped only at the first read after its tick, the time counts from the first unanswered ping, and a client that hung up or is closing is not judged. These three fail on the first push of this PR (f3576ea) and pass now: a block of 3 intervals between a tick and its poll judges nothing, a Claude that sends a large message before its pong is not dropped (the poll reads only the first 64 KB, the ping is 2.8 intervals old, and the poll is within the gap), and a client that writes data but never answers a ping is kept. The last two also fail on the gap skip alone. The other new tests guard: a client that writes data and never answers a ping is kept, a pong that waits in the socket when its ping is 3 intervals old, a late tick that finds a silent Claude's ping 2.5 intervals old, a poll 1.4 intervals after its tick that still judges, the stamp aged from the time the ping was sent, a block that restarts the count, a stale cached loop time, and a wake from sleep. `tcp_spec.lua` and `log_lines_spec.lua` follow the new tick/check split. Added after the verifier's mutation run on `68b0b13`: the check judges with the loop time of the poll and not with a time read after a younger callback blocked (a Claude whose pong arrives during that block is kept), a tick takes a wake for a wake although the cached loop time is old (a timer callback before it in the pass blocked for 2 intervals, so the clock shows 3 since the last tick and the cache shows 1), the gap skip at exactly 1.5 intervals (judges) and at 1 ms above it (does not), a drop at exactly 2.5 intervals, the stall judgement does not sit under the gap skip (a stalled client is dropped although every poll comes 1.6 intervals after its tick), and a client whose ping is still inside the window is judged for a stall. **Mutants.** My 16 are each caught by at least one test: no `update_time`; bytes do not clear the stamp; a wake does not clear it; no listed-client guard; no connected guard; limit x2 and /2; stamp overwritten each tick; pinged list empty; the check reads the real time; no gap skip; gap x3 and /3; the stall rule judges a silent client; the stall rule never runs; the dropped client keeps its Close-frame deadline. Of the verifier's 33 mutants of `68b0b13`, nine survived. Six are now killed: `update_time` inside `judge_silence`, the stall judgement under the gap skip, the gap skip at 2.0 intervals, the gap skip with `<` for `<=`, the limit with `>` for `>=`, and `answered` true only for a client with no stamp. Each has a test that fails on it. The seventh, a `tick_time` taken from the cached loop time, is equivalent since the round-3 fix (the tick time is the fresh time of the tick), and I dropped it. Two new mutants of the tick clock are killed: no `update_time`, and `update_time` after the wake test. The two that still survive are the stall judgement running before the keepalive one in the check, and the any-bytes clear after `process_data` instead of before it. The verifier classed both as equivalent. As far as I can tell, the first changes only which reason (`Not reading` or `Connection timeout`) a client gets when both rules apply to it in one poll, and the second matters only if `process_data` raises. **Random order.** The full suite passes with `--shuffle` for seeds 1 to 60 (1439 successes, 16 pending, 0 failures in each of the 60 runs). Before the fix, seeds 9, 15, 40, 57 and 59 failed (the verifier found them on `68b0b13`): the pong of the late-tick tests was built when the file loaded, from a `frame` module that only the outer `before_each` sets (`attempt to index upvalue 'frame'`). It is built in a `before_each` now. ## Replays on real Neovim A separate-process Claude (Python) answers every ping at once. Interval 300 ms. **Block matrix.** Blocks of 0.9, 1.3, 1.45 and 2.2 intervals run one after the other: the first right after a ping, in each of four contexts (a check callback, `vim.schedule`, a timer callback, an I/O read callback on a UDP socket), then the second in each of the four. 64 cases. 12 more cases run 6 blocks that cycle through all four contexts. | | Neovim 0.8.3 (libuv 1.44.2) | Neovim 0.12.3 (libuv 1.52.1) | |---|---|---| | main, 76 block cases | **6 dropped**, 70 kept | 0 dropped, 76 kept | | this PR, 76 block cases | 0 dropped, 76 kept | 0 dropped, 76 kept | | main, random blocks, 16 seeds of 20 s | **2 dropped** (seeds 10, 11) | not run | | this PR, random blocks, 24 seeds of 20 s | 0 dropped | 0 dropped | **The three paths of the verifier's finding, each with the mechanism that covers it.** 4 runs each (idle and prepare callbacks, 2 each), dropped / total: | Probe | first push (f3576ea) | gap skip only | any bytes only | both (this PR) | |---|---|---|---|---| | A block of 2.7 intervals before the poll, Claude writes 300 KB and then its pong during it | 4/4 on 0.8.3 and 0.12.3 | 0/4 | 0/4 | 0/4 | | Claude sleeps with Neovim: it answers the ping 2.7 intervals late | 3/4 | 0/4 | **4/4** | 0/4 | | Two blocks of 1.4 intervals (under the gap) with an older stamp, Claude writes 300 KB and then its pong | 4/4 | **4/4** | 0/4 | 0/4 | Each mechanism is needed: the gap skip alone drops the third row, and any bytes alone drops the second. **A client that writes every 100 ms and never answers a ping:** main drops it 3.0 intervals after its first ping. This PR keeps it (2 of 2 versions), and the stall rule of coder#467 still closes a client that never reads. **A Claude that reads pings and never answers:** dropped 3.0 intervals after its first ping on main and on this PR, on both versions. With 2 blocks of 2 intervals in the way: 8.0 intervals on both. **Re-run after the tick reads a fresh clock (Codex round 3), on the `lua/` code of this push.** Block matrix: 76 kept and 0 dropped on Neovim 0.8.3 and on 0.12.3. Random blocks: 24 seeds of 20 s, 0 dropped on both. The three F1 probes and the residual probe (300 KB and a pong behind a block, a Claude that answers 2.7 intervals late, two blocks of 1.4 intervals): kept on both. A client that writes every 100 ms and never answers: kept on both. A Claude that sends nothing: dropped 3.0 intervals after its first ping on both, and 8.0 with two blocks of 2 intervals. With six blocks of 1.3 intervals through four contexts it is dropped at 11.8 (0.8.3) and 11.9 (0.12.3) intervals, 3 later than before the change: the tick now sees the real gap, takes it for a wake, and restarts the count, as the README says. The scripts are my scratch probes, not repo files. They move into the `verify-ws-connection` replays in coder#474. ## Not in this PR - The TLA+ model in coder#474 follows this change in a separate update. ## Checks `luacheck` (with `--no-unused-args --no-max-line-length`, as CI runs it), `stylua --check`, `prettier --check` on the README, a `luajit` load of every file under `lua/`, the full busted suite (1439 successes, 16 pending, seed 424242 and seeds 1 to 60) on the code of the merge with main at `e5c5ddb` (the newer main commit `b477362` changes only `scripts/`), `verify-diff-lifecycle/check.sh` PASS (full run) and its `covered.lock` re-recorded. --- _Generated with [`xum`](https://github.com/coder/xum) • Model: `anthropic:claude-sonnet-5-5` • Thinking: `xhigh`_

ThomasK33 · 2026-11-12T18:06:21Z

Review-cap waiver (from the maintainer, 2026-11-12): one 7th review round is allowed on this PR: one push with the prepared fixes for the last verifier findings (the SKILL.md limit line and the test attribution) plus a merge of main, and one Codex review of that head. A new Opus verifier checks the head before the merge. Stop condition: a new security flaw, data-loss risk or broken core behavior on that head stops the PR for a new decision.

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

Keep this branch's keepalive paragraph in lua/claudecode/server/README.md and take main's new notification, deferred-response and in-flight bullets. Take main's verify-diff-lifecycle covered.lock and record the three locks that the comment edits of tcp.lua and main's server/init.lua changes (#539 on_open log, #558 in-flight replies in M.stop) made stale: verify-diff-lifecycle, verify-mention-queue and verify-ws-connection. The ws model still fits: the in-flight replies are ordinary writes to a connected client before stop_server.

Record the verify-ws-connection lock: main's #541 changed the file hash of lua/claudecode/init.lua in M._broadcast_at_mention, which the model does not cover. The covered blocks are unchanged.

A clean merge of #544 (terminal files only). Every covered.lock matches the code, so no lock needs a new record.

A clean merge of #577 (diff.lua). Every covered.lock matches the code, so no lock needs a new record.

ThomasK33 · 2026-11-12T20:37:16Z

@codex review

ThomasK33 · 2026-11-12T20:37:18Z

@codex security review

chatgpt-codex-connector · 2026-11-12T20:40:38Z

🛡️ Codex Security Review

Security review completed. No security issues were found in this pull request.

Reviewed commit: 9547534dd3

View security finding report

Only the user who started this review can view the report in Codex.

ℹ️ About Codex security reviews in GitHub

This is an experimental Codex feature. Security reviews are triggered when:

You comment "@codex security review"
A regular code review gets triggered (for example, "@codex review" or when a PR is opened), and you’re opted in so security review runs alongside code review

Once complete, Codex will leave suggestions, or a comment if no findings are found.

chatgpt-codex-connector

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 9547534dd3

ℹ️ About Codex in GitHub

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

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

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

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

ThomasK33 · 2026-11-13T08:47:04Z

Merge waiver (ThomasK33, answered in the run's chat): merge head 9547534 as is. The two open Codex code-review comments from round 7 (the SKILL.md rule table does not exempt a server stop, which skips on_disconnect on purpose; a failed replay can leave a child Neovim running for up to 10 minutes) go into one tracking issue with the WebSocket follow-ups, filed after this PR merges.

Before the enqueue I merged this head with main bcf1f08 locally (not pushed). All five .agents/skills/verify-*/check.sh models pass on that merge result (count pass=5 fail=0).

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

…the owned stop (coder#602) ## Why This is a follow-up to coder#593. It fixes the Snacks close and the stop in `owned.lua`, the two close paths that coder#593 left open. A job that was just started can still be a fork of Neovim until its child has run `exec`. A `jobstop` on it then ends Neovim with `Caught deadly signal 'SIGHUP'`, or the buffer delete after it hangs. coder#593 documents the race, and coder#544 made the native close wait for the exec of a young job. The Snacks close and the stop in `owned.lua` still called `jobstop` at once, so a close within milliseconds of the start could kill Neovim. ## Cause `pty_process_spawn` forks the child, and `init_child()` runs `setsid()` and resets the signal handlers only after that. Until `exec` the child has Neovim's libuv handlers. When the pty master closes in that gap (a `jobstop`), the kernel sends SIGHUP to the child, libuv's handler in the child writes into the signal pipe that it shares with Neovim, and Neovim reads a SIGHUP of its own and exits. With the child held in the gap (see Evidence), a close right after the start killed Neovim in every run for the Snacks provider and for the stop in `owned.lua`, on 0.8.0 and 0.12.3. The native provider survived in every run. ## Fix The wait moves out of `native.lua` into `owned.wait_for_exec(jobid)`, with `owned.is_young(started_at)` for the 10 s rule. The code is the same: it reads the names of Neovim and of the child from `/proc/<pid>/comm` (or `nvim_get_proc` where `/proc` is missing) and waits up to 1 s until the child has another name. - `native.close` calls it for a job younger than 10 s, as before. - `snacks.M.open` records `term._cc.job_started_at` where it already patches the instance. `snacks.close` reads it and calls the wait for a job younger than 10 s. A terminal that a reload adopted has no start time and is not waited for, as in native. Without the age rule, every Snacks close on macOS would pay about 200 ms for the two `ps` calls of the `nvim_get_proc` fallback. - `owned.lua` `stop_buffer` has no start time, so it calls it for every job. That path runs only after a reload or a provider switch, and the wait ends at the first look for a job that has run `exec`. The wait runs scheduled callbacks while the job still runs. Two Codex findings on `ea0fbfd6` were about that, and `12f1d45f` fixes both: - `snacks.close` now clears the owned mark before the wait for every terminal, not only for an adopted one. An `open()` among the callbacks can no longer adopt the terminal that is closing by its mark. - `stop_buffer` reads the channel before the wait and checks `nvim_buf_is_valid(buf)` before `jobstop`. A callback that deleted the buffer during the wait no longer makes `jobstop` raise `Invalid buffer id`. `lua/claudecode/terminal/README.md` and the `verify-terminal-lifecycle` skill describe the three places. The skill changed as follows: - The fact `OwnedStopOtherStops` reads `M.wait_for_exec(channel)` and the buffer check before `jobstop`. - The new fact `SnacksCloseClearsMark` reads the mark clear before the wait. The model has a switch of the same name in `CloseBegin`. The model counts a closing terminal as ended, so the fact breaks a rule only together with `OwnedLiveSkipsEndedJob`. `check.sh --mutants` has a row for the pair. - `OwnedLiveSkipsEndedJob` alone now breaks `OpenShowsLiveClaude`, not `CloseNeverReuses`, because the model clears the mark in every Snacks close. - The model still passes with 279492 distinct states. ## CI on `ea0fbfd6` and the fixes Two checks failed on `ea0fbfd6`. 1. The integration spec compiled its shim into a TMPDIR folder. CI's second pass runs with `TMPDIR="$RUNNER_TEMP/odd tmp 50%"`. `LD_PRELOAD` splits its value at a space or a colon, so the shim was ignored, the child was never held, and the probe timed out. `f910015b` puts the shim into `mktemp -d /tmp/claudecode.XXXXXX` when the TMPDIR path holds a space or a colon. 2. `verify-diff-lifecycle` also hashes `terminal/{native,owned,snacks}.lua`, so its `covered.lock` was stale. `3a1961a0` re-records the locks of `verify-terminal-lifecycle` and `verify-diff-lifecycle`. ## Tests - `tests/integration/terminal_close_young_job_spec.lua` runs one Neovim per case with `-u NONE` (so `minimal_init.lua` does not wait for the exec and hide the race) and `tests/helpers/hold_pty_child.c` preloaded. The shim holds the child inside `init_child()` and creates a file when it does. The probe (`tests/helpers/close_young_job_probe.lua`) starts a Claude terminal job, waits for that file, and closes the job. Cases: a plain `jobstop` as the control (it must end Neovim with SIGHUP, so the other cases can fail), the native close, the Snacks close (with a stand-in for Snacks) and the `owned.lua` stop. The spec is pending without Linux, a C compiler and `timeout`. It puts the shim into a `/tmp` folder when TMPDIR holds a space or a colon, and `tests/helpers/ld_preload_path.lua` makes that choice. - `tests/unit/ld_preload_path_spec.lua` has three cases: a plain path, a path with a space and a path with a colon. Before it, a spec pattern without the colon half passed in every CI configuration. - `tests/unit/terminal/owned_wait_for_exec_spec.lua` covers the wait (names from `/proc`, from `nvim_get_proc`, the 1 s limit, a job with no pid, unreadable names), `is_young`, the order of the stop in `owned.lua` (wait, then `jobstop`, then delete) and "leaves a buffer alone that a callback deleted during the wait". - `tests/unit/terminal/snacks_close_spec.lua` covers the Snacks close: it waits before `jobstop` for a job that just started, not for a job older than 10 s, and not for a job that exited. The case "does not let an open during the wait adopt the terminal that is closing" covers the mark clear. - Five Snacks unit specs gain `vim.loop.hrtime` in their vim mock, and one gains `vim.fn.getpid`, because the provider now reads a clock and the wait reads the pid. - `proof-pty-child-hangup.sh` compiles the same shim instead of a copy of it. Under a TMPDIR with a percent sign it failed all three cases, on `main` too. With only a space or only a colon it failed one of three, and its wrapper case passed only because the shim was not loaded. Now `d6019d13` puts its work folder into `/tmp` for such a path. - The header of `hold_pty_child.c` now says that the shim holds every fork of Neovim that calls `signal(SIGCHLD, SIG_DFL)`, including the `ps` children that `nvim_get_proc` starts, not only the pty child. ## Evidence Builds: the official `v0.8.0` release binary (`NVIM v0.8.0-1210-gd367ed9b2`, as in CI) and Neovim 0.12.3, scratch HOME and XDG dirs, on a shared host. | Run | main plus the new tests | this branch | |---|---|---| | integration spec, 10 runs per build | 10 of 10 fail on both builds (the Snacks and `owned.lua` cases fail, the control and native pass) | 0 of 10 fail on both builds | | integration spec, 20 runs per build, plain TMPDIR | not run | 0 of 20 fail on 0.8.0 and on 0.12.3 | | integration spec, 20 runs per build, `TMPDIR="odd tmp 50%"` | the spec of `ea0fbfd6` times out in this TMPDIR, as in CI | 0 of 20 fail on 0.8.0 and on 0.12.3 | | the unit specs of `tests/unit/terminal` plus `native_terminal_toggle_spec`, 20 runs | not run | 0 of 20 fail (374 successes each) | Mutants of the Lua files, one run each, on `89e74e31`. The merge of main changed no terminal file and no terminal spec, so I did not rerun them on the merge commit. "Unit" counts the failing tests among 374 in `tests/unit/terminal` plus `native_terminal_toggle_spec`. "Integration" is the new spec on 0.8.0 and 0.12.3, with the same result on both. "Fact" is the `verify-terminal-lifecycle` fact that turns FALSE in a facts-only run of `check.sh`. | Mutant | Unit | Integration | Fact | |---|---|---|---| | Snacks close does not wait | 2 failures | red | `SnacksCloseClearsMark` | | Snacks close always waits (no age rule) | 1 failure | green (the wait is harmless but slow) | none | | Snacks close never waits (age rule always false) | 2 failures | red | none | | Snacks does not record the start time | 2 failures | red | none | | Snacks clears the mark only for an adopted terminal (the form on `ea0fbfd6`) | 1 error (the open adopts the closing terminal) | green | `SnacksCloseClearsMark` | | Snacks clears the mark after the wait | 1 error (same case) | green | `SnacksCloseClearsMark` | | `stop_buffer` does not wait | 2 failures | red | `OwnedStopOtherStops` | | `stop_buffer` has no `nvim_buf_is_valid(buf)` check before `jobstop` | 1 failure | green | `OwnedStopOtherStops` | | `stop_buffer` re-reads the channel with no check (the form on `ea0fbfd6`) | 1 failure | green | `OwnedStopOtherStops` | | native close does not wait | 3 failures | red | none | | native close never counts a job as young | 3 failures | red | none | | `wait_for_exec` does not call `vim.wait` | 6 failures | red | none | | `wait_for_exec` stops while the names are equal | 4 failures | red | none | | `wait_for_exec` waits 0 ms | 4 failures | red | none | | `wait_for_exec` has no guard for an unreadable name of Neovim | 4 failures | green | none | | `wait_for_exec` calls `jobpid` without `pcall` (no guard for a job without a pid) | 1 failure and 2 errors | green | none | | `is_young` uses `<=` | 2 failures | green | none | | `is_young` reads a `nil` start time as young (no `nil` guard) | 1 failure | green | none | The control mutant (no change) is green in every column, with 374 successes. I ran the facts-only `check.sh` on every row, and "none" means that every fact stayed TRUE. A mutant of `tests/helpers/ld_preload_path.lua` that drops the colon, and one that drops the space, each fail one case of `ld_preload_path_spec.lua`. The model has its own mutants. `check.sh --mutants` removes each guard of the model in turn, and it ends with "every guard is caught" on the merge commit `191a3e24`. The pair `SnacksCloseClearsMark` with `OwnedLiveSkipsEndedJob` is caught by `CloseNeverReuses` and `OpenShowsLiveClaude`. - Gate: `MISE_LOCKFILE=false mise run clean && mise run all` with GNU timeout first on PATH exits 0 with 1925 successes, 0 failures, 0 errors and 38 pending, and luacheck reports 0 warnings in 206 files. The extra pending case is the new integration spec of coder#536, which needs a real Neovim. - `mise run format-check`: 464 files, 0 changed. - Integration runner, with a plain TMPDIR and with `TMPDIR="odd tmp 50%"`: 865 successes, 0 failures, 0 errors on 0.8.0, and 869, 0, 0 on 0.12.3. - `proof-pty-child-hangup.sh` passes 3 of 3 cases on 0.8.0 and on 0.12.3, with a plain TMPDIR, with `TMPDIR="odd tmp 50%"` and (on 0.12.3) with a TMPDIR that holds a colon. On `d6019d13`'s parent, with the odd TMPDIR, it failed 3 of 3 on both builds. - The five `check.sh` scripts (`verify-diff-lifecycle`, `verify-mention-queue`, `verify-selection-tracking`, `verify-terminal-lifecycle` and `verify-ws-connection`) all print PASS. The branch merges `origin/main` (coder#597, coder#594, coder#474, coder#596 and coder#536). coder#536 changed `diff.lua`, its README, `verify-diff-lifecycle` (SKILL.md, `check.sh` and `covered.lock`) and added `diff_answer_every_call_spec.lua`. Git merged the two edits of `verify-diff-lifecycle/covered.lock` with no conflict, and `check.sh` of all five skills prints PASS on the merge result, so no lock needed a new record after `3a1961a0`. - On the merge commit `191a3e24`, the specs this PR adds or changes pass 20 of 20 runs in a plain TMPDIR and in `TMPDIR="odd tmp 50%"` (24 successes for `owned_wait_for_exec_spec`, `snacks_close_spec` and `ld_preload_path_spec`, and 374 for the terminal unit specs plus `native_terminal_toggle_spec`). The integration spec of this PR passes 20 of 20 runs per build in both TMPDIRs. `diff_answer_every_call_spec` from coder#536 passes 10 of 10 runs per build in both TMPDIRs (9 successes each run). ## Not covered - The Snacks case uses a stand-in for Snacks, because CI installs no `snacks.nvim`. The provider code under test is the real one, and the stand-in starts a real pty job with `termopen`. - The wait reads `/proc` or `ps`. Where neither gives a name, the close goes on to `jobstop` and the race stays open, as in native before this PR. A `ps` that hangs would hang the close for as long as it hangs. I did not reproduce that. - I tested the `ps` fallback only on Linux, with `/proc` hidden from Lua. I did not run it on macOS or BSD. - A `jobstop` that other code issues, for example `:bwipeout` of the terminal buffer by the user right after the start, is not covered. - Another PR that edits `native.lua`, `snacks.lua`, `owned.lua` or a `covered.lock` must be merged one at a time with this one, and re-record the lock after its merge. --- _Generated with [`xum`](https://github.com/coder/xum) • Model: `anthropic:claude-sonnet-5-5` • Thinking: `xhigh`_

ThomasK33 added 3 commits November 10, 2026 16:37

feat(skills): add verify-ws-connection, a TLA+ model of the WebSocket…

e669e42

… connection lifecycle (prep)

docs: tell contributors to re-record every verify-* covered.lock (prep)

6489d50

chore(skills): record verify-ws-connection covered.lock

431b9c5

chatgpt-codex-connector Bot reviewed Nov 10, 2026

View reviewed changes

Comment thread .agents/skills/verify-ws-connection/replays/run.sh Resolved

Comment thread .agents/skills/verify-ws-connection/replays/harness.lua Resolved

ThomasK33 added 3 commits November 10, 2026 17:45

Merge remote-tracking branch 'origin/main' into skills/verify-ws-conn…

5167c25

…ection

chatgpt-codex-connector Bot reviewed Nov 10, 2026

View reviewed changes

Comment thread .agents/skills/verify-ws-connection/model/WsConnection.tla Resolved

Comment thread DEVELOPMENT.md Resolved

docs: iterate over the verify-* skills to find stale locks (not a bar…

df61a20

…e glob)

ThomasK33 mentioned this pull request Nov 10, 2026

fix(server): do not drop a live Claude on a late keepalive tick #479

Merged

ThomasK33 added 5 commits November 10, 2026 21:17

Merge remote-tracking branch 'origin/main' into skills/verify-ws-conn…

6949b0b

…ection

Merge remote-tracking branch 'origin/main' into skills/verify-ws-conn…

f3b607b

…ection

chatgpt-codex-connector Bot reviewed Nov 10, 2026

View reviewed changes

Comment thread .agents/skills/verify-ws-connection/model/WsConnection.tla Resolved

ThomasK33 added 5 commits November 11, 2026 17:57

Merge origin/main into skills/verify-ws-connection

d3c5976

Merge origin/main into skills/verify-ws-connection

77bb6e2

ThomasK33 added 3 commits November 11, 2026 21:17

docs(skills): say that the bytes-only contrast of blocks-before-the-p…

d57ef5c

…oll depends on timing

Merge origin/main into skills/verify-ws-connection

bd89345

ThomasK33 added 4 commits November 12, 2026 18:09

Merge origin/main into skills/verify-ws-connection

7598c56

Record the verify-ws-connection lock: main's #541 changed the file hash of lua/claudecode/init.lua in M._broadcast_at_mention, which the model does not cover. The covered blocks are unchanged.

Merge origin/main into skills/verify-ws-connection

a929777

A clean merge of #544 (terminal files only). Every covered.lock matches the code, so no lock needs a new record.

Merge origin/main into skills/verify-ws-connection

9547534

A clean merge of #577 (diff.lua). Every covered.lock matches the code, so no lock needs a new record.

chatgpt-codex-connector Bot reviewed Nov 12, 2026

View reviewed changes

Comment thread .agents/skills/verify-ws-connection/model/WsConnection.tla Resolved

Comment thread .agents/skills/verify-ws-connection/replays/harness.lua Resolved

ThomasK33 added this pull request to the merge queue Nov 13, 2026

ThomasK33 mentioned this pull request Nov 13, 2026

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

Open

Merged via the queue into main with commit f28eba7 Nov 13, 2026
7 checks passed

ThomasK33 deleted the skills/verify-ws-connection branch November 13, 2026 08:58

ThomasK33 mentioned this pull request Nov 13, 2026

fix(terminal): wait for the child's exec before the snacks close and the owned stop #602

Merged

Conversation

ThomasK33 commented Nov 10, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

What it checks

Bugs this model found

Round 7 (the one extra review round that the maintainer allowed)

What changed since the first version of this PR

What this PR changes outside the skill

Proof

Run it

Uh oh!

ThomasK33 commented Nov 10, 2026

Uh oh!

ThomasK33 commented Nov 10, 2026

Uh oh!

chatgpt-codex-connector Bot commented Nov 10, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

chatgpt-codex-connector Bot commented Nov 10, 2026

🛡️ Codex Security Review

Uh oh!

chatgpt-codex-connector Bot left a comment

Choose a reason for hiding this comment

💡 Codex Review

Uh oh!

Uh oh!

Uh oh!

ThomasK33 commented Nov 10, 2026

Uh oh!

ThomasK33 commented Nov 10, 2026

Uh oh!

chatgpt-codex-connector Bot commented Nov 10, 2026

🛡️ Codex Security Review

Uh oh!

chatgpt-codex-connector Bot left a comment

Choose a reason for hiding this comment

💡 Codex Review

Uh oh!

Uh oh!

Uh oh!

ThomasK33 commented Nov 10, 2026

Uh oh!

ThomasK33 commented Nov 10, 2026

Uh oh!

chatgpt-codex-connector Bot commented Nov 10, 2026

🛡️ Codex Security Review

Uh oh!

chatgpt-codex-connector Bot left a comment

Choose a reason for hiding this comment

💡 Codex Review

Uh oh!

Uh oh!

ThomasK33 commented Nov 10, 2026

Uh oh!

ThomasK33 commented Nov 10, 2026

Uh oh!

chatgpt-codex-connector Bot commented Nov 10, 2026

Uh oh!

ThomasK33 commented Nov 11, 2026

Uh oh!

ThomasK33 commented Nov 11, 2026

Uh oh!

chatgpt-codex-connector Bot commented Nov 11, 2026

Uh oh!

chatgpt-codex-connector Bot commented Nov 11, 2026

🛡️ Codex Security Review

Uh oh!

ThomasK33 commented Nov 12, 2026

Uh oh!

ThomasK33 commented Nov 12, 2026

Uh oh!

ThomasK33 commented Nov 12, 2026

Uh oh!

chatgpt-codex-connector Bot commented Nov 12, 2026

🛡️ Codex Security Review

Uh oh!

chatgpt-codex-connector Bot left a comment

Choose a reason for hiding this comment

💡 Codex Review

Uh oh!

ThomasK33 commented Nov 10, 2026 •

edited

Loading

chatgpt-codex-connector Bot commented Nov 10, 2026 •

edited

Loading