fix(server): drop a client that answers pings but never reads by ThomasK33 · Pull Request #467 · coder/claudecode.nvim

ThomasK33 · 2026-11-10T15:00:32Z

Why

Goal: a Claude that answers every ping but never reads must not pin Neovim's memory. Today it does. The ping timer drops a client only when no pong arrived for interval * 2. Replies and pings that this client never reads wait in libuv's write queue, which is Neovim's memory, and nothing bounds that queue. A probe on current main grew the queue to 118,225,574 bytes in 30 s (Neovim RSS about 222 MB), and the client was never closed. A local client needs the lock-file auth token to do this, but a Claude whose reader stalls while its pong path still runs does the same.

The rule

A client that answers its pings is closed, and its queue goes with it, when its libuv write queue shows no progress at two ping ticks in a row and still shows none right after libuv's next poll.

Three terms:

A tick is one run of the ping timer (every 30 s by default).
Progress means libuv wrote at least one more byte of the client's queue since the last progress, or the queue is empty.
A poll is the step of the libuv loop where libuv asks the operating system which sockets are ready.

Two places use the idea of "no write progress":

The ping timer applies the rule above to every connected client.
A deadline applies a simpler rule to a Close frame that waits in the queue. A client that broke the protocol, or that stop_server closed, has left server.clients, so the ping timer cannot see it. Without the deadline a Claude that never reads kept that socket and its queue until Neovim exited. That was the limit that fix(server): drop dead clients promptly and never time out a live Claude #455 wrote into the server README. client.close_timer is a repeating timer, one keepalive_timeout long, that runs while client.close_pending is set. A socket that wrote no byte of its queue in that window is closed, and the queue with it.

The bound is time without write progress, never queue size. A cap on size drops a live Claude that receives one large openDiff payload. The window is two ticks, so no new constant exists. The default is 60 s to 90 s after the last actual write progress. The next tick records that progress. The following two ticks find no further progress, and the second confirms the stall after the next poll. That holds for ticks that come late by less than 1.5 intervals, plus their delay. The wake rule below covers later ticks. The ping timer closes with Close 1011 and disconnect 1006 through the existing disconnect path (_disconnect_client, then on_disconnect), so pending diffs of that client are rejected as for any disconnect. The Close-frame deadline closes only the socket. The frame keeps its original status, which is the protocol error's status or 1001 from stop_server. The pending diffs of that client were already rejected by then. In both cases the Close frame cannot reach the peer, because it waits behind the queue. Closing the socket drops it.

Why the drop waits for a look after the next poll

The pushed head (8fe3c19) closed a client when its queue showed no progress for interval * 2. That can close a Claude that reads. libuv learns that a socket can take more bytes only in its poll step. Neovim can run the ping tick right after its main loop was blocked inside an I/O callback, and that tick runs before the poll that reports what Claude read during the block. A Claude that resumed reading then shows no progress, although it reads. In a real-socket probe the pushed head closed such a reader after 4.00 MB read (first table below). #479, merged to main, fixed the same kind of false drop for the pong rule by giving a late tick a second chance.

Two earlier attempts at the same defect failed in verification. Both stayed on local heads and were never pushed. The later one is the "5% head" (9a0d8d4) in the tables below. They excused a late tick, meaning a tick more than 1.05 intervals after the one before it. Two independent verifiers found two holes:

A tick that comes within 5% after its due time is not late by that rule, and it can still run before the poll. A real-socket probe let a reader resume during a 500 ms block inside an I/O callback. The reader read 1.61 MB from the socket, and that head still closed it ("Write queue stalled"). That happened on Neovim 0.12.3 and on 0.8.0, at a 5 s interval and at the default 30 s.
A tick that is late every time never counts, so a stalled client stayed past the bound. One verifier kept a stalled client for 126 s with callbacks of about 2 s.

This head has no lateness rule. When the second tick in a row finds no progress, the tick sends its ping as usual and calls after_next_poll (tcp.lua). That function starts two libuv handles:

a check handle, which libuv runs right after every poll step, in every libuv version, and
an idle handle, which keeps that poll from waiting for a timer or a socket.

The check callback closes both handles, takes them off server.pending_polls, samples the queue once more, and closes the client only if there is still no progress. A client that left or started to leave in the meantime, because the poll read its EOF, a read error, its Close frame or a protocol error, is skipped without a log line. A reader that resumed during a block before that poll makes progress by then, and the count clears. The first tick that finds no progress only sets client.write_stalled. A false first count is harmless, because the drop needs a second tick and the look after the poll. If libuv cannot create a handle, the tick leaves the client for the next tick. stop_server closes the handles of a look that did not run yet (server.pending_polls lists them).

The look is a sample, and it has one known race. libuv takes its snapshot of the ready sockets when a poll starts. A callback that blocks inside that poll, after the snapshot, hides what Claude reads during the block from the check callback that follows. A client that was stalled for the whole window (two ticks) and resumes during such a block is dropped. That is a deadline race, as with any timeout: the client was stalled when the window ended, and what it read afterwards is not reported yet. Two verifiers closed a reader that way in real-socket probes: a 0.5 s block (3.86 to 3.99 MB read, Neovim 0.12.3 and 0.8.0, 3 s and 30 s intervals) and a 1.5 s block (3.93 MB read, 5 s and 30 s). A block after the tick and before that poll keeps the reader, and so does a block in a scheduled callback. A detector for blocks inside the poll is possible: a prepare handle that times each poll, and a look that repeats until a poll was short. A prototype kept the reader in the two poll-block probes of the verifier on Neovim 0.12.3. I did not run it on 0.8 or on the full probe set. It adds a third handle, a threshold and a give-up count, and it still leaves a window as wide as the threshold, so this PR does not include it.

A tick gap above interval * 1.5 counts as a wake from sleep. A wake tick starts a fresh stall window: it resets last_pong of each connected client (as on main), resets last_drain, clears the count, and judges nothing, because Claude had no chance to read after the sleep. That delays the drop by one tick when the count was clear, and by two ticks when the wake tick takes the place of the confirming tick. The next two ticks always count, wake ticks or not, and a wake tick within them only resets last_pong. Wake ticks that come again and again are a loop that stays blocked, not sleeps. So whatever the pattern of late ticks, a stalled client is closed at the second tick after a fresh window started. A wake tick three or more ticks after the last fresh start starts a new window. Before this rule every wake tick cleared the count, and a verifier kept a client with 12.8 MB queued for 20 intervals while every tick was a wake tick. Ticks that come late by less than 1.5 intervals move the drop by their own delay and no more.

What changed

client.lua: write() counts the bytes it passes to the socket in client.queued_bytes, and every socket write goes through it (frames, pings, pongs, Close frames). A frame of more than 1 MiB is queued in pieces of 1 MiB, and the callback of the last piece reports the frame. New M.sample_write_progress, M.is_client_reading(client) and M.abandon_close_frame. close_client starts the Close-frame deadline. create_client(tcp_handle, keepalive_timeout) takes the window.
tcp.lua: the ping tick samples every connected client and, for a client that answered, calls confirm_stall at the second tick without progress. New local functions after_next_poll, close_pending_polls, confirm_stall and drop_client (the close sequence the keepalive drop and the stall drop share: Close 1011, then abandon_close_frame, then _disconnect_client with 1006). The drop logs one info line: Closed client_<n>: not reading for <s>s, <n> KB queued. start_ping_timer sets server.keepalive_timeout to interval * 2. stop_server closes pending handles.
A pong rule runs first on each tick: a client without a pong gets a second chance (pong_overdue) and then the keepalive drop, whatever its queue shows. Only a client that answered is judged for a stall.
lua/claudecode/server/README.md: the "never reads keeps its socket" limit is replaced by the rule above. The API list, the ping-timer item and the side-effects list name the new functions and handles.
tests/mocks/vim.lua: new_check and new_idle mocks. Fake clients in the server specs carry queued_bytes and get_write_queue_size.
tests/unit/server/connection_lifecycle_spec.lua: 61 tests, 28 before this round. The spec stubs valid_utf8, so the 1 MiB-and-larger frames do not run the real validator under luacov (see Verification).
covered.lock re-recorded.

Since the last push (`8fe3c19`)

The stall rule changed from "no progress for interval * 2" to "no progress at two ticks in a row, and still none right after the next poll". is_client_reading lost its timeout argument and counts through client.write_stalled.
The stall rule now sits behind the pong rule of fix(server): do not drop a live Claude on a late keepalive tick #479: a client without a pong gets the second chance and the keepalive drop, whatever its queue shows. Only a client that answered is judged for a stall.
A wake tick makes no judgement and clears the count, unless a fresh window started in the last two ticks. Then it counts like any tick.
The ping and pong byte count, and the error of the last piece of a split frame, had no test. They have tests now (the code did not change).
The lifecycle spec grew from 28 to 61 tests. The spec stubs valid_utf8, and builds its pong frame in before_each.
The server README, covered.lock and the vim mock (new_check, new_idle) follow.

Tradeoffs

Slow readers. libuv writes more only after the kernel reports the socket writable again. On a Linux loopback socket with the default 4 MiB tcp_wmem maximum, the reader had to read 1.16 to 1.54 MB (median 1.35 MB over 8 cycles) before that happened. So a Claude must read about 1.4 MB per window while a backlog exists. At the default 60 s window that is about 23 KB/s. I measured this on Linux only. A real Claude reads far faster. A reader at 100 KB/s stayed connected for 200 s (see the live probes).
A reader that keeps up just enough. Size is not capped, so a Claude that reads a little more than that floor, while Neovim queues more than it reads, still lets the queue grow. I chose this over a size cap because any cap drops a live Claude that gets a large message.
One large message. A 64 MB message that a reader takes at 1 MB/s stays connected for as long as libuv writes any of it.
Close-frame deadline. A protocol-error client that reads slowly keeps its socket while it reads. A client that stops reading is cut after one to two windows, and its Close frame is dropped. One window without progress is enough here: the client is leaving anyway, so a close that comes too early after a blocked loop costs only its Close frame.
Windows. libuv on Windows adds a whole write request to the queue size when it is queued and subtracts it when the request completes (src/win/tcp.c), while on Linux and macOS it lowers the size as bytes are written (src/unix/stream.c). So a frame of more than 1 MiB is queued in pieces of 1 MiB, and a Claude must finish one piece per window there. I have no Windows host here, so I did not run it. This rests on the libuv source and on a test that models a reader finishing whole requests.
Piece size. The 1 MiB piece is one fixed constant. It costs one extra copy of a large frame while it is queued. A frame of 1 MiB or less is one write, as before.
Two handles per look. A look exists only for a client that answered and showed no progress at two ticks in a row. The check callback closes the pair in the loop pass where it runs. A server whose clients all read normally never creates one.
One more ping. The tick that asks for the look still pings, because the drop comes after the poll. That ping is a few bytes in a queue that is dropped a moment later.
A race in the look. A client that was stalled for the whole window and resumes during a block inside the confirming poll is dropped. See "The look is a sample" above. The cost is one reconnect of Claude, with the pending diffs of that client rejected as for any disconnect.
Wake from sleep. The Close-frame deadline has no wake reset. It only closes a client that already broke the protocol or that the server stopped.

