Verify Mention Queue

---
name: verify-mention-queue
description: Model-check the claudecode.nvim @ mention queue and the WebSocket clients it sends to (TLA+/TLC) against guards read from the current Lua code. Use after a change to how @ mentions are queued, flushed, timed out, or dropped, to when a client counts as connected or ready, to how a broadcast reports its writes, or to what a stop does to the queue (lua/claudecode/init.lua send_at_mention, _broadcast_at_mention, queue_mention, schedule_mention_flush, flush_mention_queue, expire_mentions, ms_until_a_client_is_ready, report_unwritten, clear_mention_queue, process_mention_queue, M.stop, on_open and broadcast in server/init.lua, the connect and broadcast paths in server/tcp.lua, the handshake, write and send paths in server/client.lua), and before trusting such a change.
---

# Verify the @ mention queue

You send a file or a selection to Claude with `:ClaudeCodeSend`, `:ClaudeCodeAdd` or a tree command. The plugin puts the mention in one queue, oldest first. Each mention gets a deadline, `connection_timeout + connection_wait_delay` ms after the send (10.6 s by default). A flush sends the oldest mention once some connected client has been connected for `connection_wait_delay` ms since its WebSocket handshake. The broadcast reaches every connected client. A mention still queued at its deadline leaves with an error, unless a ready client is connected: then the queue drains to that client, 25 ms apart, also past the deadlines, and a flush that finds no ready client clears the mentions whose deadline passed meanwhile. This check explores every order of your sends, the clients' connects, handshakes, closes and drops, the plugin's timers and scheduled callbacks, and `:ClaudeCodeStop`/`:ClaudeCodeStart`, in a small model, with each guard switched on or off to match the code as it is now.

## Rules

| Rule                | Plain sentence                                                                                                                                                                       | Harm when broken                                                                                                                 |
| ------------------- | ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ | -------------------------------------------------------------------------------------------------------------------------------- |
| `NoSilentDrop`      | A mention you sent reaches Claude, or you see an error, unless you stopped the integration first.                                                                                    | Claude never gets the context you sent, and nothing tells you, so you ask Claude about a file it never saw.                      |
| `SentInOrder`       | Each Claude gets the mentions in the order you sent them.                                                                                                                            | Claude reads your context out of order, for example the follow-up selection before the file it refers to.                        |
| `AtMostOnce`        | Each Claude gets each mention at most once.                                                                                                                                          | Claude gets the same context twice and counts it twice.                                                                          |
| `SentWhenReady`     | A mention goes out only while some connected client has been connected for `connection_wait_delay` ms since its handshake. This holds with `disable_broadcast_debouncing` on or off. | Claude gets the mention inside the `connection_wait_delay` that the plugin leaves it to start up after its handshake.            |
| `NothingAfterStop`  | After `:ClaudeCodeStop`, no mention queued before the stop reaches Claude, and the queue raises no Lua error.                                                                        | A Lua error appears after you stopped the integration, or a mention from before the stop reaches a new Claude session.           |
| `NoStrandedMention` | Every queued mention leaves the queue: it is sent, dropped with an error at its deadline, or cleared by a stop (liveness).                                                           | The mention waits with no timer, so you never get the error that would tell you to send it again.                                |
| `ReadyDelivers`     | While a ready Claude stays connected, every queued mention goes out to it (liveness).                                                                                                | Claude is connected and ready, and the mentions you sent never arrive, or leave as a timeout error while Claude takes the queue. |
| `FlushDelivers`     | While a ready Claude stays connected, the flushes alone send it every queued mention: none waits for a deadline to pass first (liveness).                                            | A mention reaches Claude only once a deadline passes, 10.6 s after the send, not 25 to 600 ms after Claude is ready.             |

The liveness rules assume that every timer fires, every scheduled callback runs, a 101 write completes, a closing socket closes, and time passes, so a client that stays connected becomes ready. They never assume that you or Claude act. `FlushDelivers` runs with no deadline that passes: in this untimed model a deadline can pass at any step, and a deadline that spares a ready Claude schedules a flush, so it would hide a flush path that leaves a ready Claude waiting for a deadline.

