feat(skills): add verify-mention-queue, a TLA+ model of the @mention queue by ThomasK33 · Pull Request #523 · coder/claudecode.nvim

ThomasK33 · 2026-11-11T18:20:52Z

What this adds

.agents/skills/verify-mention-queue/: a TLA+ model of the @mention queue and the WebSocket clients it sends to, a check.sh on the shared harness scripts/tla/check-lib.sh, a /statechart view, and 12 headless Neovim replays. CI runs it in the covered-lock job with the other verify-*/check.sh.

The model describes the code on main after #454 and #480: one queue, a deadline per mention (connection_timeout + connection_wait_delay after the send), a flush that waits until some connected client has been connected for connection_wait_delay since its handshake (connected_at), a broadcast to every connected client, the drain to a ready client past the deadlines, and the write reports, the refused write included. It has two client slots, so a broadcast can reach two clients and the readiness rule can count both.

This PR also fixes the doc findings from the last verifier pass on #480, and adds the test the #480 advisor found missing:

.agents/skills/verify-claudecode-nvim/features/send-at-mention.md: a connected client that is not ready yet gets "Send timeout", not "Connection timeout", and the error comes at the deadline, 10.6 s after the send.
lua/claudecode/config.lua, dev-config.lua: the queue_timeout comments no longer say that mentions wait up to connection_timeout.
fixtures/issue-70/init.lua: the mention waits until its deadline, 10.6 s by default, not 10 s.
lua/claudecode/types.lua: connection_timer runs while the queue holds a mention, also while a ready client drains it. It is nil only after a deadline passed while a ready client was connected, until queue_mention or a flush with no ready client starts it again.
tests/unit/mention_queue_spec.lua: D: a send 400 ms after the handshake waits until connection_wait_delay has passed since the handshake, and the same at 540 ms. Each expects nothing 590 ms after the handshake and the mention by 610 ms. A flush that sends while under 20, 100 or 200 ms of the wait are left fails one of them. D: the first ready client sends the queue, though a second client connected later is not ready yet fails when readiness waits for the newest client (math.max in place of math.min).

These change comments and tests only. No runtime code changes.

What the model checks

NoSilentDrop: a mention you sent reaches Claude, or you see an error, unless you stopped the integration first.
SentInOrder: each Claude gets the mentions in the order you sent them.
AtMostOnce: each Claude gets each mention at most once.
SentWhenReady: a mention goes out only while some connected client has been connected for connection_wait_delay since its handshake. Default config only: with disable_broadcast_debouncing on, a send while the queue is empty skips this wait. That is a known bug, which a follow-up PR fixes (repro below).
NothingAfterStop: after :ClaudeCodeStop, no mention queued before the stop reaches Claude, and the queue raises no Lua error.
NoStrandedMention (liveness): every queued mention leaves the queue.
ReadyDelivers (liveness): while a ready Claude stays connected, every queued mention goes out to it.
FlushDelivers (liveness, with no deadline that passes): the flushes alone send a ready Claude every queued mention, so none waits for a deadline first.

check.sh reads 19 guards from init.lua, server/init.lua, server/tcp.lua and server/client.lua, and runs the model with each one as the code has it. FlushExpiresOverdue alone breaks NoStrandedMention. QueueKeepsDeadline alone breaks no rule in this untimed model: the next flush with no ready client clears the overdue mentions, so only the time of the error changes. So --mutants checks it only as a pair with FlushExpiresOverdue. The unit tests A, F4: a Claude whose handshake comes 10.3 s after the send … and the S: churn tests at 700/300 and 650/500 ms catch it alone.

A code change that keeps every fact TRUE reads only STALE, for example a change of the readiness wait or a deadline that never comes. SKILL.md names such changes, and the unit tests catch them.

Bugs it found, and the fixes

The first model, on the code before #454, broke five of its six rules. Each finding was replayed on real Neovim. #454 fixed all nine:

A: a mention that waited for a slow Claude start was dropped at the flush as older than queue_timeout, with no error.
H: Claude dropped during the 600 ms wait, and the plugin sent the mention to no client and logged success.
E: a send during the wait overtook the mention queued before it.
C: :ClaudeCodeStop during the wait raised a Lua error, and a stop and a start sent the old mention to the new Claude.
B: the connection timer stayed set after it fired, so later mentions never timed out.
S: a send while connected started no timer, so a drop within the 50 ms debounce stranded the mention.
F: a client that sent its CLOSE frame still counted as connected.
D: the flush hook ran at the TCP accept, before the handshake, so a send in between waited for the timeout while Claude was connected.
G: a queued mention kept its raw path, while a connected send was made absolute.

Four more came up in review of #454's fixes and while #480 was built, and this model's second version found one. #480 fixed all five. Items 13 and 14 were in #480's own intermediate commits and never reached main:

