fix(server): judge a silent Claude only after reading its socket by ThomasK33 · Pull Request #488 · coder/claudecode.nvim

ThomasK33 · 2026-11-10T23:51:32Z

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 #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 #467").

Problem

#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 #467

#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 fix(server): drop a client that answers pings but never reads #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 test(server): pin the Close-frame deadline delay and the wake threshold #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 fix(server): drop a client that answers pings but never reads #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 #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 #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 #474.

Not in this PR

The TLA+ model in feat(skills): add verify-ws-connection, a TLA+ model of the WebSocket connection lifecycle #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 • Model: anthropic:claude-sonnet-5-5 • Thinking: xhigh

A ping timer tick cannot tell a silent Claude from a pong that is still in the socket: libuv can run a tick before it reads the socket, after a block of the main loop in any callback. Neovim 0.8 (libuv 1.44) runs the timers again at the end of a pass, so two late ticks can run with no read between them, and #479's second-tick rule then dropped a Claude that answered every ping. A tick now pings and stamps the oldest unanswered ping (`ping_unanswered_since`, with `vim.loop.update_time()` first), and never drops. It starts a one-shot libuv check handle, which libuv runs after the poll that reads the sockets. The check drops a client whose oldest ping is `interval * 2.5` old. A pong clears the stamp, and so does a wake from sleep. A Claude that answers within `interval * 2.5` is never dropped. A Claude that never answers is dropped at the first read after the third tick that follows its first unanswered ping, as before. Removes `pong_overdue`, `is_client_alive` and the 101-callback reset of `last_pong`, which only served the old tick-side check.

ThomasK33 · 2026-11-10T23:51:39Z

@codex review

ThomasK33 · 2026-11-10T23:51:41Z

@codex security review

chatgpt-codex-connector · 2026-11-10T23:51:51Z

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-11T09:38:31.761895Z	`f52bb51`	Manual request
🔒 Security Review	✅ Completed 2026-11-11T10:42:47.460591Z	`28b9fa8`	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-10T23:54:24Z

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

Reviewed commit: f3576ea214

ℹ️ 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-10T23:55:07Z

🛡️ Codex Security Review

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

Reviewed commit: f3576ea214

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.

With libuv 1.44 (bundled in Neovim 0.8) a tick can run before the read after a block in any callback. With newer libuv it can after a block in a check callback or an I/O read callback, and not after a block in vim.schedule or a timer callback. Say so in the comment of drop_unanswered_after_read and in server/README.md, and re-record covered.lock.

…e poll A check that runs after the loop blocked between its tick and the poll judges a ping that the block made look old. Claude kept writing during the block, so a pong that it sent can wait behind more unread data than the socket holds, and the one poll after the block does not reach it. The check now judges only if its loop time is at most `interval * 1.5` after its tick. After a longer block the next tick sees the gap, takes it for a wake and clears the stamps, so such a block restarts the count. Also say in the README and the field doc that the stamp is the oldest ping sent since the last pong was read, and that only a tick that pinged a client starts a check. Add tests for the block before the poll, for the check judging with the loop time of the poll, for the stamp aged from the time of the ping, for a poll 1.4 intervals after the tick, and for the restart of the count.

The check judged a ping unanswered if no pong was read, but 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 of a large message. A block of less than 1.5 intervals before such a poll, on top of an older stamp, still made the ping look 2.5 intervals old. The read callback now clears the stamp on any bytes from the client: Claude shows it is alive by writing anything. A client that writes data but never answers a ping is no longer closed. The gap skip stays: a machine that sleeps between a tick and its poll stops Claude too, so no bytes arrive, and only the skip keeps it.

#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

# Conflicts: # lua/claudecode/server/README.md

A tick that pinged a client always arms the check and idle pair, so the wake-threshold test from #495 can no longer expect no handle. It now runs the poll and checks that the client is kept.

ThomasK33 · 2026-11-11T07:50:59Z

@codex review

ThomasK33 · 2026-11-11T07:51:02Z

@codex security review

chatgpt-codex-connector · 2026-11-11T07:53:47Z

🛡️ Codex Security Review

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

Reviewed commit: 68b0b13e5a

View security finding report

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

ℹ️ About Codex security reviews in GitHub

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

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

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

chatgpt-codex-connector

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 68b0b13e5a

ℹ️ 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".

…dle pair The README linked drop_unanswered_after_read and confirm_stall, which do not exist (the code has judge_silence and judge_stall), and said a stalled client adds a check and idle pair. A tick that pinged arms one pair that judges every client of that tick.

…ndaries The pong of the late-tick describe was built at describe time from `frame`, which only the outer before_each sets, so seeds 9, 15, 40, 57 and 59 failed with 'attempt to index upvalue frame'. New tests kill mutants that survived: update_time inside judge_silence, a tick_time taken from the cached loop time, the stall judgement under the gap skip, the gap skip at 1.5 intervals and 1 ms above it, the drop at exactly 2.5 intervals, and the stall check for a client whose ping is still inside its window.

…client that still sends, and name the check as the closer

ThomasK33 · 2026-11-11T09:32:56Z

@codex review

ThomasK33 · 2026-11-11T09:32:59Z

@codex security review

chatgpt-codex-connector · 2026-11-11T09:36:21Z

🛡️ Codex Security Review

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

Reviewed commit: f52bb51609

View security finding report

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

ℹ️ About Codex security reviews in GitHub

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

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

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

chatgpt-codex-connector

💡 Codex Review

claudecode.nvim/lua/claudecode/server/tcp.lua