## Run

```bash
.agents/skills/verify-mention-queue/check.sh            # about 60 s
.agents/skills/verify-mention-queue/check.sh --keep     # same, keeps the TLC configs and output, prints the dir
.agents/skills/verify-mention-queue/check.sh --mutants  # 25 to 50 min, after you edit the model or a fact
.agents/skills/verify-mention-queue/check.sh --record   # rewrite covered.lock, only after "Update after an intended change"
.agents/skills/verify-mention-queue/check.sh --hash-only  # under 1 s, no TLC: only compares covered.lock with the code (exit 0 or 3)
```

`check.sh` sources `scripts/tla/check-lib.sh`, the shared harness. Read its header for the options. CI runs every `.agents/skills/verify-*/check.sh` in the `covered-lock` job. The job is not required, so a PR that breaks a rule shows it red but can still merge.

Needs bash 4 or newer, Java 11 or newer (`JAVA=/path/to/java` overrides `java`), `sha256sum` or `shasum`, and curl for the first run, which downloads TLC 1.7.4 to `~/.cache/claudecode-nvim-tla/` and refuses a jar whose sha256 differs. Run one copy at a time on a shared host. TLC is CPU heavy.

Exit codes:

- `0` is PASS.
- `1` means a rule broke.
- `2` is a tool or script error, or a model whose `TypeOK` breaks.
- `3` is STALE. The covered code changed since the model was last confirmed, so the change is unverified. A broken rule exits 1 even when the record is stale.

The main run checks the five invariants in one TLC run, which stops at the first break and names only that rule. Each liveness rule has its own run. To check one invariant alone, rerun with `--keep`, edit the `INVARIANT` line of `main.cfg` in the kept dir, and run TLC there on that cfg as `check-lib.sh` does (`java -cp <jar> tlc2.TLC -config main.cfg MentionQueue.tla`).

## Does the change touch the verified code?

Run the check. `covered.lock` records a hash of each covered file: `lua/claudecode/init.lua`, `lua/claudecode/config.lua`, `lua/claudecode/server/init.lua`, `lua/claudecode/server/tcp.lua` and `lua/claudecode/server/client.lua`. Any change to one of them reads `STALE` (exit 3, or 1 with a broken rule) until someone confirms that the model still describes the code.

To show where to look, the record also hashes each block the model describes, and lists every non-comment line that names the queue, its timers, its functions, the connection or readiness check, `connected_at`, the handshake flag, the delays, `at_mentioned`, `on_open` or `on_written`, with its enclosing top-level statement. The STALE output prints a `was:`/`now:` pair for each changed file, block or line.

Covered blocks:

- In `init.lua`: `M.is_claude_connected`, `ms_until_a_client_is_ready`, `start_timer`, `clear_mention_queue`, `expire_mentions`, `report_unwritten`, `flush_mention_queue`, `schedule_mention_flush`, `queue_mention`, `M.process_mention_queue`, `M.send_at_mention`, `M._broadcast_at_mention`, `M.stop`.
- In `server/init.lua`: the `on_open` callback, `M.broadcast`, `M.get_status`.
- In `server/tcp.lua`: `M._handle_new_connection`, `M.broadcast`, `M.get_clients_info`.
- In `server/client.lua`: `write`, `M.process_data` (the handshake), `M.send_message`, `M.get_client_info`.
- `config.lua` by its file hash: the `connection_timeout` and `connection_wait_delay` defaults set the deadline.

A changed file with no changed block or line still needs a look. The `VimLeavePre` autocmd in `M.setup` calls `M.stop`, or `clear_mention_queue()` when no server runs. The record lists that `clear_mention_queue()` line as a site of `M.setup`, and a change to the `M.stop` call shows only as a changed `init.lua`. The record groups lines by file, so two branches that edit different covered files and each re-record merge `covered.lock` without a conflict. Two branches that edit the same file conflict in `covered.lock` once one of them merges. To resolve it, merge `origin/main`, follow "Update after an intended change" on the merged code if it reaches the queue, run `check.sh --record`, and commit `covered.lock` with the merge. A PASS says that the model holds for the guards the facts read, on code that matches the record. It does not review a change. STALE never means "probably fine".