Scope and blast radius

Server transport only: client.lua, tcp.lua and their README. The change adds one disconnect reason and one socket close for a Close frame that nobody drains. Both use the existing _disconnect_client and on_disconnect path. The stall drop now runs one libuv poll after the tick, from a check callback instead of the timer callback. It changes no diff state and no openDiff answer beyond that path. verify-diff-lifecycle check.sh passes after the re-record. Only the client.lua and tcp.lua file hashes and the create_client block hash changed. No code fact reads FALSE.

No credential handling changes. The auth token is neither read nor written by this diff.

The blast radius is all WebSocket clients. A client that reads normally has an empty queue at each tick, which counts as progress. The risk is a false drop of a very slow reader (see Tradeoffs). create_client has a second, optional parameter. Fake clients in tests must carry queued_bytes.

Verification

Tests

mise run all with CLAUDE_CONFIG_DIR unset, on the merged head: 1393 successes, 0 failures, 0 errors, 16 pending (specs that need a real Neovim). luacheck: 0 warnings in 163 files. mise run format-check (treefmt --ci): 329 files, 0 changed.
Server specs (tests/unit/server, tests/unit/server_spec.lua): 191 ok, 0 not ok.
scripts/run_integration_tests_individually.sh: reports 272 successes, 0 failed, 0 errors. The script counts the lines "Success" and "Success: N" in each spec's output, so the true number is 254 (the other 18 are summary lines). That counting is older than this PR, and I did not change it.
.agents/skills/verify-diff-lifecycle/check.sh: PASS (main 89,205 states, live 5,269 states) after the re-record. --hash-only: matches. No code fact reads FALSE.
Shuffled orders: the lifecycle spec and send_utf8_spec pass with busted --shuffle --seed=N for N in 467, 11, 12, 99, 2026 and the eight seeds below (64 ok each). mise run all shuffles too and prints its seed. The pong frame of the spec is now built in before_each. Building it while the file loads fails with "attempt to index upvalue 'frame'" under --shuffle --seed=N for N in 17, 18, 24, 25, 50, 51, 66 and 75 (a scan of 1 to 80, one failing test each) and passes at the other 72 seeds. Seed 467 no longer exposes it.
CI time: an earlier head of this PR made CI take about 14 minutes, because the 1 MiB-and-larger frames in the lifecycle spec ran the real UTF-8 validator under luacov. That one spec took 753 s under luacov. The spec now stubs valid_utf8 and takes 45 s (54 s on this head, on a busy machine).
The fake timer of the lifecycle spec rejects a second close(), as libuv does and as the spec's fake check, idle and socket handles already did. Before, it accepted one, and removing client.close_timer = nil from stop_close_timer passed every test. On real sockets every drop then raised "handle is already closing" from the Close frame's write callback. With the assertion, that mutant fails 3 tests.
No test passed only on retry.

Red to green and mutants

I ran the lifecycle spec of the previous head (54 tests) against older code: 22 of its tests failed against the code of the pushed head (8fe3c19), and 12 against the local 5% head (9a0d8d4, never pushed). The spec of this head has 61 tests.

Each mutant below changes one guard of this head. Every one makes at least one test fail:

Mutant	Tests that fail
The tick closes the client itself, with no look after the poll	14
The check callback closes without sampling the queue again	2
No idle handle next to the check handle	1
The handles stay open after the callback ran	4
The finished look stays in `server.pending_polls`	1
`stop_server` leaves the handles of a pending look open	1
The look skips no client that left in the poll (no guard)	3
The look skips only a client that left `server.clients`, not one that is no longer connected (a peer Close)	1
The look skips only a client that is no longer connected, not one that left `server.clients`	1
Every tick asks for a look, not only the second	35
A wake tick that starts a fresh window samples the queue	6
A wake tick that starts a fresh window does not reset `last_drain`	2
Every wake tick starts a fresh window, as before the counter	2
A fresh window protects one tick, or three, instead of two	2 and 1
A fresh window never ends	1
A wake tick inside a fresh window does not reset `last_pong`	2
Pings are written without the byte count	3
Pongs are written without the byte count	1
The write error of the last piece of a frame is dropped	5
A frame of more than 1 MiB is not split	4
The deadline of a Close frame closes without sampling	1
`drop_client` does not end the deadline	1
`stop_close_timer` does not clear `client.close_timer` before it closes the timer	3

The survivors of other mutations are listed at the end.

Real sockets, Neovim 0.12.3 (libuv 1.52.1) and 0.8.0 (libuv 1.44.2)

I ran a headless Neovim with its own XDG directories and CLAUDE_CONFIG_DIR against raw WebSocket clients that play Claude. The rows for the block and memory probes ran on the server code of 964b744. The commits after it change the wake rule, remove a dead store, and add comments and tests, so I ran the probes that touch ticks, wakes and the plain stall again on the head of the wake counter (5c910f7): the fresh.py rows, the 1.35 and 1.6 rows and the 3 s stall. client.lua and tcp.lua are the same on the final head. The auth token appears in no output file (match count 0). The probes that block the loop use one block of 0.5 s to 5.5 s, either inside an I/O callback (a libuv accept callback) or inside a scheduled callback. Every client except the "parsing reader" rows sends pongs without being pinged. The parsing reader reads and parses frames and answers each ping it reads.

A reader resumes during a block, and the tick comes just after. Interval 5 s. The reader stalled, and starts reading while the loop is blocked. "Closed" and "kept" describe the client at the end of the run.

Case	`8fe3c19` (on GitHub)	5% head (`9a0d8d4`, local)	This head
Block inside an I/O callback, tick 1.02 intervals after the last: 0.12.3	closed, 4.00 MB read	closed, 3.93 MB read	kept, 33.55 MB read
Same: 0.8.0	closed, 3.93 MB read	closed, 3.93 MB read	kept, 33.55 MB read
Same, tick 1.00 intervals after the last: 0.12.3 and 0.8.0	not run	not run	kept, 33.55 MB read
Same, parsing reader: 0.12.3 and 0.8.0	not run	closed, 3.95 MB read	kept, 33.55 MB read
Block inside a scheduled callback, tick 1.02 late: 0.12.3	kept	kept	kept
Same: 0.8.0	closed, 3.93 MB read	closed, 3.93 MB read	kept
Block of 1.35 intervals: 0.12.3 and 0.8.0	closed, 3.93 MB read	kept	kept

In the I/O callback rows, the tick after the block saw no progress yet (the probe records it). This head kept the client because the look after the next poll saw progress.

A second probe, fresh.py (not run on 8fe3c19): a reader that stalled for one tick resumes 50 ms into a 500 ms block inside an I/O callback, and the next tick runs right after the block.

Interval, Neovim	5% head (`9a0d8d4`, local)	This head (`5c910f7` and `964b744` gave the same numbers)
5 s, 0.12.3	closed, 1.61 MB read	kept, 15.97 MB read
5 s, 0.8.0	closed, 1.61 MB read	kept, 16.14 MB read
30 s (default), 0.12.3	closed, 1.61 MB read	kept, 15.97 MB read
30 s (default), 0.8.0	closed, 1.61 MB read	kept, 16.14 MB read

A stalled reader that answers each ping, with ticks that come late. Interval 5 s. A block in a timer callback after each tick makes the next tick late. The loop reads and answers nothing else.

Pattern	5% head (`9a0d8d4`, local)	`8fe3c19` (on GitHub)	`964b744`	`5c910f7` (same server code as this head)
Every tick 1.35 intervals late (below the wake threshold of 1.5), 0.12.3	kept for the whole 120 s (17 late ticks)	closed after 18.4 s	closed after 19.3 s	closed after 19.3 s
Same, 0.8.0	kept for the whole 120 s	not run	closed after 18.5 s	closed after 19.2 s
Every tick 1.6 intervals late, so every tick is a wake tick, 0.12.3	not run	not run	kept for the whole 100 s	closed after 29.3 s
Same, 0.8.0	not run	not run	kept for the whole 100 s	closed after 29.2 s
1.6 intervals late after the stall sample only, so wake ticks alternate with ticks in time, 0.12.3	not run	not run	kept for the whole 100 s	closed after 26.3 s
Same, 0.8.0	not run	not run	kept for the whole 100 s	closed after 26.2 s

The last four rows are the case that a verifier found on 964b744 (every wake tick cleared the count) and the case that my first rule for it did not cover (wake ticks that alternate with ticks in time). The counter rule above closes both.

A block inside the confirming poll (not run by me, from two verifiers). A client that was stalled for two ticks, whose reader resumed 0.05 s to 0.1 s into a 0.5 s or 1.5 s block inside the poll that the look waits for, was closed after 3.86 to 3.99 MB read. That is the deadline race described above. A 500 ms block before that poll or inside a scheduled callback kept the reader.

Plain stall, and the pong rule (interval 3 s). The reader never reads, one case answers each ping, one never answers, one answers only from 10 s, one with a 6 s block of the loop at 7.5 s (a machine that slept):

Case	Closed after	Reason
Never reads, answers pings	8.9 s (0.12.3), 8.9 s (0.8.0), also on `5c910f7`	Write queue stalled
Never reads, never answers	12.0 s	Connection timeout, after the second chance
Never reads, first pong at 10 s	12.0 s	Write queue stalled
Never reads, loop blocked 6 s at 7.5 s	19.5 s, 6 s after the wake tick	Write queue stalled

The times are the same on the 5% head. On 8fe3c19 the plain stall closes after 8.9 s too (not run for the other three).

Memory and controls (0.12.3). A raw client, no block of the loop:

Case	Result on this head
Never reads, one pong per second, 1000 requests per second (3 s ping, 6 s window)	Closed 8.9 s after the accept. The queue was 34,331,532 bytes and is then 0. Lua heap falls from 46,526 KB to 1,720 KB after a GC. RSS fell from 71,392 to 56,580 kB in this run.
Same at the default 30 s ping, 250 requests per second	Closed 89.9 s after the accept. The queue was 87,263,130 bytes and is then 0. Lua heap falls from 149,421 KB to 1,953 KB.
Breaks the protocol (BINARY frame) while the queue is 10 MB and never reads	Socket closed 7.0 s later. The queue was 10,367,540 bytes and is then 0. Lua heap 1,524 KB after a GC.
Control: reads 1 MB/s, 300 requests per second (3 s ping, 60 s)	0 disconnects. 62.65 MB read.
Control: reads 100 KB/s, 300 requests per second (default ping, 200 s)	0 disconnects. The queue reached 216,165,112 bytes.
Control: one 64 MB message, reader at 1 MB/s for 55 s (default ping)	Connected. 56.6 MB read. After the reader stopped, closed 63.7 s later.

The row for 100 KB/s shows the second tradeoff above: a reader above the floor keeps its connection while the queue grows.

What the tests and probes do not cover

No unit test runs libuv. The fake check and idle handles run their callback when the spec says that a poll happened. Only the real-socket probes show libuv's order of phases, on Linux with 0.12.3 and 0.8.0. I ran no Windows and no macOS.
A block inside the confirming poll is the race above. The probes of two verifiers show it, and no test pins it, because the fake loop has no snapshot to miss.
Neovim 0.8's uv.walk crashes on handles that luv did not create, so the probes count the check and idle handles only on 0.12.3 (0 left open at the end of every run).
The slow-reader probes send a pong every second without being pinged. A real Claude answers each ping, so the pong path here is easier than in real life.
Mutations that survive the server specs and the full suite. The list below is one non-exhaustive set: the seven survivors of one verifier's mutation set. A second verifier's independent set of 88 mutants found the same seven, one test gap (the close_timer line above, now covered), and eight more that change no behavior. A third verifier's set of 55 mutants found two survivors that do change behavior and have no test: the first delay of the Close-frame deadline (timer:start(timeout, timeout, ...) in start_close_timer). Started at once, the deadline cuts off a client that reads, before it reads its Close frame. Started after three windows, it keeps the socket of a client that never reads for three windows instead of one. Both change behavior only for a client that is already being disconnected, and no test reads the delay. I will cover them in a follow-up PR. Other survivors can exist. I know of no defect in the code behind any listed survivor.
1. An empty queue counting as progress in sample_write_progress. It is equivalent: every tick writes a ping, so a queue that is empty at a tick always follows progress.
2. Writing the Close frame that answers a peer's Close with tcp_handle:write, which skips the byte count of write(). That reply starts no deadline, and the client is closing, so the tick and the look skip it.
3. Writing the Close frame of close_client the same way. It is equivalent for the progress decisions after the socket is closing, because the deadline compares two samples of queued_bytes less the queue size, and a frame that is queued before the first sample cancels out.
4. The identity check of the Close-frame timer (client.close_timer ~= timer).
5. The check of close_pending in the timer callback, its early exit when the write already finished.
6. The check of handle:is_closing() in the timer callback.
7. The if not timer then return end guard in start_close_timer, for a vim.loop.new_timer() that fails.
  For 4 and 5 every path that clears close_pending also stops the timer in the same step, and libuv runs one callback at a time, so I know of no order that reaches them. I did not look for an order that reaches 6 and 7. A verifier's advisory pass found no failing order for 4 to 7.
  The eight that change no behavior, from the second verifier:
- <= to < for a frame of exactly 1 MiB in write(): the piece loop makes the same single write.
- The stop_close_timer call inside start_close_timer: dead code, because close_client returns early for a closing client, so the deadline starts once per client.
- The last_drain store in start_close_timer: a closing client is never logged.
- close_pending = nil when the deadline closes the socket: the cancelled write callback clears it in the same loop pass.
- The initial last_drain in create_client: the first sample always sees the drained 101 reply.
- Running fn before the handles close in the look.
- The is_closing check in close_pending_polls: pending handles are never closing.
- handle:stop() before handle:close() in the look: uv_close stops the handle.
  Tests do observe the 1011 Close frame of a ping drop: leaving it out turns 8 tests red.
The state half of the look's guard (client.state ~= "connected") is reachable and has a test. A peer Close sets the client to closing before its scheduled removal, so a look that runs in between finds a client that is listed and no longer connected. Without the guard the look reports 1006 "Write queue stalled" instead of the peer's 1000.

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

A Claude that answers each ping but never reads kept its replies in libuv's write queue, and so in Neovim's memory, without limit. The ping timer now also drops a connected client whose queue is non-empty and had no byte written for two ping intervals, the window of the keepalive. Progress counts bytes libuv wrote, so a slow reader or one large message is never dropped.

…led-write-queue

A client that broke the protocol, or that the server stopped, leaves the server's list with its Close frame still queued. The ping timer cannot see it, so a Claude that never reads kept the socket and the queue until Neovim exited. close_client now starts a deadline for the frame with the keepalive window of the server: a socket that wrote no byte for that window is closed, and the queue with it. The write callback and the deadline each end the other, and the ping timer's drop ends it too. Also records covered.lock and states the rule in the server README.

…led-write-queue

ThomasK33 · 2026-11-10T15:00:43Z

@codex review

ThomasK33 · 2026-11-10T15:00:46Z

@codex security review

chatgpt-codex-connector · 2026-11-10T15:01:02Z

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-11T05:22:00.101287Z	`1bb968f`	Manual request
🔒 Security Review	✅ Completed 2026-11-11T05:23:16.184419Z	`1bb968f`	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-10T15:03:25Z

Codex Review: Didn't find any major issues. You're on a roll.

Reviewed commit: 51fee905ba

ℹ️ 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-10T15:05:25Z

🛡️ Codex Security Review

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

Reviewed commit: 51fee905ba

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.

stylua needs two passes on one assertion. The first pass left a layout that treefmt --ci (the format-check job) formats again.

ThomasK33 · 2026-11-10T16:37:46Z

@codex review

ThomasK33 · 2026-11-10T16:37:49Z

@codex security review

chatgpt-codex-connector · 2026-11-10T16:40:46Z

Codex Review: Didn't find any major issues. Another round soon, please!

Reviewed commit: c3c934eff1

ℹ️ 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-10T16:41:04Z

🛡️ Codex Security Review

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

Reviewed commit: c3c934eff1

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.

…led-write-queue # Conflicts: # .agents/skills/verify-diff-lifecycle/covered.lock

Clients built by hand in server_spec write through client.write, which counts the bytes in client.queued_bytes.

ThomasK33 · 2026-11-10T17:57:27Z

@codex review

ThomasK33 · 2026-11-10T17:57:29Z

@codex security review

chatgpt-codex-connector

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 6d6293a5f1

ℹ️ 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-10T18:02:37Z

🛡️ Codex Security Review

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

Reviewed commit: 6d6293a5f1

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.

…gress libuv on Windows lowers a socket's write queue only when a whole write request is done. A Claude that reads one large message slowly then showed no progress and was dropped as stalled. Frames of more than 1 MiB are now queued in pieces of 1 MiB, and the callback of the last piece reports the frame.

…led-write-queue

ThomasK33 · 2026-11-10T18:38:39Z

@codex review

ThomasK33 · 2026-11-10T18:38:41Z

@codex security review

chatgpt-codex-connector · 2026-11-10T18:42:42Z

Codex Review: Didn't find any major issues. 🎉

Reviewed commit: a6d7313445

ℹ️ 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-10T18:44:33Z

🛡️ Codex Security Review

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

Reviewed commit: a6d7313445

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.

…s, drop a dead last_drain store A second wake tick in a row is a loop that stays blocked, not a sleep, so it counts like any tick. The look's client guard and its pending_polls removal get tests. The 101 reply no longer sets last_drain: the first tick sees the 101 bytes as progress anyway. The comments of write_stalled and is_client_reading describe the tick and the look.

… a run of wake ticks

…ead last_drain store

A wake tick starts a fresh stall window only when none started in the last two ticks. Wake ticks that alternate with ticks in time, or that come every time, no longer clear the count for ever: a stalled client is closed at the second tick after a fresh window started.

…e, and fix two wake-delay texts A peer Close sets the client to closing before its scheduled removal, so the confirming check sees a client that is listed and not connected. The test fails when that guard is removed. The README and the spec comment no longer say that the drop holds however late the ticks come, and a wake tick delays the drop by one tick or by two.

The fake timer accepted a second close() while the fake check, idle and socket handles already reject one. Removing client.close_timer = nil from stop_close_timer therefore passed every test, although on real sockets every drop then raises "handle is already closing" from the Close frame's ECANCELED write callback.

…ng the clients the look skips

ThomasK33 · 2026-11-11T05:19:26Z

@codex review

ThomasK33 · 2026-11-11T05:19:33Z

@codex security review

chatgpt-codex-connector · 2026-11-11T05:21:58Z

Codex Review: Didn't find any major issues. 🎉

Reviewed commit: 1bb968fc32

ℹ️ 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-11T05:23:14Z

🛡️ Codex Security Review

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

Reviewed commit: 1bb968fc32

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.

#467 (a client that answers pings but never reads) rewrote the ping tick, the pong rule and their tests. Keep its stall rule and put the keepalive of this branch next to it: - the tick pings every client, stamps the oldest unanswered ping, and arms one check and idle pair (after_next_poll) that judges both rules after the poll - a client answered when no ping of it waited for the window; only an answered client is confirmed for a stall, and a silent one is dropped by the keepalive judgement whatever its write queue shows, as under the pong rule - remove pong_overdue and is_client_alive, which the stamp replaces, and adapt the tests that named them - the spec keeps the 61 tests of #467 and adds the tests of the keepalive, the gap skip and the any-bytes rule