Lines 534 to 535 in f52bb51

    
           local now = vim.loop.now() 
        
           local elapsed = now - last_run

Refresh the loop clock before detecting a wake

When an earlier timer callback blocks for more than 1.5 intervals—or the machine is suspended while such a callback is running—libuv's cached now() here can still be the value from the start of the loop pass. The tick therefore fails to recognize the wake, preserves an old ping_unanswered_since, and the post-poll check sees a small tick-to-poll gap but a very old ping, disconnecting a live client before it has a chance to answer after resume. The later update_time() only refreshes the ping timestamp; refresh the clock before computing now and elapsed as well.

ℹ️ 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".

libuv runs the timers of a pass with the loop time of the start of the pass. A timer callback that ran before the ping timer can block for longer than 1.5 intervals, or the machine can sleep in it. The tick then read a stale time: it did not see the wake, kept the stamps of pings from before it, and the check, whose poll is within the gap of the tick, dropped a live Claude that had no time to answer. The tick now calls update_time first and uses that time for the wake test, the stamp and the gap. Found by Codex round 3.

ThomasK33 · 2026-11-11T10:39:19Z

Fixed in 67374f0 (head 28b9fa8), the P1 of review 5856693014: the tick now calls vim.loop.update_time() before it reads the clock, so the wake test, the stamp and the gap use the real time. A new test models a timer callback before the tick in the same pass that blocks for 2 intervals while the cached loop time still shows one: it fails on the previous head (the check drops the live client) and passes now.

ThomasK33 · 2026-11-11T10:39:21Z

@codex review

ThomasK33 · 2026-11-11T10:39:23Z

@codex security review

chatgpt-codex-connector · 2026-11-11T10:41:45Z

Codex Review: Didn't find any major issues. Chef's kiss.

Reviewed commit: 28b9fa8ec4

ℹ️ 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-11T10:42:46Z

🛡️ Codex Security Review

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

Reviewed commit: 28b9fa8ec4

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 on it The ping timer no longer judges at a tick. A tick pings and stamps the oldest unanswered ping, and a libuv check handle that runs after the poll drops the client. Replace the pong_overdue facts with the facts of that design: JudgesAfterRead, StampsRealTime, StampKeepsOldestPing, BytesClearStamp, GapSkip, WakeClearsStamp. NoFalseTimeout no longer counts awake time: it asks whether a Claude that never stopped answering was dropped, which also removes the accounting that let the model pass for a late tick. New environment steps: StaleLoopTime, PollMissesPong and SleepInWindow.

… text for #488 Two replays run a second Neovim as Claude: two-blocks-before-read.lua (two blocks of 1.3 intervals) and blocks-before-the-poll.lua (a pong behind 300 KB, two blocks under the gap, a sleep between a tick and its poll). SKILL.md follows the model: rule, facts, bugs, replays, scope, what a user sees for each item that is not modeled, timings and the numbering of the update steps.

…and name the keepalive rule in a spec comment With ticks on time a silent Claude is closed 3 intervals after its first unanswered ping. A tick that runs late by less than 1.5 intervals finds the ping 2.5 intervals old at its poll, so it closes earlier. The README and the tcp.lua comment said the third tick (90 s). The spec comment about the two rules still named pong_overdue and the pong rule, which #488 removed.

…at the tick The facts read the code as merged: drop_client, judge_silence and after_next_poll replace drop_unanswered_after_read, the writes go through the write helper, and the tick calls update_time before it reads the clock (ClockFreshAtTick replaces StampsRealTime). A stale tick is now a wake that only a fresh clock sees: without the fact NoFalseTimeout breaks. SKILL.md follows the code (new bug entry, the stall rule and the Close deadline as not modeled). protocol-close-window-full.lua waits half a keepalive window, because the Close deadline closes a socket that makes no progress for one window.

…r#501) ## The legacy `open_diff` raised E325 when a swap file for `<path> (New)` existed `require("claudecode.diff").open_diff(...)` (the public legacy entry point, which wraps `_open_native_diff`) opens the proposal's temp file in a split and renames the buffer to `<path> (New)`. At the rename Neovim opens a swap file under the new name. If a swap file with that name exists and its header names that buffer, the rename raises `E325: ATTENTION`. That happens when another Neovim changed a buffer with that name, or when a Neovim that was killed after `:preserve` left it. What the caller sees on `main`: `E5108` with a stack trace from `diff.lua:814`, a half-open diff (one of the two windows is in diff mode), a buffer that has a swap file, and a leftover temp file. ## Who is affected Only code that calls `open_diff` itself, such as a user's own Lua. No plugin action calls it: `openDiff` uses `_setup_blocking_diff` (`grep` finds no caller of `open_diff` or `_open_native_diff` in `lua/` besides the wrapper). So this is a small hardening fix, not a regression of a user-facing flow. ## The fix `lua/claudecode/diff.lua`, one line: the temp file is opened with `noswapfile edit`. The rename then has no swap file to meet. The buffer becomes `nofile` with `swapfile` off a few lines later anyway, so no swap file is lost. ## Proof - New real-Neovim spec `tests/integration/diff_legacy_swap_spec.lua`. A second Neovim changes a buffer named `<path> (New)` and is killed with SIGKILL after `:preserve`, which leaves a swap file whose header names that buffer. Then the spec calls `open_diff`, and asserts that it returns `success`, that the proposal buffer has no swap file, and that its name is `<path> (New)`. - On `main`: fails with `diff.lua:814: Vim:E325: ATTENTION` on Neovim 0.12.3 and on v0.8.0. - With this change: passes on both. - All other `tests/integration/diff_*_spec.lua` files pass on 0.12.3 and v0.8.0. - `mise run format-check` and `mise run check` are clean. `mise run test`: 1488 successes, 0 failures, 20 pending (the new spec is pending under busted, because it needs a real Neovim). `tests/unit/diff_spec.lua` still passes (its native-diff case only looks for an `edit` command, and `noswapfile edit` contains it). - `.agents/skills/verify-diff-lifecycle/covered.lock` is re-recorded (after merging `origin/main` at `bad488f` and again at `d63c9b3` (coder#488): each merge conflicted in the lock, so I took main's lock and ran `--record`). Only the hash of `diff.lua` changed, and `_open_native_diff` is outside the model (the model covers `openDiff` through `_setup_blocking_diff`). The model passes (89,205 distinct states). The probe, the patch and the first version of the spec come from the verifier's evidence. --- _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`_