## Read the result

`check.sh` prints the code facts first. Each fact is read by a regex from the source. `TRUE` means the regex found the guard. `FALSE` means that the model runs without that guard. A `FALSE` you did not expect is either a removed guard (a bug) or a guard reworded past the regex (a modeling error). A change that keeps every fact `TRUE` reads only STALE: for example a broadcast that never reports its writes, a deadline that never comes, an `expire_mentions` that clears nothing, a closing client that counts as connected, a typo that stops `on_open` from scheduling the flush, a `get_client_info` without `handshake_complete`, a `schedule_mention_flush` that stops the deadline while Claude is connected, a refused piece of a large frame that hides its error, or a change of the readiness wait that keeps the `wait > 0` test (`math.max` in place of `math.min` over the clients, or 200 ms taken off the wait). The unit tests in `tests/unit/mention_queue_spec.lua`, `tests/unit/server_spec.lua` and `tests/unit/server/connection_lifecycle_spec.lua` catch those, so run them too. See below for how to tell them apart.

| Fact                      | Code it reads                                                                                                                                                                                                                                                                                                 | Rule without it                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
| ------------------------- | ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | --------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- |
| `EnqueueArmsDeadline`     | `queue_mention` appends the mention with its `deadline`, starts `connection_timer` with `expire_mentions` when none runs, then calls `schedule_mention_flush(debounce_delay)`                                                                                                                                 | `NoStrandedMention`                                                                                                                                                                                                                                                                                                                                                                                                                                                         |
| `DeadlineReportsError`    | `expire_mentions` calls `logger.error` ("Send timeout" while a Claude is connected, "Connection timeout" otherwise) before it removes the expired mentions                                                                                                                                                    | `NoSilentDrop`                                                                                                                                                                                                                                                                                                                                                                                                                                                              |
| `DeadlineRearms`          | `expire_mentions` calls `clear_mention_queue()` when the queue is empty, and otherwise starts `connection_timer` for `queue[1].deadline`                                                                                                                                                                      | `NoStrandedMention`                                                                                                                                                                                                                                                                                                                                                                                                                                                         |
| `DeadlineSparesReady`     | `expire_mentions` returns at once while `ms_until_a_client_is_ready()` is 0: it clears nothing while a ready client is connected                                                                                                                                                                              | `ReadyDelivers`                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
| `SparedQueueFlushes`      | in that branch, `expire_mentions` calls `schedule_mention_flush(inter_message_delay)` before it returns, so a flush is due even when the handshake's `on_open` callback has not run yet                                                                                                                       | `NoStrandedMention`                                                                                                                                                                                                                                                                                                                                                                                                                                                         |
| `FlushExpiresOverdue`     | `flush_mention_queue` calls `expire_mentions()` when it finds no ready client: in the wait branch, and when no connected client took the frame                                                                                                                                                                | `NoStrandedMention`                                                                                                                                                                                                                                                                                                                                                                                                                                                         |
| `QueueKeepsDeadline`      | `init.lua` stops `connection_timer` only in `clear_mention_queue` and in the empty-queue branch of `schedule_mention_flush`, and starts it only in `queue_mention` and `expire_mentions`: no handshake, flush or send moves a deadline                                                                        | `NoStrandedMention`, only with `FlushExpiresOverdue` removed too. Alone it breaks no rule here: the next flush that finds no ready client clears the overdue mentions and starts the deadline again, so only the time of the error changes. The tests `A, F4: a Claude whose handshake comes 10.3 s after the send …` and `S: clients that connect every 700 ms and stay 300 ms …` (and `… 650 ms and stay 500 ms …`) in `tests/unit/mention_queue_spec.lua` catch it alone |
| `HandshakeFlushes`        | the 101 write callback in `server/client.lua` sets state `connected`, then calls `on_open`. `server/tcp.lua` passes `server.on_open`, `on_open` in `server/init.lua` schedules `process_mention_queue(true)`, and that calls `schedule_mention_flush`                                                         | `FlushDelivers`                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
| `ConnectedSchedulesFlush` | `schedule_mention_flush` starts `mention_timer` with `flush_mention_queue` while `is_claude_connected()` and no flush is due                                                                                                                                                                                  | `FlushDelivers`                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
| `FlushWaitsForReady`      | `flush_mention_queue` returns before the broadcast while `ms_until_a_client_is_ready()` is above 0                                                                                                                                                                                                            | `SentWhenReady`                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
| `WaitRearmsFlush`         | in that branch, `flush_mention_queue` starts `mention_timer` again for the end of the wait                                                                                                                                                                                                                    | `FlushDelivers`                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
| `ReadyNeedsConnected`     | `ms_until_a_client_is_ready` counts only a client in state `connected` with `handshake_complete` and `connected_at`                                                                                                                                                                                           | `SentWhenReady`                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
| `ReadyFromHandshake`      | `ms_until_a_client_is_ready` measures from `info.connected_at`, which only the 101 write callback sets, to the handshake time, and `get_client_info` returns                                                                                                                                                  | `SentWhenReady`                                                                                                                                                                                                                                                                                                                                                                                                                                                             |
| `FlushSendsHead`          | `flush_mention_queue` broadcasts `queue[1]` and removes index 1                                                                                                                                                                                                                                               | `SentInOrder`                                                                                                                                                                                                                                                                                                                                                                                                                                                               |
| `FlushChecksDelivery`     | `flush_mention_queue` returns and keeps the head when `server.broadcast` returned false. `server/init.lua` returns whether `broadcast` in `server/tcp.lua` sent to a client, and that counts only clients in state `connected`                                                                                | `NoSilentDrop`                                                                                                                                                                                                                                                                                                                                                                                                                                                              |
| `FlushRemovesHead`        | `flush_mention_queue` removes the head after the broadcast, then calls `schedule_mention_flush(inter_message_delay)`                                                                                                                                                                                          | `AtMostOnce`                                                                                                                                                                                                                                                                                                                                                                                                                                                                |
| `FailedWriteReported`     | the flush passes `report_unwritten("queue", ...)`, and the immediate send of `_broadcast_at_mention` passes `report_unwritten("command", ...)`, which logs an error when no write succeeded. `broadcast` in `server/tcp.lua` counts the writes that succeeded and calls `on_written` once, after the last one | `NoSilentDrop`                                                                                                                                                                                                                                                                                                                                                                                                                                                              |
| `RefusedWriteReported`    | `send_message` passes the error of a write that libuv refuses at once to the callback: `write` returns nil and that error                                                                                                                                                                                     | `NoSilentDrop`                                                                                                                                                                                                                                                                                                                                                                                                                                                              |
| `StopClearsQueue`         | `M.stop` calls `M.state.server.stop()`, sets `M.state.server = nil`, then calls `clear_mention_queue()`, which empties the queue and stops both timers                                                                                                                                                        | `NothingAfterStop`                                                                                                                                                                                                                                                                                                                                                                                                                                                          |
| `ImmediateWaitsForReady`  | with `disable_broadcast_debouncing` set and an empty queue, `_broadcast_at_mention` broadcasts at once only while `ms_until_a_client_is_ready()` is 0 or nil, and otherwise calls `queue_mention`                                                                                                             | `SentWhenReady`                                                                                                                                                                                                                                                                                                                                                                                                                                                             |