A second client's handshakes postponed a due flush (Codex, round 6 on fix(mention): deliver queued @mentions once, in order, or report an error #454).
A write that libuv refused at once dropped the mention with no error.
Clients that connected and left without overlap kept a mention waiting with no error.
On a head of fix(mention): give each queued mention a deadline, keep a due flush on another client's handshake, and report refused writes #480 before its drain rule (cefe258), with many mentions queued while Claude started, the first deadline cleared the rest while a ready Claude was taking them, 25 ms apart. With 100 mentions and a handshake 8.6 s after the send, fewer than half arrived, and the count changed with the host's load. drain.lua passes only when all 100 arrive, in order, with no error.
Found by this model: when Neovim ran the handshake's on_open callback late, the deadline found Claude ready before any flush was due, cleared nothing and stopped. When that Claude left before on_open ran, nothing sent or cleared the queue. The spared deadline now schedules a flush.

Proof

On the head of this PR, after merging main at 9bfc39c. The statechart runs ran on 195c1d8. The model and statechart-view.ts are unchanged since then, and the main merges after it change no mention-queue behavior:

check.sh: PASS, exit 0. main 270,120 distinct states, live-NoStrandedMention 57,814, live-ReadyDelivers 57,814, live-FlushDelivers 24,692. All 19 facts read TRUE.
check.sh --mutants: exit 0 on 86e2359 (the round-3 verifier's run, 2494 s). Every guard is caught by the rule EXPECT names, and every rule breaks at least once. Since then the model changed only in comments, check.sh and scripts/tla/ are byte-identical, and the merged code still reads all 19 facts TRUE, so each mutant run gets the same TLC input.
A scratch break of one guard in lua/ (expire_mentions spares a ready client's queue without scheduling a flush) makes check.sh exit 1: SparedQueueFlushes reads FALSE and live-NoStrandedMention is BROKEN. After the restore, git diff --shortstat is empty.
scripts/tla/test-check-lib.sh: 44 cases, 0 failed.
replays/run.sh, the same replays on four trees, old trees on Neovim 0.12.3:
- this head: 12 of 12 kept their promise on Neovim 0.8.0 and 12 of 12 on 0.12.3.
- b92e7ac (the code before fix(mention): deliver queued @mentions once, in order, or report an error #454): 0 of 12. Each replay prints its bug, for example order gets second.txt, first.txt, stop-in-wait gets init.lua:234: attempt to index field 'server' (a nil value), and churn loses the mention with no error.
- 08dbcae (the code before fix(mention): give each queued mention a deadline, keep a due flush on another client's handshake, and report refused writes #480) and d1a6724 (a fix(mention): give each queued mention a deadline, keep a due flush on another client's handshake, and report refused writes #480 head before the deadline per mention): 11 of 12. churn keeps the mention queued with no error.
churn, 10 runs on this head: 10 kept, the mention cleared with one error 10605 to 10655 ms after the send. The replay now refreshes the loop clock before the send and reads the send and the clearing on that clock, the one that stamps the deadline. Before, it read real time against a loop clock that lagged 17 to 26 ms after setup(), and printed BROKEN on correct code in about half the runs.
order with a scratch loss of the second mention (a second table.remove(queue, 1) in the flush): BROKEN, exit 1. On this head: KEPT. Before, its verdict counted a lost second mention as kept. The other replays pass their verdict expression straight to L.verdict, so a false or nil reads BROKEN there.
replays/run.sh portability (Codex round 2): from a checkout path with a space, with OUT=./rel-logs and NVIM=./bin/nvim, 2 of 2 replays kept, and every XDG_*_HOME sits under the absolute OUT. On the same path, eb16b3a's run.sh printed no verdict (E518: Unknown option). Each run is now bounded by perl -e 'alarm 120; exec @ARGV', not GNU timeout: the same wrapper with alarm 2 ended a hung headless Neovim after 2 s.
replays/run.sh exit codes (Codex round 5): a replay counts as KEPT only when it printed KEPT and its Neovim exited 0. I added two scratch replays to a copy of this head. One prints KEPT and then exits 1: it reads BROKEN … Neovim exited 1 after the verdict "KEPT …". The other prints KEPT and quits as L.verdict does: it reads KEPT. The 12 real replays read KEPT on Neovim 0.8.0 and on 0.12.3.
replays/run.sh on Neovim 0.8 (Codex round 3): each replay now runs through :luafile, as .github/workflows/test.yml does, since nvim -l needs Neovim 0.9. On 0.8.0 and 0.12.3, from a checkout path with a space and with a relative OUT, a replay that raises before its verdict reads BROKEN … printed no verdict within 3 s, with its error in the log.
statechart-view.ts: /statechart refuses a view whose regions change between states, so every state now has the regions "Sent early", "Lua error" and "Sent after a stop". Each one reads "no" until its harm happens. The generator charted three scratch breaks with 1 mention and 1 connect, and each exited 1 with a chart:
- StopClearsQueue off, against NothingAfterStop: the flush after the stop raises a Lua error.
- FlushWaitsForReady off, against SentWhenReady.
- StopClearsQueue off, against ~leaked alone: the last state shows "Sent after a stop: a mention queued before :ClaudeCodeStop reached a Claude after the stop".
  Pele 1.9.0 rendered each chart to SVG. On the same leak input, 93fb4cb's view exited 2 ("Return the same regions for every state") and charted nothing.
verify-diff-lifecycle/check.sh: PASS. Main's fix(server): log Authenticated after the token check and run git once per lookup #539 added a log line to on_open and changed a comment in tcp.lua. The flush is still scheduled the same way, so I re-recorded the mention model's covered.lock after check.sh read all 19 facts TRUE.
busted, full suite, shuffled (seed 12345): 1709 successes, 0 failures, 0 errors, 25 pending. luacheck: 0 warnings in 181 files. treefmt --ci: 0 files changed. shellcheck (--exclude=SC1091,SC2016) on check.sh and replays/run.sh: clean.

Repro of the known bug: disable_broadcast_debouncing skips the readiness wait

It runs the real plugin in a headless Neovim with a loopback Claude, sends right after the handshake, and measures on the loop clock that stamps connected_at. Save it as repro-immediate.lua in the repo root, then run from there (IMMEDIATE=0 is the default config):

repo=$PWD dir=$(mktemp -d)
cp repro-immediate.lua "$dir" && cd "$dir"
for imm in 1 0; do
  CLAUDE_CONFIG_DIR="$dir/claude" REPLAY_LIB="$repo/.agents/skills/verify-mention-queue/replays/lib.lua" IMMEDIATE=$imm \
    nvim --headless -u NONE -i NONE --cmd "set rtp^=$repo" -c 'luafile repro-immediate.lua' -c 'cquit 1'
done

-- Does a send right after Claude's handshake reach Claude before connection_wait_delay has passed?
-- IMMEDIATE=1 sets disable_broadcast_debouncing = true; otherwise the default config (control).
-- Times are on the loop clock that the plugin stamps connected_at with (vim.loop.now()).
local uv = vim.uv or vim.loop
local L = dofile(vim.env.REPLAY_LIB)
local immediate = vim.env.IMMEDIATE == "1"
local cc = require("claudecode")
cc.setup({ terminal = { provider = "none" }, track_selection = false, disable_broadcast_debouncing = immediate })
assert(cc.state.server, "the server did not start")
local c = L.connect()
assert(L.upgrade(c), "no handshake")
local connected_at
for _, info in ipairs(require("claudecode.server.init").get_status().clients or {}) do
  if info.state == "connected" then
    connected_at = info.connected_at
  end
end
assert(connected_at, "no connected_at")
uv.update_time()
local sent_age = uv.now() - connected_at
L.send(L.file("early.txt"))
local got_age
vim.wait(2000, function()
  if #L.received(c) > 0 then
    uv.update_time()
    got_age = uv.now() - connected_at
    return true
  end
  return false
end, 1)
local wait = cc.state.config.connection_wait_delay
io.stdout:write(
  string.format(
    "RESULT disable_broadcast_debouncing=%s connection_wait_delay=%d sent %d ms after the handshake; Claude got it %s; queue=%d; %s\n",
    tostring(immediate),
    wait,
    sent_age,
    got_age and (got_age .. " ms after the handshake") or "never (2 s)",
    #(cc.state.mention_queue or {}),
    (got_age and got_age < wait) and "BEFORE READY" or "after ready"
  )
)
vim.cmd("qall!")

Output:

NVIM v0.12.3: RESULT disable_broadcast_debouncing=true connection_wait_delay=600 sent 4 ms after the handshake; Claude got it 7 ms after the handshake; queue=0; BEFORE READY
NVIM v0.12.3: RESULT disable_broadcast_debouncing=false connection_wait_delay=600 sent 4 ms after the handshake; Claude got it 600 ms after the handshake; queue=0; after ready
NVIM v0.8.0-1210-gd367ed9b2: RESULT disable_broadcast_debouncing=true connection_wait_delay=600 sent 3 ms after the handshake; Claude got it 3 ms after the handshake; queue=0; BEFORE READY
NVIM v0.8.0-1210-gd367ed9b2: RESULT disable_broadcast_debouncing=false connection_wait_delay=600 sent 3 ms after the handshake; Claude got it 600 ms after the handshake; queue=0; after ready

How to run

.agents/skills/verify-mention-queue/check.sh            # about 60 s
.agents/skills/verify-mention-queue/check.sh --mutants  # 25 to 50 min
NVIM=nvim .agents/skills/verify-mention-queue/replays/run.sh  # about 2 min

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

…queue Adds .agents/skills/verify-mention-queue/: a TLA+ model of the @mention queue and the WebSocket clients it sends to (init.lua queue_mention, schedule_mention_flush, flush_mention_queue, expire_mentions, ms_until_a_client_is_ready, M.stop; on_open and broadcast in server/; the handshake, write and send paths in server/client.lua), a check.sh on the shared harness scripts/tla/check-lib.sh, a /statechart view, and headless Neovim replays. check.sh reads 19 guards from the code and checks 8 rules: NoSilentDrop, SentInOrder, AtMostOnce, SentWhenReady, NothingAfterStop, and the liveness rules NoStrandedMention, ReadyDelivers and FlushDelivers. SKILL.md lists the bugs the model found and the PRs that fixed them (#454, #480). Each replay shows the promise kept on the code.

… was described The verify-claudecode-nvim send-queue feature, the queue_timeout comments in config.lua and dev-config.lua, the issue-70 fixture, and the connection_timer type said that mentions wait up to connection_timeout, or named only the connection timeout error. Since #480 a mention times out connection_timeout + connection_wait_delay after its send, a client that is connected but not ready yet gets the Send timeout error, and the deadline timer is nil while a ready client drains the queue.

…f connection_wait_delay The advisor on #480 found that no test pins the length of the wait: a flush that sent once the wait left was under 200 ms passed every test. This one sends 400 ms after the handshake and expects nothing at 550 ms and the mention at 650 ms.

…ound

#480

ThomasK33 · 2026-11-11T18:20:58Z

@codex review

ThomasK33 · 2026-11-11T18:21:00Z

@codex security review

chatgpt-codex-connector · 2026-11-11T18:21:12Z

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-12T07:37:54.080198Z	`06ccb52`	Manual request
🔒 Security Review	✅ Completed 2026-11-12T07:33:13.924442Z	`06ccb52`	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-11T18:23:56Z

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

Reviewed commit: a6dda5e4c6

ℹ️ About Codex in GitHub

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

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

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

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

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

🛡️ Codex Security Review

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

Reviewed commit: a6dda5e4c6

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.

…ter a spared deadline

…ady client A send 540 ms after the handshake must wait the last 10 ms, so a flush that sent while under 20, 100 or 200 ms of the wait were left fails. A second client that connected later must not hold the flush for the first ready client, so a readiness that waits for the newest client fails.

… before the fixes sync.lua now also accepts the empty queue that the handshake left before #454, so the five replays that use it run through on that code. churn.lua sends while no client is connected, the path that hung before #480.

…ndings, and the scope notes

…-queue

…mment and the main merge

ThomasK33 · 2026-11-11T20:58:58Z

@codex review

ThomasK33 · 2026-11-11T20:59:00Z

@codex security review

chatgpt-codex-connector · 2026-11-11T21:02:11Z

🛡️ Codex Security Review

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

Reviewed commit: eb16b3aa24

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: eb16b3aa24

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

…-queue

…rrect the skill's notes churn.lua refreshes the loop clock before the send and measures on it, so a correct deadline no longer reads early. order.lua counts a lost second mention as BROKEN. SKILL.md: churn.lua does not catch a QueueKeepsDeadline revert alone, the cefe258 drain count is 41 to 43, the readiness-wait example keeps the wait > 0 test, --mutants takes up to 50 min, and ClaudeCodeSendComplete fires only on the connected path.

…made while Claude is not connected

…ith a space, and with a relative OUT Codex round 2 on #523: run.sh used GNU timeout, interpolated the checkout path into `set rtp^=`, and built the XDG paths from a relative OUT after the cd. perl's alarm now bounds each run, REPLAY_REPO reaches 'runtimepath' through Lua, and OUT and a relative NVIM become absolute before the loop.

ThomasK33 · 2026-11-12T00:04:55Z

@codex review

ThomasK33 · 2026-11-12T00:04:57Z

@codex security review

chatgpt-codex-connector · 2026-11-12T00:11:03Z

🛡️ Codex Security Review

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

Reviewed commit: 86e235954d

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.

… that a follow-up PR fixes

ThomasK33 · 2026-11-12T03:29:37Z

@codex review

ThomasK33 · 2026-11-12T03:29:39Z

@codex security review

chatgpt-codex-connector · 2026-11-12T03:31:44Z

Codex Review: Something went wrong. Try again later by commenting “@codex review”.

Failed to set up container

ℹ️ 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-12T03:32:38Z

Codex Review: Didn't find any major issues. Already looking forward to the next diff.

Reviewed commit: 93fb4cb03c

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

…-queue

…, and widen two measured ranges /statechart refuses a view whose state() returns different region keys across states, so a SentWhenReady or NothingAfterStop break charted nothing. The Sent early, Lua error and Sent after a stop regions are now in every state, as "no" until their harm happens. SKILL.md: the cefe258 drain delivered 30 to 45 in our runs, and the immediate path reached Claude a few ms after the handshake (3 to 10 in our runs).

…ine and tcp.lua comment (#539)

…-queue

ThomasK33 · 2026-11-12T06:22:14Z

@codex review

ThomasK33 · 2026-11-12T06:22:16Z

@codex security review

chatgpt-codex-connector · 2026-11-12T06:25:36Z

🛡️ Codex Security Review

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

Reviewed commit: 3ceb6ecc2c

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: 3ceb6ecc2c

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

…-queue

… exited 0 Codex round 5 on #523: run.sh counted a replay that printed KEPT and then exited nonzero (a failing VimLeavePre, the alarm) as kept. It now reads BROKEN with the exit code. SKILL.md: say so, and give the cefe258 drain as fewer than half, since the count changed with the host's load.

ThomasK33 · 2026-11-12T07:28:50Z

@codex review

ThomasK33 · 2026-11-12T07:28:53Z

@codex security review

chatgpt-codex-connector · 2026-11-12T07:33:12Z

🛡️ Codex Security Review

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

Reviewed commit: 06ccb5213e

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 · 2026-11-12T07:37:52Z

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

Reviewed commit: 06ccb5213e

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

…sual-edit tests (coder#553) ## What failed CI run 43167645889 (job `integration-tests (stable)`, PR coder#523, head `3ceb6ecc`) failed `tests/integration/selection_visual_edit_spec.lua:230`, "sends no selection for d after a :write in visual mode", with `{false, 'alpha'}`. ## Cause: a timing bug in the test, not in the plugin The test presses `ve`, waits 20 ms, runs `:write`, waits 20 ms and presses `d`. It then asserts that Claude was never sent a non-empty selection. That holds only while `d` comes within the 100 ms debounce of `ve`. When anything delays the keys past it (a slow `:write` on a busy host, a stalled loop), the debounce sends the selection that you are still making, with the mode still visual. That send is right: you did select `alpha`. The plugin then sends the cursor (an empty selection) the moment `d` runs. `sent_no_selection` counted every message, so it also counted the right one. I traced it with time stamps, on Neovim 0.12.3 and 0.8.0. In every failing run the sequence is the same: ``` 0 ms press ve 20 ms write start 167 ms write end 167 ms SENT text="alpha" empty=false mode=v <- the debounce, before d 247 ms press d 297 ms SENT text="" empty=true mode=n <- the cursor, right after d ``` A phantom after `d` would carry ` beta` (the text at the old marks) and a mode other than `v`. None of the 30 traces has one. A deterministic repro makes `:write` block for 150 ms with a `BufWritePost` autocmd: the same sequence, the same failure, and the plugin ends with the cursor held and ` beta gamma` on line 1. The sibling test "sends no selection for d after a plugin edited another line in visual mode" has the same shape and failed too (`wait(20)` stalled). The `ved`, `vec` and `Vj>` tests press all their keys in one `press`, so no timer can fire between them. ## The fix Round 1 (`43a12838`): `sent_no_selection(from)` looks only at the messages after number `from`. The two tests record `#sent` before they press `d`, and assert that a selection sent before the operator is the one the user made. With the flush made to never skip (`if false and entry ...`), the five operator tests fail on both versions, these two included. Round 2 (the Opus verifier's two findings): - **F1, a second flake in the same tests (also on `main`).** After an operator the plugin sends the cursor when its flush or the debounce has run, and `get_latest_selection()` is `nil` until then. A host that stalls the loop past the fixed `wait(400)` made the test fail with `attempt to index a nil value`. The five operator tests (`ved`, `vec`, `Vj>`, and the plugin-edit and `:write` tests) now call `wait_for_cursor()`: `vim.wait` with a condition (the plugin holds an empty selection) and a 5 s limit, then `wait(200)` so that a selection sent late by the debounce would still show. The release tests keep `wait(400)`: the flush on Esc sends the selection before `press` returns, so `get_latest_selection()` is never `nil` there. - **F2, the early-selection check compared only the text.** `assert_is_the_selection` checks the text and the range (`0:0` to `0:5`) of every selection sent before the operator. Round 3 (Codex P2): when the debounce sends `alpha` before `d`, the tests passed even if the plugin only forgot the selection locally and never sent the cursor. Each of the five operator tests now also asserts that the last `selection_changed` sent is a cursor. A mutant whose flush sets `latest_selection` to the cursor without sending it passes the round-2 spec 12 of 12, and fails this spec's plugin-edit and `:write` tests under the 150 ms stall on both versions (a verifier reran it: 2 of 12 fail, those two). Without a stall, `tests/selection_test.lua` already catches that mutant. ## Proof Deterministic stalls, on Neovim 0.12.3 and 0.8.0 (generated copies of the spec, not part of the PR): | Stall | Old spec (`main`) | Round-1 spec | This spec | | --- | --- | --- | --- | | 150 ms between the selection and `d` (`:write` and plugin-edit tests) | 2 of 12 fail (`{false,'alpha'}`) | passes | 12 of 12 pass | | loop blocked 450 ms right after the operator (the five operator tests) | 5 of 12 fail (`attempt to index a nil value`) | 5 of 12 fail | 12 of 12 pass | | no stall | 12 of 12 | 12 of 12 | 12 of 12 | Wrong range, right text (the in-visual selection sent with its end line moved by 5), with the 150 ms stall: the round-1 spec passes 12 of 12 on both versions, and this spec fails the plugin-edit and `:write` tests (both on 0.8.0 and in 3 of 4 runs on 0.12.3, one run failed only the `:write` test). Same-window load (24 runners in parallel and 8 `dd conv=fsync` loops, or 40 runners with 12 disk loops and 16 CPU burners): | Window | Old or round-1 spec: runs that failed | This spec | | --- | --- | --- | | round 1, 0.12.3, old spec | 25 of 72 (`{false,'alpha'}`) | 0 of 72 (round-1 spec) | | round 1, 0.8.0, old spec | 4 of 72 | 0 of 72 (round-1 spec) | | round 2, 0.12.3, 40 runners, round-1 spec | 24 of 80 (all 24 `attempt to index a nil value`: `Vj>` 15, `vec` 7, `:write` 1, `ved` 1) | 0 of 80 (round-2 spec) | | this head (verifier rerun, load up to about 114) | not reproduced: the round-1 spec also passed 0 of 80 | 0 of 80 on 0.12.3, 0 of 40 on 0.8.0 | A window with lower load had no failure for either spec (0 of 72 each), so the deterministic stalls above are the proof and the load windows the check. Other gates: the spec passes 12 of 12 on both versions on an idle host. The CI-style integration runner (private `HOME`, normal and `odd tmp 50%` `TMPDIR`) passes with 417 tests per run on 0.12.3 and 309 per run on v0.8.0, and leaves the real cache untouched. `luacheck` shows 0 warnings in 181 files and `treefmt --ci` 0 changes. ## Notes for the reviewer coder#540 moves `sent_no_selection` to the outer scope of this spec and adds cases that use it. It resolves the conflict when it merges `main`. --- _Generated with [`xum`](https://github.com/coder/xum) • Model: `anthropic:claude-sonnet-5-5` • Thinking: `xhigh`_

…ing off (coder#541) ## What this fixes With `disable_broadcast_debouncing = true` and an empty queue, `_broadcast_at_mention` broadcast a send at once and skipped the readiness check. A Claude whose WebSocket handshake completed less than `connection_wait_delay` ms ago (600 ms by default) got the mention while it was still starting up. On real Neovim 0.8.0 and 0.12.3 it arrived 3 to 10 ms after the handshake. With the default config the same send waits the full 600 ms. The option is not in the README or the `config.lua` defaults. It is typed in `types.lua` and described in `lua/claudecode/README.md`, so a user config can set it. The fix is in `lua/claudecode/init.lua` (`M._broadcast_at_mention`): the immediate path now also needs `ms_until_a_client_is_ready()` to be 0. That means some connected client completed its handshake `connection_wait_delay` ms ago. Otherwise the mention goes through the queue, which sends it once a client is ready. Behavior is unchanged in two cases: - Some client is ready: the send still goes out at once, with nothing queued. - No client reports a handshake time: the immediate path still runs and fails at once with "Failed to broadcast …", as before. The verify-mention-queue skill (coder#523, now on main) found this through a Codex review on its model. coder#523 excluded this config from its `SentWhenReady` rule as a known bug. coder#523 merged first, so this PR adds the model branch and flips that wording. ## The verify-mention-queue model now covers this path - `model/MentionQueue.tla`: a new variable `immediate` holds the user's `disable_broadcast_debouncing`. Each run starts with either value and keeps it. With it on, a send while Claude is connected and the queue is empty broadcasts at once while some connected client is ready. Otherwise the send queues as before. The writes all succeed, all fail later, or are refused at once, as in a flush. - `check.sh`: a new fact, `ImmediateWaitsForReady`, read from `_broadcast_at_mention`. It reads TRUE only when the readiness guard comes before every `.broadcast(` and `queue_mention(` line of that function (a broadcast written as an indexed call or through an alias still reads TRUE; the unit tests catch those), so an unguarded broadcast added before the guard reads FALSE. With it FALSE, `SentWhenReady` breaks. `FailedWriteReported` now also reads the immediate send's `report_unwritten("command", …)`. - `SKILL.md`: `SentWhenReady` holds with `disable_broadcast_debouncing` on or off. The scope note now describes the check instead of a known bug, and the facts table lists the new fact. ## Tests The first two tests were committed before the fix (ebcdb89) and failed on main: - `tests/unit/mention_queue_spec.lua`, `D: with debouncing off, a send right after the handshake still waits for connection_wait_delay`: a fake loop runs a send 100 ms after the handshake. It expects the mention in the queue, nothing at 590 ms and the mention at 610 ms. On main the queue stayed empty and the mention went out at once. - `tests/integration/mention_immediate_send_spec.lua` (real Neovim, so CI runs it on stable and v0.8.0): a loopback Claude completes the handshake. - A send right after the handshake must reach Claude only once `connection_wait_delay` has passed. The time is measured on the loop clock that stamps `connected_at`. On main: `Claude got the mention 3 ms after its handshake, before 600 ms` (0.8.0) and `6 ms` (0.12.3). - A send once Claude is ready must still go out at once, with nothing queued. This one passes before and after the fix. - `tests/unit/mention_queue_spec.lua`, `D: with debouncing off, a send 1 ms before Claude is ready still waits in the queue` (verifier F1 on 24b7ee7, tightened after the verifier on 700cbf6). The first two tests send 500 ms or more before ready, so a readiness check with a tolerance survived them. The fake clock makes the 1 ms exact on any Neovim. Each of these mutations of the guard fails only this test: `< 2`, `< 20`, `<= 20` and `< 100`. With the fix, the spec passes 53 of 53. ## Replay runner and wording (minor findings from coder#523 round 6) - `replays/run.sh`: it exits 2 before the first replay when `NVIM` names no Neovim, and the error names the path as given. A `NVIM` in a missing folder used to turn into `/nvim`. bash's "Alarm clock" note now goes to the replay's log, not the terminal. The comment no longer cites a VimLeavePre error, because Neovim exits 0 after one. - `drain.lua` and `SKILL.md` now say "an 8.6 s wait before Claude connects" where they said "handshake". ## Checks run The gates ran on 4a06553, with main at d123707. The head then merges main's 37ee1e3 (coder#554, coder#564): `diff_inline.lua`, the integration runner and diff specs. None of them touches the mention queue or a file of this PR, and all four `covered.lock` files match the head. Two results ran on earlier commits: - `--mutants` ran on 3980bc3. Since then `check.sh` changed only in how it reads `ImmediateWaitsForReady`, which still reads TRUE, so each mutant run gets the same TLC input. - The statechart runs ran on 334f122. The model is the same on the head. The results on 4a06553: - `verify-mention-queue/check.sh`: PASS, 20 facts TRUE. `main` 540,240 distinct states, `live-NoStrandedMention` 115,628, `live-ReadyDelivers` 115,628, `live-FlushDelivers` 48,296. Three counts are exactly twice the old ones and `live-FlushDelivers` is 1.96 times (24,692 before), because each run checks both values of `immediate`. - `verify-mention-queue/check.sh --mutants`: exit 0 in 6543 s on a loaded host (load average about 60 to 118). Every guard is caught by the rule `EXPECT` names (`ImmediateWaitsForReady=FALSE` by `SentWhenReady`), and every rule breaks at least once. - A scratch copy of the model with an action property that says the immediate send never happens: TLC breaks it (314 states, 1 mention, 1 connect), so the branch is reachable. With `ImmediateWaitsForReady = FALSE`, `SentWhenReady` breaks. - `/statechart` with the committed view still charts three scratch breaks, `StopClearsQueue` and `FlushWaitsForReady` off. All 3 exited 1 with a chart. - Every other `verify-*/check.sh` passes: - `verify-diff-lifecycle`: 89,205 / 5,269 states. Its lock merged from main. - `verify-selection-tracking`: 129,986 states. - `verify-terminal-lifecycle`: 263,060 states. - The selection and terminal models hash all of `init.lua`, so I re-recorded their `covered.lock` files after the fix. Neither model reads `_broadcast_at_mention`. - `replays/run.sh`: 12 of 12 kept on Neovim v0.8.0 and 12 of 12 on v0.12.3, on the head. - With `NVIM=/nonexistent/nvim`, `./no-such-nvim` or `nvim-not-on-path`, it exits 2 before any replay and names the path. - On a copy of the head, a replay that prints KEPT and exits 1 reads BROKEN. A replay that hangs is ended by the alarm and reads BROKEN with exit 142. "Alarm clock" is in its log, and the terminal got 0 bytes of stderr. - busted, full suite, shuffled (seed 12345): 1769 successes, 0 failures, 0 errors, 29 pending. - `scripts/run_integration_tests_individually.sh`: Neovim v0.8.0, 400 successes, 0 failed, 0 errors. Neovim v0.12.3, 537 successes, 0 failed, 0 errors. `mention_immediate_send_spec.lua` passed 2 of 2 on each version. - `ImmediateWaitsForReady` reads TRUE on the head. With an unguarded broadcast before the guard (the verifier's probe R4), it reads FALSE. - luacheck: 0 warnings in 186 files. `treefmt --ci`: 0 files changed. ## Repro ```lua -- In a headless Neovim with the plugin on 'runtimepath', CLAUDE_CONFIG_DIR set to a temp dir: require("claudecode").setup({ terminal = { provider = "none" }, track_selection = false, disable_broadcast_debouncing = true }) -- Connect a WebSocket client, complete the handshake, then right away: require("claudecode").send_at_mention(vim.fn.getcwd() .. "/a.txt", nil, nil, "repro") -- Before this fix the client gets the at_mentioned frame within a few ms. After it, it arrives 600 ms after the handshake. ``` `tests/integration/mention_immediate_send_spec.lua` is the runnable form. --- _Generated with [`xum`](https://github.com/coder/xum) • Model: `anthropic:claude-opus-5-5` • Thinking: `xhigh`_

ThomasK33 added 6 commits November 11, 2026 17:33

chore(skills): re-record the diff model after the queue comment fixes

5dfe9d7

docs(skills): count the four findings that review of the #454 fixes f…

d56790f

…ound

chore(skills): record the verify-mention-queue model against main after

a6dda5e

#480

ThomasK33 added 6 commits November 11, 2026 20:10

docs(types): connection_timer runs during a drain, and is nil only af…

38a6430

…ter a spared deadline

docs(skills): correct the deadline guard pair, the churn and drain fi…

f72a3e5

…ndings, and the scope notes

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

295db38

…-queue

chore(skills): re-record the diff model after the connection_timer co…

eb16b3a

…mment and the main merge

chatgpt-codex-connector Bot reviewed Nov 11, 2026

View reviewed changes

Comment thread .agents/skills/verify-mention-queue/replays/run.sh Resolved

Comment thread .agents/skills/verify-mention-queue/replays/run.sh Resolved

Comment thread .agents/skills/verify-mention-queue/replays/run.sh Resolved

ThomasK33 mentioned this pull request Nov 11, 2026

chore(skills): add a tools/call wire probe to the verify-claudecode-nvim skill #517

Merged

ThomasK33 added 5 commits November 11, 2026 23:23

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

85f2101

…-queue

docs(skills): say that ClaudeCodeSendComplete never fires for a send …

d0dae1f

…made while Claude is not connected

docs(skills): say that perl bounds each mention replay

86e2359

docs(skills): call the immediate-broadcast readiness skip a known bug…

93fb4cb

… that a follow-up PR fixes

ThomasK33 mentioned this pull request Nov 12, 2026

fix(queue): keep the readiness wait for a send with broadcast debouncing off #541

Merged

ThomasK33 added 5 commits November 12, 2026 05:38

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

1ff11a3

…-queue

chore(skills): re-record the mention model after main's on_open log l…

195c1d8

…ine and tcp.lua comment (#539)

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

bc61ca1

…-queue

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

3ceb6ec

…-queue

chatgpt-codex-connector Bot reviewed Nov 12, 2026

View reviewed changes

Comment thread .agents/skills/verify-mention-queue/replays/run.sh Resolved

ThomasK33 added 2 commits November 12, 2026 06:55

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

82424d0

…-queue

ThomasK33 mentioned this pull request Nov 12, 2026

test(selection): count only what is sent after the operator in two visual-edit tests #553

Merged

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

github-merge-queue Bot removed this pull request from the merge queue due to failed status checks Nov 12, 2026

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

Merged via the queue into main with commit e4c56fd Nov 12, 2026
7 checks passed

ThomasK33 deleted the skills/verify-mention-queue branch November 12, 2026 08:49

Conversation

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

Uh oh!

What this adds

What the model checks

Bugs it found, and the fixes

Proof

How to run

Uh oh!

ThomasK33 commented Nov 11, 2026

Uh oh!

ThomasK33 commented Nov 11, 2026

Uh oh!

chatgpt-codex-connector Bot commented Nov 11, 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 11, 2026

Uh oh!

chatgpt-codex-connector Bot commented Nov 11, 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!

Uh oh!

ThomasK33 commented Nov 12, 2026

Uh oh!

ThomasK33 commented Nov 12, 2026

Uh oh!

chatgpt-codex-connector Bot commented Nov 12, 2026

🛡️ Codex Security Review

Uh oh!

ThomasK33 commented Nov 12, 2026

Uh oh!

ThomasK33 commented Nov 12, 2026

Uh oh!

chatgpt-codex-connector Bot commented Nov 12, 2026

Uh oh!

chatgpt-codex-connector Bot commented Nov 12, 2026

Uh oh!

ThomasK33 commented Nov 12, 2026

Uh oh!

ThomasK33 commented Nov 12, 2026

Uh oh!

chatgpt-codex-connector Bot commented Nov 12, 2026

🛡️ Codex Security Review

Uh oh!

chatgpt-codex-connector Bot left a comment

Choose a reason for hiding this comment

💡 Codex Review

Uh oh!

Uh oh!

ThomasK33 commented Nov 12, 2026

Uh oh!

ThomasK33 commented Nov 12, 2026

Uh oh!

chatgpt-codex-connector Bot commented Nov 12, 2026

🛡️ Codex Security Review

Uh oh!

chatgpt-codex-connector Bot commented Nov 12, 2026

Uh oh!

Uh oh!

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

ThomasK33 commented Nov 11, 2026 •

edited

Loading

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

edited

Loading