…ld (coder#495) ## Why The goal is a test suite that fails when someone changes the first delay of the Close-frame deadline or the wake threshold of the ping timer. Both came out of the two verification lanes of coder#467 (merged as edcbe3c). One lane found mutants of the deadline line that passed every test. The other found a mutant of the wake line that did the same. The lanes also asked for two wording fixes in the server README. What goes wrong if the lines regress: 1. The Close-frame deadline (`start_close_timer` in `client.lua`) waits one keepalive window for a Close frame that sits in a queue. If its first delay becomes 0, it closes a client that still reads, in the next loop iteration. The verifier measured a reader at 1 MB/s that got 7.85 MB of the 23 to 25 MB queued, then EOF and no Close frame. If its first delay becomes three windows, a client that never reads keeps its queue for 18.0 s instead of 6.0 s at a 3 s ping interval. 2. The wake rule (`elapsed > interval * 1.5` in `start_ping_timer`) counts a tick as a wake when it comes more than 1.5 intervals after the tick before it. A wake tick starts a fresh stall window only when it comes three or more ticks after the last fresh start. If `>` becomes `>=`, a tick at exactly 1.5 intervals restarts the window, and a stalled client that answers pings stays up to two ticks longer (60 s at the default interval). If the factor grows, a real wake is counted as a late tick. No runtime behavior is wrong today. Only the tests were missing. ## What changed 1. `test(server): pin the first delay of the Close-frame deadline`. One test asserts that the deadline timer first runs after `2 * interval`. The fake timers of the lifecycle spec run a callback only when a test calls it, so no earlier test read `delay`. 2. `test(server): pin the wake threshold to the millisecond`. Two tests in the stall-confirmation block. A tick at exactly 1.5 intervals is not a wake, so the stalled client is dropped. A tick 1 ms above 1.5 intervals is a wake, so the count clears and no confirmation is armed. The message of commit 4ccbab1 is imprecise. It says existing tests "used gaps of 1.4 intervals and 20 intervals only". Main's spec also uses gaps of 1, 1.06 and 1.3 intervals and a first tick of 3.33 intervals. No existing gap lay between 1.4 and 3.33 intervals, so the conclusion holds. I do not amend the commit. 3. `docs(server): name a read error and state the wake gap exactly`. - README line 81 now says the confirmation skips a client whose poll read "its EOF, a read error, its Close frame or a protocol error". A read error removes the client the same way an EOF does (`tcp.lua`, `read_start` callback). A new test pins the claim. - README line 81 said ticks run "late by less than 1.5 intervals". The code compares the gap to the tick before, and a gap above `interval * 1.5` is a wake. The sentence now says "late ticks, each of which comes at most `interval * 1.5` after the tick before it", and "a tick that comes more than `interval * 1.5` after the tick before it counts as a wake from sleep". ## Scope Changed: `tests/unit/server/connection_lifecycle_spec.lua` (4 tests) and one line of `lua/claudecode/server/README.md`. Not changed, with the reason: 1. Server Lua. The behavior is right, so no `lua/` file changes and `covered.lock` stays valid. 2. M17 (the idle handle is not closed when `new_check` returns nil). `luv` raises on out-of-memory and `uv_check_init` always returns 0 on the pinned luv 1.52.1 and libuv 1.52.1. The branch cannot run on a real runtime, so a test would pin only an injected failure. The existing test pins the documented outcome for an idle handle that libuv cannot create: the tick leaves the client for the next tick. 3. M18 (an empty queue does not count as progress). It was listed in coder#467 as equivalent. Each tick writes a ping, so an empty queue at a tick always follows progress. 4. The text of the merged coder#467 description, which named only some survivors. GitHub keeps it as it is. This PR is the follow-up it promised. ## Blast Radius Tests and one documentation line. No runtime code runs differently. `check.sh --hash-only` reports that `covered.lock` matches the code. ## Verification Each mutant below is one edit to a line of `lua/claudecode/server/`. "main spec" is the lifecycle spec from `origin/main` (61 tests). "new spec" is the spec of this branch (65 tests). The edit is reverted after each run. | Mutant | Edit | main spec | new spec | |---|---|---|---| | D1 | `timer:start(0, timeout, ...)` in `client.lua` | 61 ok, 0 red | 1 red: "first runs the deadline one window after the frame" | | D2 | `timer:start(timeout * 3, timeout, ...)` | 61 ok, 0 red | the same test | | W1 | `elapsed >= (interval * 1.5)` | 61 ok, 0 red | 1 red: "counts a tick at exactly the wake threshold" | | W2 | factor 2 instead of 1.5 | 61 ok, 0 red | 1 red: "starts a fresh stall window at a tick 1 ms above" | | W3 | factor 1.4 | 61 ok, 0 red | 1 red: "counts a tick at exactly the wake threshold" | | W4 | `interval * 1.5 + 1` | 61 ok, 0 red | 1 red: "starts a fresh stall window at a tick 1 ms above" | | R1 | the confirmation drops the membership half of its guard | 1 red (EOF test) | 2 red (EOF test and the new read-error test) | | R2 | the confirmation drops the state half of its guard | 1 red (peer-Close test) | 1 red (the same test). The read error removes the client from the list, so the state half is not what the new test pins. | On the branch, the lifecycle spec passes 65 of 65 and no test is red. Gates at head `5411fe16a94e41811ff2448eff004558be3a0183`: 1. `mise run all` (`BUSTED_SEED=46731`) exits 0. 1397 successes, 0 failures, 0 errors, 16 pending. luacheck: 0 warnings, 0 errors in 163 files. treefmt: 329 files, 0 changed. The 16 pending tests need a real Neovim. The verifiers of coder#467 counted 1393 successes at the coder#467 head, so this branch adds 4. 2. `mise run format-check` exits 0. 329 files, 0 changed. 3. Server specs (`busted -o TAP tests/unit/server tests/unit/server_spec.lua`) exit 0. 195 ok, 0 not ok. The verifiers of coder#467 counted 191 at the coder#467 head, so this branch adds 4. 4. The lifecycle and UTF-8 specs in shuffled order, 12 seeds (1 to 10, 46731, 46733): each exits 0 with 68 ok and 0 not ok. 5. `check.sh --hash-only` exits 0: "covered.lock matches the code". I did not run `scripts/run_integration_tests_individually.sh`. The change touches no code that the integration specs reach. --- _Generated with [`xum`](https://github.com/coder/xum) • Model: `anthropic:claude-sonnet-5-5` • Thinking: `xhigh`_

…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`_

…n another client's handshake, and report refused writes (coder#480) ## What you get Each queued @mention now has a deadline: `connection_timeout + connection_wait_delay` ms after you sent it (10.6 s by default). No handshake and no disconnect moves the deadline. At its deadline, a mention that is still queued leaves with an error, unless a ready Claude is connected. A ready Claude is one that completed its WebSocket handshake `connection_wait_delay` ms ago (600 ms by default). While a ready Claude is connected, no deadline clears a mention. The queue drains to it, oldest first, 25 ms apart, also past the deadlines. When that Claude leaves, the next flush clears every mention whose deadline passed meanwhile, with an error, and the rest wait for their own deadlines. So a Claude that completes its handshake less than `connection_timeout` ms after a send, and stays connected, gets that mention, and every other mention still queued when it is ready. With 100 mentions sent at once and a handshake 8 s or 9.8 s later, all 100 arrive. The error says which case you are in: - No client connected: "Connection timeout - clearing N queued @ mentions" (the same text as before). - A client connected that is not ready yet: "Send timeout - clearing N queued @ mentions that the connected Claude did not take in time". Before this change, each handshake stopped the connection timeout. Clients that connected and left without overlapping (for example a new client every 1000 ms that stays 300 ms) held a mention for as long as they kept doing it, with no error. They still never become ready, so the mention leaves with an error at its deadline. Another client's handshakes no longer delay a queued mention. A mention goes out once some connected client is ready. The broadcast then reaches every connected client, including one that connected later and is still in its own wait. Before, while one Claude stayed connected, each handshake of another client restarted the wait of a flush that was already due. When libuv refuses a write at once, you now see an error too. luv returns nil and the error for such a write and never runs its callback. `send_message` ignored that return, so `broadcast` never reported, and the queue dropped the mention without a word. ### Behavior changes 1. A drop no longer gives a queued mention a fresh `connection_timeout`. The deadline counts from the send. 2. Mentions sent at different times time out at different times. Before, one timeout from the first queued mention cleared them all. These fix the Codex round-6 finding on coder#454 ([thread](coder#454 (comment))), which the user waived for coder#454 so that it ships here. They also fix a gap the advisor on coder#454 found, the Codex round-1 finding on this PR, and the verifier's findings on 0585211, d1a6724 and cefe258. ## Change - `init.lua` `queue_mention`: it stamps each mention with its deadline, and starts `M.state.connection_timer` when it is not running. - `init.lua` `expire_mentions`, the `connection_timer` callback: while no ready client is connected, it clears the queued mentions whose deadline passed, with one error, and starts the timer again for the oldest mention left. When the oldest mention went out since, it clears nothing. While a ready client is connected, it clears nothing, makes sure a flush is due, and stops. - `init.lua` `flush_mention_queue`: it sends the oldest mention only once some connected client is ready (`ms_until_a_client_is_ready`). Otherwise it waits for the first such moment and checks again then. A flush that finds no ready client calls `expire_mentions`, so the mentions whose deadline passed while a ready client took the queue leave at once. - `init.lua` `schedule_mention_flush`: it no longer starts or stops the timeout while the queue holds a mention. The bound on the wait for a ready client (`ready_wait_since`) is gone, as the deadline covers it. - `init.lua` `M.process_mention_queue(true)`, the handshake hook: it no longer restarts the flush timer. - `server/client.lua`: a client records `connected_at` when its handshake completes, and `get_client_info` returns it. - `server/client.lua` `send_message`: it passes the error of a write that libuv refuses at once to the callback. `broadcast` then counts that write as failed and still calls `on_written` once. Main added a `write` helper that every socket write goes through (coder#467). It now returns what `tcp_handle:write` returned, and it stops a large frame at the first piece that libuv refuses at once (Codex round 4, hardening: libuv refuses all pieces or none, and `at_mentioned` frames are never split). - `config.lua` and `dev-config.lua`: the `connection_timeout` comment says what the setting does now. - `types.lua`, the comments in `init.lua` and `server/client.lua`, and `lua/claudecode/README.md` state the rules above. - `fixtures/issue-70/README.md` names the deadline and `expire_mentions` in place of the removed `start_connection_timeout_if_needed`. ## Tests All tests are in `tests/unit/mention_queue_spec.lua` unless noted. The tests run the real server code on a fake libuv loop, so each time below is exact. Tests that fail on cefe258, the previous head: - `F1: 100 mentions sent at once all reach a Claude whose handshake comes 8000 ms later`, and the same at 9800 ms. - `F1: when a ready Claude leaves after the deadline, the rest leave at the next flush`: one error, within 25 ms of the drop, for every mention it did not get. - `F1: when a ready Claude leaves after the deadline while another waits, the rest leave at once`: the same, while a second Claude that is not ready yet is connected. - `D: a Claude that gets ready just at the deadline gets the mention`. - `F1: a ready Claude that leaves before its handshake callback ran does not strand the queue`. The verify-mention-queue model found this path once I gave it the drain rule: Neovim runs the handshake's `on_open` callback late when its loop was busy, so the deadline can find Claude ready before any flush is due. Without the flush that the spared deadline now schedules, a Claude that left before `on_open` ran left the queue with nothing that sent or cleared it. - In `tests/unit/server/connection_lifecycle_spec.lua`: `stops at a piece that libuv refuses at once, and passes its error to the callback once`. On real Neovim 0.12.3, with the plugin's own timers and a loopback WebSocket client: 100 mentions sent at once, and a handshake 8.6 s later. On this head all 100 arrive, in order, with no error. On cefe258, 36 arrive, and at 10.6 s you see "Send timeout - clearing 64 queued @ mentions that the connected Claude did not take in time". Tests that fail on d1a6724: - `S: clients that connect every <period> ms and stay <life> ms do not hold a mention past its deadline`, for 1000/300, 700/300, 650/500 and 900/100 ms: no two clients connected at once. The mention is sent 1 ms after the first handshake. Each test expects one error at 10601 ms, and no client receives the mention. - `S: clients that overlap but each leave before they are ready do not hold a mention past its deadline`: a new client every 200 ms that stays 300 ms. One error at 10601 ms, with the Send timeout text. - `A, F4: a Claude whose handshake comes 10.3 s after the send is not ready by the deadline: you see an error` - `H: a handshake and a drop just before the deadline do not move it` - `B: mentions sent 5 s apart with no Claude each time out at their own deadline`: errors at 10.6, 15.6 and 20.6 s. - `B: of two mentions sent 5 s apart, a Claude ready between their deadlines gets the second` - `B, C: :ClaudeCodeStop drops the deadline of the old mention: a mention sent after a restart gets its own` - `C: a stop cancels a deadline whose callback already waits for the main loop` - `F1: when a ready Claude leaves in the middle of the queue, the rest leave at their deadline`: one error at 10.6 s for every mention it did not get. It passes on cefe258. Tests that pass on d1a6724 and pin a rule: - `A: a Claude whose handshake comes 9.9 s after the send is ready at 10.5 s and gets the mention` - `B, control: the deadline of a mention that went out clears no later mention` - `E: a send while a flush is due does not postpone that flush`. It kills the `queue_mention` mutant that the verifier found surviving (`F2-send-restarts-flush` below). Tests from earlier rounds: - `D: handshakes of other clients do not postpone a flush that is due for a connected Claude`. It fails on 3f42e01, the last coder#454 head. - `D: when the Claude a flush was kept for leaves, a newly connected Claude still gets connection_wait_delay`. It fails on 7e8860c, the first head of this PR. - The readiness rule: `D: a Claude whose handshake came 700 ms after its TCP connect still gets connection_wait_delay`, `D: a Claude whose CLOSE frame arrives as a flush is due does not count as ready`, `D: when the Claude a flush waits for leaves during the wait, the next Claude gets its own wait`, and `D: a Claude that answered a ping just now has still been connected since its handshake`. - `H: a write that libuv refuses at once shows an error too`, and a `server_spec.lua` case where one client's write is refused and another's succeeds: `on_written` runs once, with 1. The fake loop fails a test when its timers keep firing at one moment, so a mutant that loops makes a test fail instead of hanging the run. Three earlier tests contradicted the final rules, and I replaced them: "H: after a drop in the wait, the mention gets a whole connection_timeout for Claude to come back", "B, control: the connection timeout runs from the first queued mention, not from the latest", and, on cefe258, "D: a Claude that gets ready just at the deadline is too late". I removed "C: a flush that the deadline cancelled does not send a mention sent right after the deadline": its path no longer exists, as no deadline clears a mention while a ready Claude is connected. Mutants: I ran 47 mutants of the queue, deadline, drain, readiness, broadcast and write-report code. Each mutant changes one guard alone. 46 of them make at least one test fail. `no-identity-check` survives. `start_timer` runs a callback only while its timer is still the one in `M.state`, and the mutant drops that check, so a stale flush or deadline callback runs once more. Every queue callback re-checks the queue and the clients, and no deadline clears a mention while a ready client is connected. So a stale callback can no longer send a mention early or clear one, and I found no path that tells the two apart. I kept the check: without it, a stale callback stops the live timer of its name. `C2-connected-at-accept` now sets `connected_at` from `client.last_pong`, which after coder#488 holds the time of the TCP accept (or of the last pong). Before, it left `connected_at` nil and duplicated `connected-at-unset`. The definitions follow, as the code each mutant replaces (`-`) and its replacement (`+`). A mutant with no `+` lines deletes the code. <details> <summary>The 47 mutants</summary> 1. `closing-counts` in `init.lua` ```diff - takes no frames. - if info.state == "connected" and info.handshake_complete == true then + takes no frames. + if (info.state == "connected" or info.handshake_complete == true) and info.handshake_complete == true then ``` 2. `no-identity-check` in `init.lua` ```diff - if M.state[name] == timer then + if true then ``` 3. `flush-ignores-broadcast-result` in `init.lua` ```diff - if not server.broadcast("at_mentioned", params, report_unwritten("queue", mention.file_path)) then + if not (server.broadcast("at_mentioned", params, report_unwritten("queue", mention.file_path)) or true) then ``` 4. `stop-keeps-queue` in `init.lua` ```diff - -- Clear the queued @ mentions and stop the queue's timers: nothing queued before the stop reaches Claude - clear_mention_queue() ``` 5. `queued-path-raw` in `init.lua` ```diff - queue_mention(mention.file_path, mention.start_line, mention.end_line) + queue_mention(file_path, start_line, end_line) ``` 6. `immediate-overtakes` in `init.lua` ```diff - if immediate and #mention_queue() == 0 then + if immediate then ``` 7. `no-on-open` in `server/client.lua` ```diff - if on_open then - on_open(client) - end ``` 8. `broadcast-always-true` in `server/init.lua` ```diff - return tcp_server.broadcast(M.state.server, json_message, on_written) > 0 + tcp_server.broadcast(M.state.server, json_message, on_written) + return true ``` 9. `tcp-broadcast-counts-closing` in `server/tcp.lua` ```diff - if client.state == "connected" then - sent = sent + 1 + if true then + sent = sent + 1 ``` 10. `bad-path-queued-anyway` in `init.lua` ```diff - if not mention then - return false, format_error - end - queue_mention(mention.file_path, mention.start_line, mention.end_line) + mention = mention or { file_path = file_path, start_line = start_line, end_line = end_line } + queue_mention(mention.file_path, mention.start_line, mention.end_line) ``` 11. `tcp-broadcast-ignores-on-written` in `server/tcp.lua` ```diff - if on_written then - pending = pending + 1 + if false then + pending = pending + 1 ``` 12. `tcp-broadcast-reports-before-writes` in `server/tcp.lua` ```diff - if dispatched and not reported and pending == 0 and sent > 0 then + if dispatched and not reported and sent > 0 then ``` 13. `tcp-broadcast-counts-failed-writes` in `server/tcp.lua` ```diff - if not err then - written = written + 1 - end + written = written + 1 ``` 14. `unwritten-silent` in `init.lua` ```diff - logger.error(component, "Claude's connection failed + logger.debug(component, "Claude's connection failed ``` 15. `mock-broadcast-no-report` in `server/mock.lua` ```diff - if written > 0 and on_written then + if false then ``` 16. `immediate-on-written-noop` in `init.lua` ```diff - M.state.server.broadcast("at_mentioned", params, report_unwritten("command", formatted_path)) + M.state.server.broadcast("at_mentioned", params, function() end) ``` 17. `immediate-reports-raw-path` in `init.lua` ```diff - report_unwritten("command", formatted_path) + report_unwritten("command", file_path) ``` 18. `tcp-broadcast-no-dispatched-guard` in `server/tcp.lua` ```diff - if dispatched and not reported and pending == 0 and sent > 0 then + if not reported and pending == 0 and sent > 0 then ``` 19. `send-message-ignores-refusal` in `server/client.lua` ```diff - if not queued and err and callback then + if false then ``` 20. `flush-ignores-readiness` in `init.lua` ```diff - if wait and wait > 0 then + if false then ``` 21. `readiness-uses-newest-client` in `init.lua` ```diff - wait = wait and math.min(wait, left) or left + wait = wait and math.max(wait, left) or left ``` 22. `handshake-restarts-flush` in `init.lua` ```diff - schedule_mention_flush(M.state.config.connection_wait_delay) - else + stop_timer("mention_timer") + schedule_mention_flush(M.state.config.connection_wait_delay) + else ``` 23. `connected-at-unset` in `server/client.lua` ```diff - client.connected_at = vim.loop.now() ``` 24. `C2-connected-at-accept` in `server/client.lua` ```diff - client.connected_at = vim.loop.now() + client.connected_at = client.last_pong ``` 25. `I4-closing-counts-ready` in `init.lua` ```diff - if info.state == "connected" and info.handshake_complete == true and info.connected_at then + if info.handshake_complete == true and info.connected_at then ``` 26. `I9-readiness-from-last-pong` in `init.lua` ```diff - local left = math.max(0, info.connected_at + M.state.config.connection_wait_delay - vim.loop.now()) + local left = math.max(0, info.last_pong + M.state.config.connection_wait_delay - vim.loop.now()) ``` 27. `I12-no-recheck-after-wait` in `init.lua` ```diff - local wait = ms_until_a_client_is_ready() - if wait and wait > 0 then + local wait = not M.state.skip_ready_check and ms_until_a_client_is_ready() + M.state.skip_ready_check = nil + if wait and wait > 0 then + M.state.skip_ready_check = true ``` 28. `no-remove-head` in `init.lua` ```diff - table.remove(queue, 1) - logger.debug("queue", "Sent queued + logger.debug("queue", "Sent queued ``` 29. `send-restarts-flush-v2` in `init.lua` ```diff - elseif M.is_claude_connected() and not M.state.mention_timer then + elseif M.is_claude_connected() then ``` 30. `F2-send-restarts-flush` in `init.lua` ```diff - start_timer("connection_timer", timeout, expire_mentions) - end - schedule_mention_flush(debounce_delay) + start_timer("connection_timer", timeout, expire_mentions) + end + stop_timer("mention_timer") + schedule_mention_flush(debounce_delay) ``` 31. `clear-keeps-deadline` in `init.lua` ```diff - M.state.mention_queue = {} - stop_timer("mention_timer") - stop_timer("connection_timer") + M.state.mention_queue = {} + stop_timer("mention_timer") ``` 32. `empty-queue-keeps-deadline` in `init.lua` ```diff - if #mention_queue() == 0 then - stop_timer("mention_timer") - stop_timer("connection_timer") + if #mention_queue() == 0 then + stop_timer("mention_timer") ``` 33. `timeout-silent` in `init.lua` ```diff - logger.error("queue", "Connection timeout - clearing " + logger.debug("queue", "Connection timeout - clearing " ``` 34. `send-timeout-silent` in `init.lua` ```diff - logger.error( - "queue", - "Send timeout + logger.debug( + "queue", + "Send timeout ``` 35. `F4-connection-text-while-connected` in `init.lua` ```diff - if M.is_claude_connected() then - logger.error( + if false then + logger.error( ``` 36. `deadline-restarts-on-send` in `init.lua` ```diff - if not M.state.connection_timer then - start_timer("connection_timer", timeout, expire_mentions) - end + start_timer("connection_timer", timeout, expire_mentions) ``` 37. `deadline-without-wait-delay` in `init.lua` ```diff - local timeout = M.state.config.connection_timeout + M.state.config.connection_wait_delay + local timeout = M.state.config.connection_timeout ``` 38. `handshake-stops-deadline` in `init.lua` ```diff - if from_new_connection then - schedule_mention_flush + if from_new_connection then + stop_timer("connection_timer") + schedule_mention_flush ``` 39. `handshake-moves-deadline` in `init.lua` ```diff - if from_new_connection then - schedule_mention_flush + if from_new_connection then + local timeout = M.state.config.connection_timeout + M.state.config.connection_wait_delay + for _, queued in ipairs(mention_queue()) do + queued.deadline = vim.loop.now() + timeout + end + if #mention_queue() > 0 then + start_timer("connection_timer", timeout, expire_mentions) + end + schedule_mention_flush ``` 40. `expire-clears-whole-queue` in `init.lua` ```diff - while expired < #queue and queue[expired + 1].deadline <= now do + while expired < #queue do ``` 41. `expire-keeps-mentions` in `init.lua` ```diff - for _ = 1, expired do - table.remove(queue, 1) - end ``` 42. `expire-no-rearm` in `init.lua` ```diff - else - start_timer("connection_timer", queue[1].deadline - now, expire_mentions) - end + end ``` 43. `expire-rearms-for-newest` in `init.lua` ```diff - start_timer("connection_timer", queue[1].deadline - now, expire_mentions) + start_timer("connection_timer", queue[#queue].deadline - now, expire_mentions) ``` 44. `F1-expire-while-ready` in `init.lua` ```diff - if ms_until_a_client_is_ready() == 0 then + if false then ``` 45. `F1-wait-keeps-overdue` in `init.lua` ```diff - expire_mentions() - if #mention_queue() > 0 then + if #mention_queue() > 0 then ``` 46. `F1-no-client-keeps-overdue` in `init.lua` ```diff - logger.debug("queue", "No connected client took queued @ mention: " .. mention.file_path) - expire_mentions() - + logger.debug("queue", "No connected client took queued @ mention: " .. mention.file_path) + ``` 47. `F1-spare-without-flush` in `init.lua` ```diff - schedule_mention_flush(inter_message_delay) - return - end - local queue = mention_queue() + return + end + local queue = mention_queue() ``` </details> ## Validation All on the pushed head, after merging main at 09b78fd. coder#488 on main removed `client.last_pong = vim.loop.now()` from the 101 write callback, so the merge sets `client.connected_at = vim.loop.now()` there, the handshake time as before. Outside `covered.lock` and that line, the change of this PR is the same as at 3de15f5, apart from index lines and hunk offsets: - luacheck on `lua/` and `tests/`: 0 warnings / 0 errors in 173 files - busted, full suite, shuffled: 1516 successes / 0 failures / 0 errors / 20 pending, with `--coverage` (seed 1794411584) and without (seed 12345) - Real-Neovim integration tests (Neovim 0.12.3): 313 success, 0 failed - `treefmt --ci`: 0 files changed - The 47 mutants: 46 killed, 1 survived (`no-identity-check`, see above) - Real Neovim 0.12.3, 100 mentions at once and a handshake 8.6 s later: 100 received, in order, 0 errors - `verify-diff-lifecycle`: I re-recorded `covered.lock` after each change to a covered file, and `check.sh` passes. - `verify-mention-queue` (the model for the skill PR that follows this one, not in this PR): every TLC check passes on this code, with the drain rule and its three new guards. `check.sh` still exits 3 (STALE) on this head, because the skill's `covered.lock` needs a re-record. The skill PR does that. --- _Generated with [`xum`](https://github.com/coder/xum) • Model: `anthropic:claude-opus-5-5` • Thinking: `xhigh`_

…n tracking (coder#477) ## Status coder#524 is merged (`a41254a4`). It changed the flush on visual exit: the changedtick comparison is gone, and a `visual_entry` that the buffer listener marks takes its place. This PR models it. Codex round 4 (`91660323`) raised two P2 threads, fixed in round 5 (`f974ee06`: both lanes clean). The Opus and GPT verifiers of `f974ee06` found one documentation defect and three minors, fixed in this round 6 (the last). The replays also found a family of bugs that coder#524 left: any edit made while you select whose check has not run when the next key arrives. Three are reproduced (a mapping, a key that arrives during the plugin's callback, an autocmd edit at a mode change), and fix PR coder#540 fixes all three. Their replays print `BUG` on `main` until coder#540 merges. ## What this adds `.agents/skills/verify-selection-tracking/`: a TLA+ model of what Claude sees as the user's current selection (`lua/claudecode/selection.lua`), checked by TLC against guards that `check.sh` reads from the Lua code, on the shared harness from coder#450. The model has no clock, so it covers every `visual_demotion_delay_ms`. A change that removes or rewords a guard makes a rule break or the covered code read STALE. The model describes `main` as it is now: the four bugs it found are fixed (coder#452), and so are the cases that reviews found afterwards (coder#471, coder#481, and the recursion of coder#481's code that coder#493 fixed). ## The ten rules, as plain sentences | Rule | Plain sentence | | --- | --- | | `ReleaseSent` | Right after you release a selection in a file (Esc), Claude holds it, also when you made it faster than the 100 ms debounce (issue coder#246), and when a plugin edited another line or a `:write` ran while you selected. | | `NoPhantomSelection` | Claude only gets text you selected, never the text at the `'<,'>` marks after an operator such as `d` changed it. | | `NoTerminalSelection` | Claude never gets a selection in the Claude terminal buffer. | | `HeldUntilMoved` | Once events settle in a file, a selection you released stays with Claude while the cursor has not moved and its text is unchanged. | | `HeldInTerminal` | Once events settle in the Claude terminal, Claude still holds the selection you released while its text is unchanged. | | `HeldEndsWhenMoved` | Once events settle in a file, Claude holds a released selection only while the cursor has not moved since you released it. | | `SameFile` | Once events settle in a file, Claude's selection is in that file. | | `ClaudeSeesCursor` | Once events settle in a file, a cursor-only selection that Claude holds is where the cursor is, and in visual mode Claude holds the live selection. | | `NoDeletedText` | Once events settle, Claude holds no selection text that its buffer no longer has. | | `TimerClosedOnce` | No timer handle is closed twice (Neovim would raise `handle ... is already closing`). | "Once events settle" means no debounce or demotion timer runs, no timer callback waits in the `vim.schedule` queue, and the check that the buffer listener queued with `vim.schedule` has run. ## Bugs this model found The first version of the model broke four rules on the code before coder#452. Each path was replayed on Neovim 0.12.3. **coder#452 fixed all four**: 1. `HeldEndsWhenMoved`: Claude kept a released selection after the cursor left it (`vb` Esc `gv` `d`, or `ve` Esc `l` `h` inside 100 ms). 2. `NoDeletedText`: Claude kept a held selection after you edited its text without moving the cursor (`viw` Esc `x` `x`). 3. `SameFile`: with a long `visual_demotion_delay_ms`, Claude held another file's cursor (`:b b.txt`, `:b a.txt`). 4. `ClaudeSeesCursor`: with a long `visual_demotion_delay_ms`, Claude held a cursor position you had left (Esc `l`, wait, `h`). **coder#471** closed the case a Codex review of coder#452 found: an operator consumes a second selection and you enter the Claude terminal within the debounce. The model's flush-skip step (`FlushSkipReports`) describes the fixed code, and `tests/integration/selection_held_spec.lua` replays the path with a real terminal buffer. **coder#481** closed the case a reviewer of this PR found, and no step of the model could express it: Claude holds selection A, you go to the Claude terminal, and A's file changes while you are there (Claude rewrites it and Neovim reloads it, or a plugin deletes the selected text). Claude kept the deleted text until you came back. The model now has a step for it (`YouEditOtherBuffer`) and three facts: `ListensToSelectionBuffer`, `TerminalReportsHeldBuffer` and `UpdateChecksHeldText`. `replays/held_after_reload_in_terminal.lua` and `replays/held_after_edit_in_terminal.lua` replay the two triggers on real Neovim. **coder#524** closed the case an advisor of this PR found, and no step of the model could express it: you select, a plugin edits another line (or a `:write` runs) while you are still in visual mode, and you press Esc inside the 100 ms debounce. The flush took a moved changedtick for an operator that consumed the selection, so Claude got the cursor and not the selection. The model now has two steps that move only the changedtick (`YouEditByPluginInVisual`, `YouWriteInVisual`) and three facts for the new code (`FlushSkipsOperator` rewritten, `ListenerNotesVisualEdit`, `VisualCheckSparesPluginEdit`). `FlushIgnoresTick` is the old comparison as a fact: it reads `FALSE` on the code before coder#524, and the model then breaks `ReleaseSent` and `HeldUntilMoved` (`NoPhantomSelection` still holds, because the old guard did stop operators). Three replays (`release_after_plugin_edit_in_visual.lua`, `release_after_plugin_append_in_visual.lua`, `release_after_write_in_visual.lua`) print `BUG` on `fcea49af` (the commit before coder#524) and `OK` on `main`, on Neovim 0.12.3 and 0.8.0. **Still open, found by the replays:** the flush on Esc skips a selection that has an edit nobody checked yet, and the check that clears a plugin's edit runs in `vim.schedule`, after the command or callback that made the edit returns. When a key comes first, the flush takes the edit for an operator's and Claude gets the cursor, not the selection, although its text is untouched. The model runs that check in the step of the edit, so it does not show this, and a PASS says nothing about it. Three ways to get there print `BUG` on Neovim 0.8.0 and 0.12.3 (3 of 3 runs each): a mapping that edits another line and presses Esc in one typeahead (`release_in_same_typeahead_as_plugin_edit.lua`), a key that arrives while a timer callback of the plugin still runs (`release_with_key_during_plugin_callback.lua`, with `nvim_input`; the Opus verifier found it with an attached UI), and an autocmd that edits when visual mode starts with the Esc already in the typeahead (`release_after_autocmd_edit_in_visual.lua`, a `ModeChanged` handler for `n:v`; the GPT verifier found it). In a tree with coder#540 (a `vim.on_key` listener runs the check at the next key) all 16 replays print `OK` on both versions. A plugin edit whose check runs before the next key is not affected (`release_after_plugin_edit_in_visual.lua`). **coder#457** and **coder#463** changed `getCurrentSelection` and moved the terminal check into `M.is_claude_terminal_buffer`. The model follows that move (`FlushSkipsTerminal`, `UpdateSkipsTerminal`). It makes no claim about what `getCurrentSelection` answers when nothing is tracked. ## What changed from the model that found those bugs - The model now describes the fixed code: `clear_held_state`, `reconcile_held_selection` (called from `CursorMoved`, `BufEnter` and `TextChanged`), the changedtick record `selection_tick`, `cursor_at_flush.left` and `.away`, and the flush-skip report. That adds nine facts (21 in all), the coder#481 guards add three (24 in all), and the coder#524 guards add three more (27 in all). - `SameFile` and `ClaudeSeesCursor` no longer break on the code as written. The special case that ran their mutants with `DelayBelowDebounce = TRUE` is gone, and the check uses `FALSE` (every delay). - Five guards break no rule alone, because another guard covers for them (`FlushSkipReports` only together with `EntryClearsHeld`). `--mutants` removes each with its partner (four `A+B` keys in `EXPECT`): `DemotionClearsHeldState` + `MoveReports` and `PendingClearsHeld` + `ReconcileOnCursorMoved` break `ClaudeSeesCursor`, `ElseClearsHeldState` + `LeaveNoted` breaks `SameFile`, `EntryClearsHeld` + `FlushSkipReports` breaks `HeldEndsWhenMoved`. I found these pairs by running each such guard together with each other guard. SKILL.md lists them. - The model has a `YouEditByPlugin` step: `TextChanged` without `CursorMoved`. In the model, `ReconcileOnTextChanged` and `TextChangeReports` each break `NoDeletedText` alone because of it. On real Neovim they do not: the buffer listener (`on_lines`) also fires for an edit of the current buffer and runs the same check. `replays/held_after_plugin_edit.lua` prints `OK` with either call removed from `lua/` (I removed each: all 18 replay runs print `OK`, while `check.sh` reports `BROKEN: NoDeletedText`). So a `BROKEN` trace for these two guards is a counterexample of the model, not a failure of the running plugin. SKILL.md says so. `--mutants` still requires both guards, because the model has no other way to end the hold at that edit. - The model keeps the changedtick as one bit on the visual entry ("moved since visual mode started"), not as a number per buffer: the code before coder#524 only compared it with the value recorded at entry, and a changedtick only grows. A number per buffer multiplies the states and the `--mutants` time by an estimated 5 to 10 and adds no behavior (I did not build it). The bit is kept only while an entry exists and a guard reads it, so the main run has fewer states (129,986) than before (178,962). - `LeaveNoted` breaks `HeldEndsWhenMoved` alone only when the user can visit a second file, so `--mutants` runs that rule with two files. - The model has a `YouEditOtherBuffer(b)` step: the text of a buffer that is not current changes, `TextChanged` does not fire for it, and the plugin sees the change only through its `nvim_buf_attach` listener (`on_lines`, `on_reload`, `on_detach`) or when you come back. The listener only queues its check with `vim.schedule`, so the model sets a queued-check bit at the edit and runs the check in its own step (`ListenerCheckRuns`), after any other step (Codex round 2). `ListensToSelectionBuffer`, `TerminalReportsHeldBuffer` and `UpdateChecksHeldText` are the guards of coder#481 that break `NoDeletedText` when removed. - `HeldInTerminal` is new in this round (Opus verifier). `HeldUntilMoved` only holds in a file, so two regressions that drop a released selection in the Claude terminal passed every rule: `update_selection` in the terminal that reports the cursor although the text did not change, and a demotion in the terminal that publishes the cursor of the held buffer. The new rule says that Claude keeps the selection there. It passes on the model, and six guard removals break it, so it is not vacuous. - The 16 replays (`replays/`) exit 0 on `OK` and 1 on `BUG`. Eleven replay a path that once broke a rule and show the promise kept (the three added for coder#524 are the plugin edit, the plugin append and the `:write` in visual mode). `held_after_line_inserted_above.lua` (a line inserted above a held selection makes Claude lose the selection and get the cursor, although the text still exists) and `v_escape_selects_one_character.lua` (a bare `v` and Esc selects the character under the cursor, so it is a selection) show things that are not rules. Three replay known bugs and print `BUG` until coder#540 merges (see "Still open"). `replays/run.sh` works without GNU `timeout` (macOS) and with a checkout path that has a space, a comma or a quote (Codex round 2). ## Proof All on this branch, Neovim 0.12.3, Java from mise: - `check.sh`: `main: pass (129986 distinct states found)`, `== RESULT: PASS` (exit 0, a fresh lock), all 27 facts `TRUE`. - `check.sh --mutants` (4486 s, about 75 min, at a load average of 22 to 31): 26 keys (22 single guards and four `A+B` pairs), `== mutants: every guard is caught`, no rule is vacuous (exit 0). The new facts are caught as `EXPECT` says: `FlushSkipsOperator` and `ListenerNotesVisualEdit` break `NoPhantomSelection`, `VisualCheckSparesPluginEdit` and `FlushIgnoresTick` break `ReleaseSent`. The run is on `c731ebae`. Since then the model changed only in its comments (the spec without comments is identical, and `check.sh` still reports 129,986 states), and `check.sh` changed in one regex and its comment (the `ListensToSelectionBuffer` regex now reads both forms of `on_lines`, see below). The TLC inputs of `--mutants` (model, constants, `EXPECT`, and the fact values, which are all `TRUE` on `main`) are the same, so I did not run it again. The verifiers ran it on `f974ee06` (Opus 5075 s, GPT 5201 s): 26 keys caught, exit 0. - The code before coder#524: `check.sh` runs on the `selection.lua` of `fcea49af` once two stand-in blocks (`visual_entry_of`, `note_visual_edit`, which the old code does not have) are added at the end of the file. Exactly four facts read `FALSE`: `FlushSkipsOperator`, `ListenerNotesVisualEdit`, `VisualCheckSparesPluginEdit` and `FlushIgnoresTick`. `check.sh` exits 1 with `main: BROKEN: ReleaseSent`, the first broken rule it prints (trace: you select, a plugin edits another line, you press Esc). TLC with that fact set breaks `ReleaseSent` and `HeldUntilMoved` (the Opus and GPT verifiers ran it too), `--mutants` lists `HeldInTerminal` as well for `FlushIgnoresTick`, and `NoPhantomSelection` holds. Putting the old comparison back into the `selection.lua` of this tree gives the same: `check.sh` exits 1, `FlushSkipsOperator FALSE`, `FlushIgnoresTick FALSE`, `main: BROKEN: ReleaseSent`. - Each new guard removed alone from `selection.lua` flips only its own fact: the flush condition (`FlushSkipsOperator`, `main: BROKEN: NoPhantomSelection`), the `note_visual_edit(entry)` call in `on_lines` (`ListenerNotesVisualEdit`, `NoPhantomSelection`), and the mode test of the check (`VisualCheckSparesPluginEdit`, `ReleaseSent`). - Scratch breaks on this tree (edit `lua/`, run, then `git checkout -- lua/` and an empty `git diff --shortstat`): - Dropping `reconcile_held_selection(not entered_buffer)` from `M.on_cursor_moved`: `check.sh` exits 1, `ReconcileOnCursorMoved FALSE`, `main: BROKEN: HeldEndsWhenMoved`, and `replays/held_after_quick_move.lua` prints `BUG the cursor moved after the release, but Claude still holds "alpha"`. - Making the `selection_text_is_there` test in `demote_if_selection_text_changed` always true: `check.sh` exits 1, `TextChangeReports FALSE`, `main: BROKEN: NoDeletedText`, and `replays/held_after_edit.lua` prints `BUG Claude holds "alpha" at 0-5, the buffer has "alphb" there`. - Dropping `watch_selection_buffer(bufnr)` from `record_selection_read`: `check.sh` exits 1, `ListensToSelectionBuffer FALSE`, `main: BROKEN: NoDeletedText`, and `replays/held_after_reload_in_terminal.lua` prints `BUG Claude holds "alpha", but a.txt is "beta gamma"`. - `scripts/tla/test-check-lib.sh`: `COUNT cases=44 failed=0 skipped=0`. - Replays: 16 probes on Neovim 0.12.3 and 0.8.0, each at the default delay and with `DELAY_MS=50` (that setting changes only the two long-delay probes): 13 print `OK` and the three known-bug probes print `BUG` (coder#540). On `fcea49af` the three probes for coder#524 print `BUG` on both versions. In a tree with coder#540 (a scratch copy of the skill, not part of this PR) all 16 print `OK` on both versions, and the two new known-bug replays ran 4 times each on both versions with the same result. - At `91660323`, a script that removed each of the 24 guards from `selection.lua` alone showed that exactly its own fact turns `FALSE` (seven regexes read a second guard before; the Opus verifier found three of them). The regexes of `FlushOnVisualExit`, `ReconcileOnCursorMoved` and `ReconcileOnTextChanged` are anchored now, because a commented-out handler call used to leave the fact `TRUE`: with each call commented out in `selection.lua`, only its own fact reads `FALSE`. This round I did the same by hand for the three new guards (see above), and I rewrote the `ListensToSelectionBuffer` regex twice: in round 5 for the code after coder#524 (`on_lines` and `on_reload` call `check_soon` inside `if holds_selection_of(buf) then`), and in this round to read both forms (it read `FALSE` on the `selection.lua` of `fcea49af`, which listens). It is `TRUE` on `fcea49af` and on this head, and `FALSE` when `check_soon()` is removed from `on_lines` or from `on_reload`, and when `watch_selection_buffer(bufnr)` is removed from `record_selection_read` (only its own fact in each case). - `shfmt -i 2`, `shellcheck --exclude=SC1091,SC2016`, `stylua --check`, `prettier --check` and `treefmt --ci` (379 files, 0 changed): clean. `luacheck` 0 warnings in 181 files. `tests/selection_test.lua` and `tests/unit/visual_delay_timing_spec.lua`: 156 successes, 0 failures. This PR changes no `lua/` or `tests/` file. - `covered.lock` is recorded last. This round the flush, `on_mode_changed` and `watch_selection_buffer` blocks changed (coder#524), and `visual_entry_of` and `note_visual_edit` are new blocks. The file hashes of `init.lua` and `server/init.lua` changed with `main`. In round 6 the `on_connect` block changed too (coder#539 moved a debug log line: no send, no timer, no selection state), and the lock is re-recorded. I merged `origin/main` several times and read each diff of the covered code: coder#454 (`server.broadcast` returns, mention queue), coder#481, and coder#493, whose change in `demote_if_selection_text_changed` made the regex of `TerminalReportsHeldBuffer` read `FALSE`. I re-pointed it and re-recorded the lock. coder#467 and coder#491 touch no covered file of this skill. coder#497 changed one debug log argument in the `tools/call` handler of `server/init.lua`, and coder#499 changed the disconnect cleanup in the same file (`on_disconnect`: a client without a handshake owns no diff, and the cleanup waits until Neovim allows window changes). Both are outside `M.broadcast` and the `on_connect` callback, and neither can reach the selection state, a timer or a send, so only the file hash changed and I re-recorded the lock. ## Run it ```bash .agents/skills/verify-selection-tracking/check.sh # about 1 min .agents/skills/verify-selection-tracking/check.sh --mutants # about 1 to 1.5 h (4486 s in the last run), after you edit the model or a fact .agents/skills/verify-selection-tracking/check.sh --hash-only # about 5 s, only compares covered.lock with the code NVIM=~/.local/share/mise/installs/neovim/0.12.3/bin/nvim \ .agents/skills/verify-selection-tracking/replays/run.sh held_after_operator.lua ``` CI runs every `.agents/skills/verify-*/check.sh` in the `covered-lock` job, as for `verify-diff-lifecycle`. ## Review record - Codex round 1 (`ac7f243`): clean in both lanes. - Codex round 2 (`f91391f`): security clean. Code lane, three P2s: the model ran the listener check atomically with the edit, `replays/run.sh` needed GNU `timeout`, and it put raw paths into Neovim commands. All three are fixed. - GPT and Opus verifiers on `f91391f`: ISSUES. F1 (SKILL.md scope omitted a held buffer that becomes a Claude terminal, now a scope bullet) and minors F3 to F10 are applied, except F4 (six blind-spot mutants remove a guard's effect without touching a line a fact reads: the fact stays `TRUE`, but `covered.lock` reads STALE, so `check.sh` exits 3, not 0). F2 and the GPT finding of the same kind stay a disclosed limit: the model runs the buffer listener only for a buffer that is not current, although `on_lines` also fires for an edit of the current buffer, so a `BROKEN` trace for `ReconcileOnTextChanged` or `TextChangeReports` is a counterexample of the model, not a failure of the running plugin (SKILL.md, "Read the result"). - Codex round 3 (`e18a1cf`): clean in both lanes. - GPT and Opus verifiers on `e18a1cf`: ISSUES. Opus N2 (impact: the `HeldUntilMoved` row promised more than its rule checks, and two regressions in the terminal passed): new rule `HeldInTerminal`, rows fixed, `--mutants` rerun. GPT F1 (impact: SKILL.md said a bare `v` and Esc keeps the held selection, but Claude gets the one selected character): the text now says what the code does, and a replay shows it. Minors fixed: N1 anchored autocmd-call regexes, N3 a demotion in a terminal that only its name marks does not take Condition 3, N4 "once events settle" includes the listener's queued check, N5 the shrink step names the three two-file rules, N6 the update step names the listener operators, N7 the `held_after_plugin_edit.lua` comment, N8 statechart labels for the listener steps, N9 user impact of the listener and `holdLoose` items, N10 the `--hash-only` time. - Codex round 4 (`91660323`): security clean. Code lane, two P2 threads, both fixed in this round: the Rules table delimiter (`2c88f30e`) and the model that restricted `YouEditByPlugin` to normal mode, so TLC could not reach a moved changedtick on release (`YouEditByPluginInVisual`, `YouWriteInVisual`, `FlushIgnoresTick`). - GPT and Opus verifiers on `91660323`: PASS, with minors. Fixed here: M1 the Rules table, M4 the `holdLoose` exemption names `HeldInTerminal`, M5 "the rows whose rule is `none`", M6 the return for an unloaded buffer in the Claude terminal is in the not-modeled list (I replayed it on 0.8.0 and 0.12.3). M2 and M3 (a regex that misses a blind-spot mutant or reads through a shared helper) are not changed: the lock reads STALE for them, as for F4 above. - Codex round 5 (`f974ee06`): both lanes clean, CI green, no open threads. - Opus and GPT verifiers on `f974ee06`: ISSUES, one documentation defect (F1) and three minors, all fixed in round 6. F1: SKILL.md said that an edit from a timer, a job or an autocmd cannot hit the same-typeahead bug. The true boundary is any edit whose check has not run when the next key arrives. Two more ways to get there are reproduced and have replays (a key that arrives during the plugin's callback, an autocmd edit at a mode change), the model, replay and SKILL.md text now say so, and coder#540 fixes all three. M1: `check.sh` prints only the first broken rule, and `--mutants` shows the others. M2: the operator order sentence (`on_lines` first, with the mode already normal, then `ModeChanged`) is fixed. M3: the `ListensToSelectionBuffer` regex and the old fact set (four facts, shown with `check.sh` itself). - Codex round 6: this head (the last round). ## Notes for the reviewer - The diff is one new skill folder: SKILL.md, `check.sh`, `covered.lock`, `model/` (the TLA+ spec and a `/statechart` view) and `replays/`. It touches no `lua/` code. - `DEVELOPMENT.md` is not edited here: the skill-listing change belongs to the PR that owns it. --- _Generated with [`xum`](https://github.com/coder/xum) • Model: `anthropic:claude-sonnet-5-5` • Thinking: `xhigh`_

… connection lifecycle (coder#474) 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`, coder#450), after `verify-diff-lifecycle`. It describes the keepalive as coder#488 merged it (d63c9b3, with the fix for the fresh clock at the tick). On the code of coder#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 coder#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 coder#455. Reviews of this PR then found four more false timeouts that the first model could not see. coder#479 and coder#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 coder#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 (coder#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 (coder#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 coder#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 coder#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 coder#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 coder#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 coder#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 coder#539 changed a log line in `on_open` and coder#558 answers in-flight requests before `stop_server`). The second merge made the ws lock stale once more: main's coder#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 (coder#544 and coder#577, terminal and diff files only) needed no new record. ## What changed since the first version of this PR - The model follows coder#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 (coder#467 handles that stall) and a client that writes data but never answers a ping, which coder#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 coder#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 coder#479 are gone, because coder#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 coder#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 coder#455 (3d4332c). `short-block-after-ping` keeps `2 of 3` on main before coder#479 (b65d266). `two-blocks-before-read` keeps `1 of 3` on the code of coder#479 on Neovim 0.8.3. `blocks-before-the-poll` keeps `0 of 3` on the first push of coder#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 coder#544) 1887 successes, 0 failures, 34 pending. The last merge (coder#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 ```bash .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`](https://github.com/coder/xum) • Model: `anthropic:claude-sonnet-5-5` • Thinking: `xhigh`_

ThomasK33 added 4 commits November 10, 2026 14:28

Merge remote-tracking branch 'origin/main' into fix/server-bound-stal…

26e4b3d

…led-write-queue

Merge remote-tracking branch 'origin/main' into fix/server-bound-stal…

51fee90

…led-write-queue

style(tests): apply the second stylua pass to connection_lifecycle_spec

c3c934e

stylua needs two passes on one assertion. The first pass left a layout that treefmt --ci (the format-check job) formats again.

Merge remote-tracking branch 'origin/main' into fix/server-bound-stal…

39a4a77

…led-write-queue # Conflicts: # .agents/skills/verify-diff-lifecycle/covered.lock

ThomasK33 closed this Nov 10, 2026

ThomasK33 reopened this Nov 10, 2026

ThomasK33 added 2 commits November 10, 2026 17:25

Merge remote-tracking branch 'origin/main' into fix/server-bound-stal…

251a10d

…led-write-queue # Conflicts: # .agents/skills/verify-diff-lifecycle/covered.lock

test(server): give the broadcast fixtures queued_bytes

6d6293a

Clients built by hand in server_spec write through client.write, which counts the bytes in client.queued_bytes.

chatgpt-codex-connector Bot reviewed Nov 10, 2026

View reviewed changes

Comment thread lua/claudecode/server/client.lua Resolved

ThomasK33 added 3 commits November 10, 2026 18:25

Merge remote-tracking branch 'origin/main' into fix/server-bound-stal…

6259bca

…led-write-queue

chore(verify): re-record covered.lock for the piece-wise writes

a6d7313

ThomasK33 added 11 commits November 11, 2026 02:27

Merge remote-tracking branch 'origin/main' into own-467-freshpoll

aab573a

docs(server): state the deadline race of the look and the bound under…

ead1701

… a run of wake ticks

chore(verify): re-record covered.lock for the wake run rule and the d…

905d002

…ead last_drain store

chore(verify): re-record covered.lock for the wake tick counter

5c910f7

Merge remote-tracking branch 'origin/main' into own-467-freshpoll

538a27f

Merge remote-tracking branch 'origin/main' into own-467-freshpoll

f0f9cc1

docs(server): name the peer Close next to EOF and protocol errors amo…

1bb968f

…ng the clients the look skips

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

Merged via the queue into main with commit edcbe3c Nov 11, 2026
7 checks passed

ThomasK33 deleted the fix/server-bound-stalled-write-queue branch November 11, 2026 05:42

github-actions Bot mentioned this pull request Nov 11, 2026

chore(release): 0.5.0 #444

Open

This was referenced Nov 11, 2026

test(server): pin the Close-frame deadline delay and the wake threshold #495

Merged

fix(mention): give each queued mention a deadline, keep a due flush on another client's handshake, and report refused writes #480

Merged

This was referenced Nov 11, 2026

feat(skills): add verify-selection-tracking, a TLA+ model of selection tracking #477

Merged

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

Merged

Conversation

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

Uh oh!

Why

The rule

Why the drop waits for a look after the next poll

What changed

Since the last push (8fe3c19)

Tradeoffs

Scope and blast radius

Verification

Tests

Red to green and mutants

What the tests and probes do not cover

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

Uh oh!

chatgpt-codex-connector Bot commented Nov 10, 2026

🛡️ Codex Security Review

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!

chatgpt-codex-connector Bot commented Nov 10, 2026

🛡️ Codex Security Review

Uh oh!

ThomasK33 commented Nov 10, 2026

Uh oh!

ThomasK33 commented Nov 10, 2026

Uh oh!

chatgpt-codex-connector Bot left a comment

Choose a reason for hiding this comment

💡 Codex Review

Uh oh!

Uh oh!

chatgpt-codex-connector Bot commented Nov 10, 2026

🛡️ Codex Security Review

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!

chatgpt-codex-connector Bot commented Nov 10, 2026

🛡️ Codex Security Review

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!

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

ThomasK33 commented Nov 10, 2026 •

edited

Loading

Since the last push (`8fe3c19`)

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

edited

Loading