… it contradicts (coder#533) ## Why The goal is that every claim in the README contracts of this repository is true for the code at `main`, and that each correction names its evidence. A contract is the README of one folder. It states what the code does and cites the function that does it. The branch `docs-gtz7` corrected many claims at an old commit of `main`. `main` has moved since (peer PRs coder#445 to coder#522 rewrote several passages and changed the code). This PR merges `main` into that work, re-checks every line that it changes against the current code, and fixes the lines that the peers made stale or that the merge joined into false text. ## What changed Docs only, in seven README files. The branch has four parts. 1. The commits of `docs-gtz7` (three content commits and a merge of `main`): a refresh of the contracts against the code, a pass that fixed the drift that the refresh left, and a pass that corrected claims which runtime probes disproved. 2. Five merge commits of `main` (the second for coder#522, the third for coder#524 and coder#530, the fourth for coder#506, the fifth for coder#531 and coder#526). Where a peer PR and `docs-gtz7` both changed a passage, `main`'s text won. A `docs-gtz7` correction stayed only where it is still true. 3. Nine correction commits. Six verifier agents, one per file or half file, checked every line that this diff changes against the code. They ran headless Neovim 0.12.3 probes (one on 0.10.4) where reading did not decide the claim. I applied their corrections in commits that group the files: server, root and plugin, tools, lua, terminal, scripts, the main-text fixes, and one for the exit sentences and the last seven findings. A second verifier then found one false sentence (the exit sentence below) and seven wording findings, which that last commit fixes. 4. One commit for two P2 findings of the Codex code review on `42ef1bd1`. First, `stop` and the token mismatch in `start` try to remove the lock file and only log a warning when that fails (`lua/claudecode/init.lua:642-647`, `:605-608`), so three sentences in `README.md` now say "tries to". Second, the headless auto-setup check in `plugin/README.md` used `--cmd "set rtp^=$PWD"`, which Ex splits at a space in the checkout path. I ran it in `/…/with space/repo` on Neovim 0.12.3: it fails with `E518` and prints `0`. The `lua vim.opt.rtp:prepend(vim.fn.getcwd())` form prints `2`, and `0` without the auto-setup line, as the README says. Per file, with the number of claims checked and the result: | File | Claims checked | True | False | Incomplete | Unverified | Edits | |---|---|---|---|---|---|---| | `README.md` (Repository Blueprint) | 41 | 39 | 0 | 2 | 0 | 2 | | `plugin/README.md` | 40 | 39 | 0 | 1 | 0 | 1 | | `lua/claudecode/README.md` | 198 | 173 | 11 | 14 | 0 | 23 | | `lua/claudecode/server/README.md` | 88 | 75 | 3 | 9 | 1 | 13 | | `lua/claudecode/terminal/README.md` | 106 | 100 | 2 | 4 | 0 | 5 | | `lua/claudecode/tools/README.md` | 68 | 54 | 4 | 10 | 0 | 14 | | `scripts/README.md` | 7 | 0 | 2 | 4 | 0 | 13 | A false claim was true at the old base or never true. An incomplete claim leaves out a condition that the code has. The row for `scripts/README.md` lists the seven items of the coder#462 verifiers (one more was misleading). The 541 claims of the first six rows split into 480 true, 20 false, 40 incomplete and 1 unverified. ### Re-sync items after the peer PRs - coder#530 (invalid `provider`). `lua/claudecode/README.md` said that an invalid `provider` keeps the previous value "although the warning says Defaulting to 'native'". `main` now warns `Keeping '<provider>'` (`lua/claudecode/terminal.lua:483-488`). The sentence says what the warning names now. The defect is gone from the list of code defects below. - coder#531 (release-please runner). The `run-release-please.sh` bullet of `scripts/README.md` keeps the verified text and adds `main`'s clause that `commonmark` must be on the module path too. The runner requires it at load (`scripts/release-please-runner.js:27`). The Communique, Prettier and output code that the runner bullet cites did not change. - coder#526 (snacks tests). It changes comments and dead window option assignments in `lua/claudecode/terminal/snacks.lua`. No line of this PR depends on them. - coder#524 (visual selection and plugin edits). The two conflicts were passages about the buffer listener and the flush of a visual selection. `main`'s text won in both, and the root `Editor state` bullet keeps the verified autocmd group list with `main`'s listener wording (`lua/claudecode/selection.lua:watch_selection_buffer`, `note_visual_edit`). The selection claims that this PR changes (`selection_changed` positions, `selection.lua` internals) do not depend on the code that coder#524 changed. - coder#459 (lockfile). `README.md` no longer says that `start` leaves the lock file on disk after a token mismatch: `start` removes it and stops the server (`lua/claudecode/init.lua:603-619`). The System Verification bullet about `CLAUDE_CONFIG_DIR` and `tests/lockfile_test.lua` is gone: the test hides the caller's value and stays in a private home (`tests/lockfile_test.lua:340-355`, `:439-442`). `lockfile.update` is removed from `lua/claudecode/README.md`: the module has no such function. The `start` and `stop` bullets use the text of coder#459, and `stop` is described as an attempt to remove the lock file (`init.lua:635-670`). - coder#461 (openFile reload). The reload-error passage of `lua/claudecode/tools/README.md` is the text of `main`. The claim that the recovery read does not end Visual mode stays. A probe confirmed it in both forms: plain Visual mode, and Visual mode that CTRL-O started. The read runs through `nvim_buf_call`, so the mode stays on (`lua/claudecode/tools/open_file.lua`). - coder#462 (WebSocket shell clients removed). No README cites `scripts/lib_claude.sh` or another deleted file (a grep over the seven files finds none). ### Corrections per file <details> <summary>README.md</summary> - The list of what rejects a pending `openDiff` now includes Claude's `close_tab` and `closeAllDiffTabs` calls, which reject it through `close_diff_by_tab_name` (`lua/claudecode/diff.lua:2040-2044`, `:2105-2107`, `lua/claudecode/tools/close_tab.lua:53`, `lua/claudecode/tools/close_all_diff_tabs.lua:30`). - At exit, Neovim fires `BufUnload` for each loaded buffer before `VimLeavePre`, and the proposal buffer's `BufUnload` autocmd rejects its pending diff (`lua/claudecode/diff.lua:1279-1285`). So with one pending diff the rejection runs before the `VimLeavePre` cleanup. With two or more pending native diffs there is one exception: the reject of a new-file diff in the current tab with `diff_opts.on_new_file_reject = "keep_empty"` (the default) deletes its proposal buffer (`diff.lua:1171-1175`, `:1523-1524`), Neovim's exit loop then stops firing `BufUnload`, and the cleanup removes the other diffs with no answer. Probes on Neovim 0.8.0, 0.9.5, 0.10.4, 0.11.5 and 0.12.3 show both cases, and the `unified` layout answers every diff. The sentence states both. A fix PR (F13) follows, see "Defects in the code". - `start` removes the lock file on a token mismatch (see above). - The Processes bullet adds `:checkhealth claudecode` (`<cli> --version`, `lua/claudecode/health.lua:43-66`) and the `git rev-parse` of `terminal.git_repo_cwd` (`lua/claudecode/cwd.lua:28-42`). - `CLAUDE_CONFIG_DIR` set but empty uses `~/.claude/ide` (`lua/claudecode/lockfile.lua:11-18`). Three lines say so now. - The Side Effects bullet lists the autocmd groups of `lua/` and `plugin/` (`ClaudeCodeShutdown`, `ClaudeCodeSelection`, `ClaudeCodeMCPDiff`, `ClaudeCodeDiffCleanup`, `ClaudeCodeNativeAdopted`, `ClaudeCodeOpenFileNewFiles`, and one `snacks_win_<id>` per Snacks terminal whose split the plugin re-creates, `lua/claudecode/terminal/snacks.lua:259`), the `nvim_buf_attach` listeners (`lua/claudecode/selection.lua:175-191`) and the `"unified"` highlight groups (`lua/claudecode/diff_inline.lua:33-36`). </details> <details> <summary>plugin/README.md</summary> - Commands from auto-setup exist after a startup script that waits (`:sleep` or `vim.wait()`) lets the deferred `setup` run. They do not exist when the `-c` commands and `VimEnter` run. Headless probes on Neovim 0.12.3 (`plugin/claudecode.lua:13-17`). - The other 39 changed claims held: the load guard order, the second `source` doing nothing, the version error on Neovim older than 0.8, the failed module load shown once, the auto-setup global read twice, and the error from the deferred `setup`. </details> <details> <summary>lua/claudecode/README.md: 23 corrections with evidence</summary> - Only :ClaudeCodeSend uses the local add_paths_to_claude. :ClaudeCodeTreeAdd and :ClaudeCodeAdd call M.send_at_mention in their own code. Evidence: lua/claudecode/init.lua:703, init.lua:830, init.lua:904, init.lua:914, init.lua:974-975, init.lua:1021-1022, init.lua:1126. - expand_tilde expands only `~` and `~/...`. A path such as `~user/x` stays as it is. Evidence: lua/claudecode/init.lua:1113-1117, lua/claudecode/utils.lua:167-181. - The fallback split runs create_split, whose leave_preview_window moves from the preview window to a tiled Claude terminal window in the same tab before it splits. Evidence: lua/claudecode/diff.lua:803-810, diff.lua:263-276, diff.lua:279-281. - Since coder#483 and coder#469, diff_inline.lua no longer calls _resolve_diff_as_saved (it calls _write_proposal) and it also calls _register_reject_when_hidden and _close_proposal_window. Evidence: lua/claudecode/diff_inline.lua:471, diff_inline.lua:485, diff_inline.lua:616, lua/claudecode/diff.lua:1228-1234, commits 6eef218 (coder#483) and 36f4a0e (coder#469). - lockfile.update no longer exists: PR coder#459 (0e63cc7) removed it. Evidence: lua/claudecode/lockfile.lua:74, lockfile.lua:84, lockfile.lua:208, lockfile.lua:239, lockfile.lua:292 (the only M functions), commit 0e63cc7 (coder#459). - terminal.setup also calls get_provider, whose fallback warnings go through logger.warn, as the bullet above says. Evidence: lua/claudecode/terminal.lua:584, terminal.lua:124-130, terminal.lua:145, terminal.lua:163-166, terminal.lua:178. - A connected send that the debounce queues still fires ClaudeCodeSendComplete. Only the disconnected branch fires none. Evidence: lua/claudecode/init.lua:383-398, lua/claudecode/init.lua:1395-1400, lua/claudecode/init.lua:401-416. - The terminal call and the event happen only when _broadcast_at_mention succeeds. Evidence: lua/claudecode/init.lua:383-400. - No handshake polling exists since coder#454/coder#480. The 50 ms, 25 ms and connection_wait_delay facts repeat main's queue bullet. A send with debouncing off still queues behind a non-empty queue. Evidence: lua/claudecode/init.lua:283-289, lua/claudecode/init.lua:110-111, lua/claudecode/init.lua:1381-1396. - PR coder#452 added TextChangedI and TextChangedP. Evidence: lua/claudecode/selection.lua:387. - Since coder#452 reconcile_held_selection reports the cursor at CursorMoved, not after visual_demotion_delay_ms. A text change and another buffer also end the hold. Evidence: lua/claudecode/selection.lua:237-265, lua/claudecode/selection.lua:118-159, lua/claudecode/selection.lua:576-584, tests/selection_test.lua:2341. - find_main_editor_window skips only a fixed filetype list, not every explorer or outline sidebar. Evidence: lua/claudecode/diff.lua:157-190. - find_main_editor_window can return a window of another tab (current tab first), as the bullet above says. Evidence: lua/claudecode/diff.lua:125-142, lua/claudecode/diff_inline.lua:382-409. - Probe: proposal "a\n\n" is accepted as "a\n" (split_lines drops one trailing empty line, and the newline fix adds none back). Evidence: lua/claudecode/diff_inline.lua:44-52, lua/claudecode/diff_inline.lua:526-540, lua/claudecode/diff_inline.lua:303, probe_unified_accept.out. - An invalid diff percentage falls back to split_width_percentage, not straight to 0.30. Evidence: lua/claudecode/diff.lua:50-69. - PR coder#469 set the unified proposal buffer to bufhidden=hide (main's bullet above says so), WinClosed/BufHidden reject it. Evidence: lua/claudecode/diff_inline.lua:299, lua/claudecode/diff_inline.lua:475-485, lua/claudecode/diff.lua:1189-1222. - The close_tab tool also passes a client_id. Evidence: lua/claudecode/tools/close_tab.lua:53, lua/claudecode/diff.lua:2105-2148. - At qa! the BufUnload autocmd (diff.lua:1283) calls _resolve_diff_as_rejected before the VimLeavePre cleanup runs, for one pending diff. With two or more native diffs, a keep_empty reject of a new-file diff deletes its buffer and stops the exit loop, so the later diffs stay pending until the cleanup (the Augroups bullet states this). Evidence: lua/claudecode/diff.lua:1171-1175, lua/claudecode/diff.lua:1279-1285, lua/claudecode/diff.lua:1523-1524, probes on 0.8.0 to 0.12.3. - PR coder#478 added the WinClosed autocmd that deletes the handler. Evidence: lua/claudecode/diff.lua:455-463, tests/unit/diff_new_tab_terminal_handler_spec.lua:127. - require('claudecode').setup validates log_level (assert) before logger.setup runs. Evidence: lua/claudecode/init.lua:462-465, lua/claudecode/config.lua:15, lua/claudecode/config.lua:98-106, lua/claudecode/logger.lua:26-40. - Neovim 0.10 has no 'messagesopt' and always stops. The parenthetical read as if only 0.11+ stops. Evidence: probe_echospace.out (0.10.4: NO SUCH OPTION, 0.11.5: hit-enter,history:500). - With laststatus=1 and two windows v:echospace is 68, not 51. Evidence: probe_echospace.out. - PR coder#445 removed the skip. The loop runs every file. Evidence: scripts/run_integration_tests_individually.sh:86-88. </details> <details> <summary>lua/claudecode/server/README.md: 13 corrections with evidence</summary> - The pending check/idle pair of a tick runs judge_silence and judge_stall, not only a stall confirmation Evidence: lua/claudecode/server/tcp.lua:601-611, tcp.lua:424-435, tcp.lua:490. - The state stays `closing` after on_close. On_close only removes the client (README line on client states says it never becomes `closed`) Evidence: lua/claudecode/server/client.lua:363-371, tcp.lua:227-228, tcp.lua:275-283. - start_close_timer also sets `closed` when a keepalive window passes with no write progress Evidence: lua/claudecode/server/client.lua:459-466, client.lua:140-144. - Completes the state list: _disconnect_client does not touch client.state (probe: on_disconnect saw state `connected` after EOF) Evidence: lua/claudecode/server/tcp.lua:209-217, tcp.lua:255-294, probe-server/events.log client_8, client_9. - PR coder#480 added connected_at to get_client_info Evidence: lua/claudecode/server/client.lua:522-531, client.lua:292. - PR coder#454 moved process_mention_queue from on_connect to on_open Evidence: lua/claudecode/server/init.lua:57-73, client.lua:294-296. - After the merged sentences, `It` reads as process_data or the Close frame. Process_data does check the whole message Evidence: lua/claudecode/server/frame.lua:156-168, client.lua:184-188. - parse_frame rejects a 1-byte Close payload with 1002 (same bullet group says so), so only an empty payload reaches the 1000 default Evidence: lua/claudecode/server/frame.lua:157-160, client.lua:352-361, probe S5, S6. - Since PR coder#455/coder#488 last_pong plays no part in the keepalive Evidence: lua/claudecode/server/client.lua:381-383, client.lua:529, tcp.lua:220-222, tcp.lua:474-475. - PR coder#497/coder#500: tools/call answers -32602 for a non-string name before handle_invoke. Contradicts the JSON-RPC errors bullet Evidence: lua/claudecode/server/init.lua:353-368. - Two callbacks share the name: process_data's on_error carries client errors (other bullets say so), server.on_error only server failures Evidence: lua/claudecode/server/tcp.lua:121,190,196,524, tcp.lua:229-231, client.lua:202,275. - The 101/error write callback calls on_error when err or not success Evidence: lua/claudecode/server/client.lua:271-279, probe events client_1..3. - The message carries the tool name Evidence: lua/claudecode/tools/init.lua:90-96. </details> <details> <summary>lua/claudecode/terminal/README.md: 5 corrections with evidence</summary> - FALSE since coder#464: native close and the first get_active_bufnr of a module copy adopt a marked live terminal. The sentence also contradicts the same bullet's second sentence. Evidence: lua/claudecode/terminal/native.lua:292, lua/claudecode/terminal/native.lua:574-577, probe probe-terminal/probe_native_reload.out. - INCOMPLETE: on Neovim 0.12.3 termopen also returns 0 under :silent! for a modified buffer, which is not an invalid argument. Evidence: probe probe-terminal/probe_termopen.out (cases D, E, F, G, H, I), lua/claudecode/terminal/native.lua:237-242. - INCOMPLETE: through the dispatcher a missing Snacks never reaches the ERROR notification, because get_provider falls back to native. Evidence: lua/claudecode/terminal.lua:133-146, lua/claudecode/terminal.lua:192-196, lua/claudecode/terminal/snacks.lua:691-693. - INCOMPLETE: an unset snacks_win_opts.position falls back to split_side (left or right), so cc_show re-creates a split itself. Evidence: lua/claudecode/terminal/snacks.lua:374-377. - INCOMPLETE: for an adopted terminal each entry with a config replaces term._cc.config, so it is not the config captured at open. Evidence: lua/claudecode/terminal/snacks.lua:463-474, lua/claudecode/terminal/snacks.lua:646-647, lua/claudecode/terminal/snacks.lua:747. </details> <details> <summary>lua/claudecode/tools/README.md: 14 corrections with evidence</summary> - FALSE after PR coder#500: handle_invoke uses `params.arguments or {}`, so no Lua error and no -32000 (probe p1: openFile/saveDocument -32602, getDiagnostics []). Also contradicted line 17. Evidence: lua/claudecode/tools/init.lua:88, lua/claudecode/server/init.lua:357, probes/p1_static.out. - FALSE: the script loops over every tests/integration/*_spec.lua with no skip. PR coder#445 (a4d3238) made it run command_args_spec again. Evidence: scripts/run_integration_tests_individually.sh:86. - Misleading: bufnr() finds 'file.txt', 'b/file', './dir/../dir/file.txt' and '' (current buffer). Probes p1 and p5. Evidence: lua/claudecode/tools/save_document.lua:31, lua/claudecode/tools/check_document_dirty.lua:27, probes/p1_static.out, probes/p5_bufnr.out. - INCOMPLETE after PR coder#457: with no stored selection it reads the editor (the bullet above says so), so it does not always return the stored selection. Evidence: lua/claudecode/tools/get_current_selection.lua:37-39, :83-95. - INCOMPLETE: the -32603 table is returned, not raised, so build_response sends it as `{ result = ... }`. Also joins the hard-wrapped bullet like the rest of the file. Evidence: lua/claudecode/tools/close_tab.lua:26-33, lua/claudecode/tools/init.lua:180-182, lua/claudecode/server/init.lua:387. - Format: the merge wrapped a quoted error message across two lines inside a code span, so a search for the message misses it. Every other bullet is one line. Evidence: lua/claudecode/tools/open_diff.lua:56. - Coherence: the inserted sentence split 'finds it' from 'Without one', so 'one' no longer names the loaded buffer. The moved claim is TRUE (probe p1). Evidence: lua/claudecode/tools/open_file.lua:133-140, probes/p1_static.out. - INCOMPLETE: expand_tilde leaves `~user/...` unchanged. Evidence: lua/claudecode/utils.lua:167-181, lua/claudecode/tools/open_file.lua:547. - INCOMPLETE: with makeFrontmost=false the answer is the JSON object, and in the middle of a command openFile appends a suffix. Evidence: lua/claudecode/tools/open_file.lua:735, :741, :746-760, probes/p4_openfile_save.out. - INCOMPLETE: source and code are nil (absent from the JSON) when the diagnostic has none. Evidence: lua/claudecode/tools/get_diagnostics.lua:82-83. - INCOMPLETE: nvim_get_current_tabpage() returns a handle. Probe p1: tabpagenr() 2, handle 3, groupIndex/viewColumn 2/3. Evidence: lua/claudecode/tools/get_open_editors.lua:19, :65-66, probes/p1_static.out. - INCOMPLETE: reload_file_buffers skips a modified buffer, and a diff kept for another client does not close. Evidence: lua/claudecode/diff.lua:2015-2018, :2025-2027, :1104. - INCOMPLETE: no API tells which loaded buffers were opened before their file existed. The loop marks every loaded, named, normal buffer whose file is not readable. Evidence: lua/claudecode/tools/open_file.lua:170-179. - INCOMPLETE (minor): with diff_opts.layout = "unified" diff.lua hands the result to diff_inline, which builds it. Evidence: lua/claudecode/diff.lua:1050-1053, lua/claudecode/diff_inline.lua:526-537. </details> <details> <summary>scripts/README.md: 7 items of the coder#462 verifiers, each checked against the scripts</summary> - The CI paragraph named no job for "the same job". It now names the three jobs of `.github/workflows/test.yml` (`unit-tests`, `integration-tests`, `covered-lock`), says that `integration-tests` runs the runner twice (the second time with a `TMPDIR` that holds a space and a `%`), and says that `Required` needs only `unit-tests` and `integration-tests` (`test.yml` lines 52-80, 98-167, 215-234). - `tla/check-lib.sh` exit precedence: 2 wins over 1, and 1 wins over 3. A stale lock plus a broken rule exits 1. `--hash-only` exits 0 or 3, and `--record` exits 0. A script that sources the lib and ends without `tla_main` turns an exit 0 into exit 2. Probed with a fake `curl` and a fake TLC: default with a broken rule and a stale lock gave rc=1, default with a pass and a stale lock rc=3, a broken `TypeOK` rc=2, `--record` on a stale lock rc=0 (`scripts/tla/check-lib.sh:81-84`, `:226-246`, `:313-333`, `:406-419`). - `tla_init` comes right after `SKILL` and `MODEL`, before `covered_block` (`.agents/skills/verify-diff-lifecycle/check.sh:15-29`, `scripts/tla/check-lib.sh:461`). - `run-release-please.sh` prints nothing itself, and exits 1 with no message when `release-please` is missing. The runner's stdout and file outputs are listed: release-please's own log lines go to stdout (info and debug) and stderr (warnings and errors), the `key=value` lines go to `GITHUB_OUTPUT` or to stdout when it is unset, and `--dry-run` prints JSON after the log lines and still runs Communique. Probed without a token and without network: wrapper rc=1 with no output, and `Error: GITHUB_TOKEN must be set` (`scripts/release-please-runner.js:487-492`, `:555`, `:590`, `:614`). - `--record` and `--hash-only` exit before the TLC jar is fetched, so they never download it and need no `java`. A plain run and `--mutants` do. Probe with an empty cache and a fake `curl`: `--hash-only` and `--record` made 0 `curl` calls, a plain run and `--mutants` made 1 and exited 2 (`scripts/tla/check-lib.sh:452-453`, `:147-151`). - The Lua repros: under `nvim -l` an uncaught error prints `E5113` and exits 1, `cquit N` and `os.exit(N)` exit N, and a bare file name run from `scripts/` fails with `module 'claudecode.diff' not found`. In the `:luafile` form of CI an uncaught error falls through to `cquit 2` (probes on Neovim 0.12.3, and `-l` exit 1 on 0.9.5, 0.10.4 and 0.11.5). - `repro_issue_70.sh` and `repro_issue_277.sh` side effects that the file did not list: work dir names, the `att-home` folder, the empty `/tmp/agent-tty/<8 hex>` socket folder and the `homes.json` entry that `agent-tty` leaves, the inherited environment, the three background probes of 70 and their `PORT.lock` files (a SIGKILL leaves the lock), the unpinned diffview.nvim clone of 277, the state and cache files of `NVIM_APPNAME=issue-277`, the `perl` timeouts, and the nested copy under an existing `issue277-artifacts-latest`. A full run of 277 with private dirs took 32 s. A SIGKILL run left the lock file and 3 processes until `agent-tty destroy`. - `manual_test_helper.lua` calls the handler itself, so no response sender is stored for its coroutine. Any resolution after the handler yields (accept, reject, or `qa!`) logs `No global response sender found for coroutine`. It is expected and harmless (all four CI-form runs exited 0). </details> ## Scope - No code changes. `covered.lock` does not change. - Lines of `scripts/README.md` about `repro_issue_218.sh` stay as they are on `main`. PR coder#458 owns them, and its merge will change them. - I checked every line that this diff changes. Lines that the diff does not touch were not re-verified, except where a verifier found one false while reading its neighbors. Those fixes are in the last correction commit: `server/mock.lua` is required by `tests/unit/server/mock_spec.lua`, the augroup and `utils.lua` lists, the empty `CLAUDE_CONFIG_DIR`, and the Processes bullet. - Probes ran on Linux with Neovim 0.12.3. One probe ran on 0.10.4. The old Neovim claims that earlier lanes proved on 0.8 were not run again. - One claim stays unverified: the sentence in `lua/claudecode/server/README.md` that a client whose EOF the server read in the same read as its request is handled as the code says. Six probe tries did not produce that case. The sentence is a softening, so I kept it. - The terminal README says that the wait before a `close` does not prevent a hang at exit. A probe saw the hang with and without a `close`, so the probe does not prove that the buffer delete causes it. I did not open neovim/neovim#42508 (the host has no network). ### Defects in the code that the verifiers found These need a code fix and a test, so they are not in this docs PR. 1. Accepting a `unified` diff drops one trailing empty line of the proposal: `"a\n\n"` is accepted as `"a\n"` (`lua/claudecode/diff_inline.lua:44-52` and `:531`). The native layout is not affected. A probe shows it. The README says the accepted text is the proposal lines that setup computed. 2. `lua/claudecode/server/tcp.lua:19` says the PRNG is seeded once per process. It is seeded once per load of the module. 3. `lua/claudecode/server/init.lua:59-60` logs "Authenticated WebSocket client connected" from `on_connect`, before the authentication check runs. 4. `lua/claudecode/cwd.lua:36-42` runs the same `git rev-parse` twice. 5. At exit, a pending native diff can stay unanswered. Two native diffs are pending, and the first one (the lower proposal buffer number) is a new file in the current tab with `diff_opts.on_new_file_reject = "keep_empty"` (the default). On `:qa!` its reject deletes its proposal buffer (`lua/claudecode/diff.lua:1171-1175`, `:1523-1524`), Neovim's exit loop stops firing `BufUnload` (`src/nvim/main.c`, the `bufref_valid` check), and the `VimLeavePre` cleanup removes the second diff with no answer. Reproduced on Neovim 0.8.0, 0.9.5, 0.10.4, 0.11.5 and 0.12.3, with and without the server. A separate PR (F13) will make exit answer every pending diff. It will change the exit sentences of this PR: the openDiff bullet in `README.md` (Global Invariants, the sentence that starts "When Neovim exits") and the Augroups bullet in `lua/claudecode/README.md` (the sentences about `BufUnload` and the exception). ## Blast Radius Seven README files. Nothing loads them at runtime. A wrong correction here misleads a reader but breaks no behavior. ## Verification - Six Opus verifiers, one per file (two for the 198 claims of `lua/claudecode/README.md`). Each checked every claim that the diff adds or changes against the code, and every `[file:symbol]` citation, with file and line evidence. Their findings, edits and probe scripts are in the evidence folder of the run. - A second, independent verifier checked the head `bcacd14c` (134 sentences and all seven scripts items, with probes on Neovim 0.8.0 to 0.12.3). It found one false sentence (the exit sentence, now fixed with its exception) and seven wording findings (fixed). It found no other false claim. - Citation check on the final head: 760 citations, links and test paths over the seven files, 1 flagged. The flagged one is `[plugin/claudecode.lua:pcall(require, "claudecode")]`, an expression that `main` already cites in that README. - `mise run all`: exit 0 on the final head `e3e48af1` (1682 successes, 0 failures, 0 errors, 24 pending, `luacheck` 0 warnings and 0 errors in 178 files). `mise run format-check`: exit 0 on the final head (355 files, 0 changed). 1676 successes, 0 failures, 0 errors, 24 pending. `luacheck` reports 0 warnings and 0 errors in 178 files. The format step changes 0 files. - `git merge-tree --write-tree` of the head and `origin/main` (`3a0bb769`) is clean. - The merges of coder#524 and coder#530 changed one sentence of `lua/claudecode/README.md` and merged two conflict hunks. I checked that sentence and the merged bullets against `lua/claudecode/terminal.lua` and `lua/claudecode/selection.lua` at `a41254a4`. I did not run a verifier agent over the merge delta. --- _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 6 commits November 11, 2026 00:29

Merge origin/main into fix/keepalive-late-ticks

13385a7

# Conflicts: # lua/claudecode/server/README.md

test(server): run the poll after a wake tick instead of counting handles

68b0b13

A tick that pinged a client always arms the check and idle pair, so the wake-threshold test from #495 can no longer expect no handle. It now runs the poll and checks that the client is kept.

chatgpt-codex-connector Bot reviewed Nov 11, 2026

View reviewed changes

Comment thread lua/claudecode/server/README.md Resolved

Comment thread lua/claudecode/server/README.md Resolved

ThomasK33 added 4 commits November 11, 2026 08:12

docs(server): fix a stray backtick, say when the stall rule closes a …

8dda933

…client that still sends, and name the check as the closer

Merge origin/main into fix/keepalive-late-ticks

f52bb51

chatgpt-codex-connector Bot reviewed Nov 11, 2026

View reviewed changes

ThomasK33 added 2 commits November 11, 2026 10:22

Merge origin/main into fix/keepalive-late-ticks

28b9fa8

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

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

ThomasK33 deleted the fix/keepalive-late-ticks branch November 11, 2026 13:14

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

chore(release): 0.5.0 #444

Open

ThomasK33 mentioned this pull request Nov 11, 2026

fix(diff): open the legacy diff's temp file without a swap file #501

Merged

Conversation

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

Uh oh!

Result

Problem

Change

With #467

Behavior

Tests

Replays on real Neovim

Not in this PR

Checks

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 11, 2026

Uh oh!

ThomasK33 commented Nov 11, 2026

Uh oh!

chatgpt-codex-connector Bot commented Nov 11, 2026

🛡️ Codex Security Review

Uh oh!

chatgpt-codex-connector Bot left a comment

Choose a reason for hiding this comment

💡 Codex Review

Uh oh!

Uh oh!

Uh oh!

ThomasK33 commented Nov 11, 2026

Uh oh!

ThomasK33 commented Nov 11, 2026

Uh oh!

chatgpt-codex-connector Bot commented Nov 11, 2026

🛡️ Codex Security Review

Uh oh!

chatgpt-codex-connector Bot left a comment

Choose a reason for hiding this comment

💡 Codex Review

Uh oh!

ThomasK33 commented Nov 11, 2026

Uh oh!

ThomasK33 commented Nov 11, 2026

Uh oh!

ThomasK33 commented Nov 11, 2026

Uh oh!

chatgpt-codex-connector Bot commented Nov 11, 2026

Uh oh!

chatgpt-codex-connector Bot commented Nov 11, 2026

🛡️ Codex Security Review

Uh oh!

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

ThomasK33 commented Nov 10, 2026 •

edited

Loading

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

edited

Loading