On `BROKEN`, the script prints the TLC trace as action names. Each action in `model/MentionQueue.tla` names the Lua function it models. The two client slots are `1` and `2`. Read the trace with the pstack `/statechart` skill:

1. Rerun with `--keep`.
2. Copy the broken run's `.cfg` from the kept dir. Set `Mentions = 1`, `MaxConnects = 1` and `MaxStarts = 0`, then add a mention only if the path needs two (an order break), a connection only if it needs a second client, and a start only if it needs a restart. For a liveness rule, keep the `PROPERTY` line. Stop at the smallest config that still breaks the rule.
3. Give `/statechart` the kept `MentionQueue.tla`, that cfg, and the view `model/statechart-view.ts`. `/statechart` charts invariants. For a liveness rule, read the kept `live-<rule>.out` trace instead: it ends in `Stuttering` or `Back to state`, the point after which nothing more happens to the mention.

The report tells the path in plain words, for example "you send a mention, Claude opens its socket, Claude asks for the WebSocket, the handshake completes, the handshake schedules a flush, Claude's socket goes away, the flush finds no client, a second Claude completes its handshake: the deadline never runs". Then decide which kind of failure it is:

- **Real bug.** The path is one the code can take. A fact went `FALSE` because the change removed or moved a guard. Replay it on the real code before you report it: copy the closest script in `replays/` and drive the real functions in the path's order. Report it in the code's words. Never weaken a rule or the model to make it pass.
- **Modeling error.** The facts are `TRUE` but the path needs a step the code cannot take, or a fact reads `FALSE` because the guard was reworded and still works (for example `if info.handshake_complete == true and info.state == "connected" then` reads `FALSE` for `ReadyNeedsConnected`). Fix the regex or the model, run `--mutants`, and say what you changed.

## Bugs this model found

The first model of this queue, on the code before #454, broke five of its six rules. Each finding below was replayed on real Neovim, and each is fixed. Its replay under `replays/` now shows the promise kept on the code at the commit in `covered.lock`.

1. `NoSilentDrop`, expired at the flush (#454 finding A, `replays/expired-at-flush.lua`). You sent while Claude was not connected, and Claude completed its handshake more than about 4.4 s later. The flush then dropped the mention as older than `queue_timeout` (5 s), with no error. Fixed in #454: a mention stays queued until a client took it or its wait ended with an error. #480 set the end of that wait to the deadline, which gives a Claude that completes its handshake within `connection_timeout` its `connection_wait_delay`. The untimed model does not see the deadline length. The `A:` tests in `tests/unit/mention_queue_spec.lua` pin it.
2. `NoSilentDrop`, lost in the wait (#454 finding H, `lost-in-wait.lua`, `lost-in-wait-reconnect.lua`). Claude dropped during the 600 ms wait after its handshake, and the plugin sent the mention to no client and logged success. Fixed in #454. Checked by `FlushChecksDelivery`.
3. `SentInOrder` (#454 finding E, `order.lua`). A send during the wait took the 50 ms debounce path and overtook the mention queued before it. Fixed in #454: one queue, and the flush sends its head. Checked by `FlushSendsHead`.
4. `NothingAfterStop` (#454 finding C, `stop-in-wait.lua`, `restart-leak.lua`). `:ClaudeCodeStop` during the wait raised `attempt to index field 'server' (a nil value)`, and a stop and a start sent the old mention to the new Claude. Fixed in #454. Checked by `StopClearsQueue`.
5. `NoStrandedMention`, the timer never reset (#454 finding B, `timer-never-reset.lua`). `M.state.connection_timer` stayed set after it fired, so a later mention never timed out. Fixed in #454. Checked by `EnqueueArmsDeadline` and `DeadlineRearms`.
6. `NoStrandedMention`, the connected path had no timer (#454 finding S, `drop-in-debounce.lua`). A send while Claude was connected started no timeout, so a drop within the 50 ms debounce left the mention with nothing that sent or dropped it. Fixed in #454. Checked by `EnqueueArmsDeadline`.
7. `NoStrandedMention`, a closing client counted as connected (#454 finding F, `closing-client.lua`). A send in the tick after Claude's CLOSE frame took the connected path and was stranded too. Fixed in #454: `is_claude_connected` needs state `connected`. With a deadline on every mention, a closing client that counts can no longer strand one, so no fact reads this guard. The replay and the `F:` test pin it.
8. `FlushDelivers`, the handshake window (#454 finding D, `handshake-window.lua`). The flush hook ran at the TCP accept, before the WebSocket handshake. A send in between waited for the timeout while Claude was connected. Fixed in #454 with `on_open`. Checked by `HandshakeFlushes`.
9. The path of a queued mention (#454 finding G). A queued mention kept the raw path you gave, while a connected send went through `_format_path_for_at_mention`. The model has no paths. Fixed in #454. The `G:` tests pin it.

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:

10. A second client's handshakes postponed a flush that was due for a connected Claude (Codex, round 6 on #454). The readiness rule from `connected_at` fixed it. An untimed model cannot see a flush that comes later, so the test `D: handshakes of other clients do not postpone a flush that is due for a connected Claude` pins it.
11. `NoSilentDrop`, a refused write. A write that libuv refused at once never ran its callback, so the broadcast never reported, and the queue dropped the mention with no error. Checked by `RefusedWriteReported`.
12. `NoStrandedMention`, client churn (`churn.lua`). Clients that connected and left without overlap stopped the connection timeout at each handshake, and the mention waited with no error. The deadline per mention fixed it. The model catches a revert of that fix only together with `FlushExpiresOverdue` (see the facts table). The `S:` churn tests and `A, F4: …` in `tests/unit/mention_queue_spec.lua` catch it alone. `churn.lua` does not: each flush that finds no ready client starts the deadline again, so the mention still leaves on time. It catches the code before the deadline per mention (`08dbcae`, `d1a6724`), where no flush did that.
13. `ReadyDelivers`, a drain cut at the deadline (`drain.lua`). On a head of #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 an 8.6 s wait before Claude connects, 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. Now no deadline clears a mention while a ready client is connected. Checked by `DeadlineSparesReady`.
14. `NoStrandedMention`, a spared queue with no flush due. This model found it in #480's drain rule before that reached a pushed head. Neovim runs the handshake's `on_open` callback late when its loop was busy, so 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. Checked by `SparedQueueFlushes`, and pinned by the test `F1: a ready Claude that leaves before its handshake callback ran does not strand the queue`.

## Replays

```bash
NVIM=nvim .agents/skills/verify-mention-queue/replays/run.sh                     # every replay, about 2 min
NVIM=nvim .agents/skills/verify-mention-queue/replays/run.sh order stop-in-wait  # some of them
```

`run.sh` runs each replay in a fresh headless Neovim (`-u NONE -i NONE`, this checkout first on `runtimepath`) with its own `XDG_*_HOME`, `CLAUDE_CONFIG_DIR` and cwd under `OUT` (default: a new `mktemp -d` dir, printed first). `perl` ends a replay that runs past 120 s, so `run.sh` needs no GNU `timeout`. Each replay runs through `:luafile`, not `nvim -l`, so Neovim 0.8 runs them too. It prints one verdict line per replay (`KEPT <rule>: ...` or `BROKEN <rule>: ...`) and a count line, exits 1 when a replay is `BROKEN`, counts a replay as `KEPT` only when it printed `KEPT` and its Neovim exited 0, and writes each replay's timeline, with what the user sees and any Lua error, to `$OUT/<name>.log`. `replays/lib.lua` plays Claude with real loopback WebSocket clients in the same Neovim. It reads the auth token from plugin state and never prints it. Each replay drives the real functions in the order of its model path, and `vim.wait` pumps the real event loop between steps, so the plugin's own timers and `vim.schedule` callbacks run with the default delays. `closing-client.lua` feeds Claude's CLOSE frame through the real `server/client.lua` `process_data` with the `on_close` that `server/tcp.lua` passes, so that the send lands in the same tick. Six replays wait for a deadline or a long drain, so they take 11 to 22 s each.

## Update after an intended change

1. Read every `was:`/`now:` line of the STALE output and the code behind it.
   - If only `file` lines changed, and the change cannot reach the queue, its timers, the connection or readiness check, the handshake, a broadcast or a stop (for example a diff or terminal change in `init.lua`), say so in the PR. Then skip to step 4.
2. If the behavior changed, change the action in `model/MentionQueue.tla` that cites that code. If a guard moved, change its fact regex in `check.sh`. If a new caller queues, flushes or clears mentions, model it as an action or add a fact for its guard.
3. Run `check.sh --mutants`. Every fact must be caught by its rule, and every rule must break at least once.
4. Run `check.sh` and read the result. Run `replays/run.sh` when the change can reach a replay's path.
5. Run `check.sh --record` only once you have confirmed that the model describes the code at this commit. Commit `covered.lock` with the change.

## Scope and bounds

- The invariants run with 3 mentions, 2 client slots, 2 TCP connects and 1 restart, about 540,000 distinct states. The liveness rules run with 2 mentions: about 116,000 states for `NoStrandedMention` and `ReadyDelivers`, and about 48,000 for `FlushDelivers`. Each run checks both values of `disable_broadcast_debouncing`, which doubles each count.
- Two client slots, so two clients can be connected at once. A broadcast reaches both, and the readiness rule counts both. A third client is not modeled: a bug that needs three clients at once, such as a third client's handshake that postpones a flush, is not caught here. The test `D: handshakes of other clients do not postpone a flush that is due for a connected Claude` connects 11 clients.
- Time is untimed. "`connection_wait_delay` has passed since the accept" and "since the handshake" are steps of each client, and any deadline can pass at any step. So the model does not check the deadline length or a flush that comes late. `tests/unit/mention_queue_spec.lua` checks both, with a fake clock, and the replays check them with real timers.
- A broadcast's writes all succeed, all fail later, or are all refused at once. When one client's write succeeds and another's fails, the code counts a success, and the model does not explore that mix.
- The model covers `disable_broadcast_debouncing` on and off: each run starts with either value and keeps it. With it on, a send while Claude is connected and the queue is empty goes out at once while some connected client is ready, and otherwise waits in the queue like any send (`ImmediateWaitsForReady`). Before that check, the immediate send skipped the readiness wait: on real Neovim 0.8.0 and 0.12.3, a send right after the handshake reached Claude a few ms after it (3 to 10 in our runs), where the queue waits the full 600 ms. The model sends through `send_at_mention`, which takes the immediate path only while Claude counts as connected. `_add_paths_to_claude` calls `_broadcast_at_mention` without that check: with it on and no client connected, its send shows "Failed to broadcast …" at once. That error at once breaks no rule, and the model leaves it out. Under busted, `_broadcast_at_mention` broadcasts at once unless a test sets `enable_broadcast_debouncing_in_tests`.
- `start_timer` runs a callback only while its timer is still the one in `M.state`. The model takes that as given: a stop cancels the callbacks that wait for the main loop. If that check broke, a callback whose timer fired, and was then stopped or replaced before the main loop ran the callback, would still run once: it would stop the newer timer and run its flush or deadline check early. Both read the queue, the clients and the deadlines again when they run, so the user would see at most a mention that goes out before its 50 ms debounce or 25 ms gap ends. A verifier removed the check: the unit tests in `tests/unit/mention_queue_spec.lua`, `tests/unit/server_spec.lua` and `tests/unit/server/connection_lifecycle_spec.lua`, and the `stop-in-wait`, `restart-leak`, `lost-in-wait-reconnect` and `drain` replays, still passed. It found no harm.
- The model has no paths. A path that `_format_path_for_at_mention` refuses returns an error at once and is not queued.
- `VimLeavePre` is modeled as a stop. Neovim exits after it, so the steps after it in a path do not run.
- `ClaudeCodeSendComplete`, the terminal, logging other than the queue errors, selection tracking and ping timers are not modeled. `ClaudeCodeSendComplete` fires only for a send made while Claude counts as connected, when the plugin accepts the send and not when Claude gets it. A send made while Claude is not connected never fires it, also when the queue delivers it later. A bug in the others shows outside the queue: the terminal does not open or take focus, a selection reaches Claude wrong, or a ping timer drops a Claude that still works, which the model sees as one more drop.
- A pass covers this model at these bounds, for the facts `check.sh` reads, on the covered files exactly as recorded in `covered.lock`. Any other tree reads STALE.