Verify Terminal Lifecycle

---
name: verify-terminal-lifecycle
description: Model-check the claudecode.nvim Claude terminal lifecycle (TLA+/TLC) against guards read from the current Lua code - the native and snacks providers, the code that finds a Claude after a plugin reload, and the provider choice (lua/claudecode/terminal.lua, terminal/native.lua, terminal/snacks.lua, terminal/owned.lua, and the terminal commands and send_at_mention in init.lua). Use after a change to how the Claude terminal is started, shown, hidden, closed, adopted, or cleaned up after Claude exits, or to how terminal.lua picks a provider, and before trusting such a change.
---

# Verify the Claude terminal lifecycle

You open Claude in a Neovim terminal, hide it, show it, send it context, and close it. Claude can exit on its own. The plugin can reload while Claude runs (`:Lazy reload`). The plugin must run one Claude at a time, stop it when you close it, show a running Claude when you open it, and touch only its own window. This check explores every order of your commands, Claude's exits, the plugin's scheduled callbacks, autocmds that call the plugin during a start, and one module reload (with a possible change of provider) in a small model. Each guard is switched on or off to match the code as it is now.

## Rules

| Rule                        | Plain sentence                                                                                                     | Harm when broken                                                                                        |
| --------------------------- | ------------------------------------------------------------------------------------------------------------------ | ------------------------------------------------------------------------------------------------------- |
| `AtMostOneClaude`           | At most one Claude runs, apart from the one a close is stopping.                                                   | Two Claude sessions connect to Neovim. One of them is untracked, so no command reaches it.              |
| `CloseStopsClaude`          | When `:ClaudeCodeClose` returns, no Claude that ran when it began still runs.                                      | You close Claude and it keeps running in a buffer you cannot see.                                       |
| `CloseNeverReuses`          | The plugin never tracks again a terminal it began to close.                                                        | An open during the close's wait gets the terminal that is being deleted, and you end up with no Claude. |
| `OpenShowsLiveClaude`       | After an open, a show or a focus, you see a running Claude. A snacks terminal with `auto_close = false` is exempt. | You get `[Process exited]` or your own file instead of Claude, and a queued at-mention times out.       |
| `HideKeepsClaude`           | Hiding Claude's window keeps Claude running.                                                                       | A toggle ends the Claude session and loses the conversation.                                            |
| `HideNoError`               | Hiding Claude's window raises no error, also while a start runs.                                                   | `:ClaudeCode` prints an `E5108`/`E444` or `Invalid window id` error trace and does nothing.             |
| `FailedStartLeavesNoWindow` | A failed start leaves no window, no buffer and no tracked terminal.                                                | A broken `terminal_cmd` leaves an empty split, and the next open reuses a terminal with no job.         |
| `ExitClosesOnlyOwnWindow`   | With `auto_close`, Claude's exit closes only Claude's own window, and never the last window.                       | The plugin closes a window where you edit a file, or raises `E444` from a scheduled callback.           |

`OpenShowsLiveClaude` exempts snacks with `auto_close = false` on purpose. `lua/claudecode/terminal/README.md` documents that snacks reuses the tracked instance while `terminal:buf_valid()` is true, and registers its `TermClose` handler only with `auto_close`. So an open after Claude exited shows the exited terminal again. The native provider starts a new Claude in that case.

## Run

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

The script sources `scripts/tla/check-lib.sh`, which pins TLC 1.7.4 by sha256 and downloads it to `~/.cache/claudecode-nvim-tla/` on the first run. It needs bash 4 or newer, Java 11 or newer (`JAVA=/path/to/java` overrides `java` on PATH), `sha256sum` or `shasum`, and curl for that first download. Run one copy at a time on a shared host. TLC is CPU heavy. CI runs every `.agents/skills/verify-*/check.sh` in the `covered-lock` job on every pull request.

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.

## Does the change touch the verified code?

Run the check. `covered.lock` records a hash of each covered file: `lua/claudecode/terminal.lua`, `lua/claudecode/terminal/native.lua`, `lua/claudecode/terminal/snacks.lua`, `lua/claudecode/terminal/owned.lua` and `lua/claudecode/init.lua`. Any change to one of them reads `STALE` (exit 3) until someone confirms that the model still describes the code. `init.lua` is covered because the model's steps are its `:ClaudeCode`, `:ClaudeCodeFocus`, `:ClaudeCodeOpen` and `:ClaudeCodeClose` commands and `send_at_mention`. `terminal/external.lua` and `terminal/none.lua` are not modeled and not covered.

The record also hashes each block the model describes, and lists every non-comment line of the covered files that touches the tracked terminal (`OWNED_MARK`, `cleanup_state(`, `forget_exited_job`, `forget_ended_terminal`, `adopt_existing_terminal`, `wrap_terminal`, `upgrade_wrapper`, `remember_backdrop`, `register_window_events`, `adopted_config`, `focus_adopted`, `stop_snacks_terminal`, `stop_native_terminal`, `stop_other`, `stop_buffer`, `open_terminal(`, `close_terminal(`, `hide_terminal(`, `show_hidden_terminal(`, `cc_hide(`, `cc_show(`, an assignment to `terminal`, `termopen`, `jobstop`, `vim.wait(`, `nvim_win_close`, `get_provider()`, `load_provider(`, or a `terminal.open/close/simple_toggle/focus_toggle/ensure_visible(` call), with its enclosing top-level statement. The STALE output prints a `was:`/`now:` pair per changed file, block or line.

Covered blocks:

- In `terminal.lua`: `load_provider`, `get_provider`, `ensure_terminal_visible_no_focus`, `M.open`, `M.close`, `M.simple_toggle`, `M.focus_toggle`, `M.hide_float`.
- In `terminal/native.lua`: `is_last_window`, `is_valid`, `forget_exited_job`, `forget_ended_terminal`, `adopt_existing_terminal`, `stop_snacks_terminal`, `open_terminal`, `close_terminal`, `is_terminal_visible`, `hide_terminal`, `show_hidden_terminal`, `focus_adopted`, `M.open`, `M.simple_toggle`, `M.focus_toggle`, `M.get_active_bufnr`.
- In `terminal/snacks.lua`: `is_available`, `setup_terminal_events`, `cc_is_visible`, `cc_hide`, `cc_show`, `forget_ended_terminal`, `remember_backdrop`, `register_window_events`, `find_backdrop`, `find_window`, `wrapper_options`, `wrap_terminal`, `upgrade_wrapper`, `adopted_config`, `adopt_existing_terminal`, `stop_native_terminal`, `M.open`, `M.close`, `M.simple_toggle`, `M.focus_toggle`, `M.get_active_bufnr`, `M.hide_float`.
- In `terminal/owned.lua`: `M.job_ended`, `M.is_live`, `M.find`, `stop_buffer`, `M.stop_other`.
- In `init.lua`: the `if terminal_ok then` block that creates the terminal commands, and `M.send_at_mention`.

A PASS says 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 a guard that a regex reads from the source. `TRUE` means the regex found the guard. `FALSE` means the model runs without that guard. On a healthy tree every fact is `TRUE`. A `FALSE` is either a removed guard (a bug) or a guard reworded past the regex (a modeling error). See below for how to tell them apart.

How a provider finds the Claude it started (`owned.lua`, and the adoption in each provider):

| Fact                       | Code it reads                                                                                                                |
| -------------------------- | ---------------------------------------------------------------------------------------------------------------------------- |
| `OwnedUnstartedIsNotEnded` | `job_ended` is `return channel ~= 0 and not pcall(vim.fn.jobpid, channel)`: a buffer whose job has not started has not ended |
| `OwnedLiveNeedsMark`       | `is_live` requires `vim.b[buf][mark]`. Both providers adopt through `owned.find(OWNED_MARK)`                                 |
| `OwnedLiveSkipsEndedJob`   | `is_live` requires `not M.job_ended(buf)`                                                                                    |

The native provider:

| Fact                             | Code it reads                                                                                                                                                                                                                                                                                                                                                  |
| -------------------------------- | -------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- |
| `NativeMarkBeforeTermopen`       | `start_terminal` sets `vim.b[new_bufnr][OWNED_MARK] = true` after `nvim_create_buf` and before `nvim_win_set_buf` (which fires `BufEnter`) and `pcall(vim.fn.termopen, ...)`                                                                                                                                                                                   |
| `NativeAdoptsHiddenTerminal`     | `adopt_existing_terminal` takes `owned.find(OWNED_MARK)`, with no check that a window shows the buffer                                                                                                                                                                                                                                                         |
| `NativeShowsAdoptedHidden`       | `focus_adopted` (used by `M.open` and `M.simple_toggle`) and the `M.focus_toggle` branch call `show_hidden_terminal` for an adopted terminal that no window shows                                                                                                                                                                                              |
| `NativeExitClearsMark`           | termopen's `on_exit` schedules a function that clears `vim.b[new_bufnr][OWNED_MARK]` and calls `forget_exited_job(job_id, effective_config.auto_close)`                                                                                                                                                                                                        |
| `NativeAdoptedExitHandled`       | `adopt_existing_terminal` adds a buffer-local `TermClose` autocmd that schedules `forget_exited_job(adopted_jobid, config.auto_close)`                                                                                                                                                                                                                         |
| `NativeExitForgetsOwnJobOnly`    | `forget_exited_job` returns when `job_id ~= jobid`                                                                                                                                                                                                                                                                                                             |
| `NativeExitKeepsLastWindow`      | `forget_exited_job` closes the tracked window only `and not is_last_window(current_winid_for_job)`, and `is_last_window` counts tab pages and non-floating windows                                                                                                                                                                                             |
| `NativeExitChecksWindowBuffer`   | for a valid buffer, `forget_exited_job` closes the tracked window only `if vim.api.nvim_win_get_buf(current_winid_for_job) == current_bufnr_for_job`                                                                                                                                                                                                           |
| `NativeEntriesForgetEndedJob`    | `M.open`, `M.simple_toggle` and `M.focus_toggle` call `forget_ended_terminal()` first, which runs `forget_exited_job` for a tracked buffer whose `job_ended` is true                                                                                                                                                                                           |
| `NativeRescansSwappedWindow`     | `is_valid` scans the windows again when the tracked window shows another buffer, and clears `winid` when none shows Claude                                                                                                                                                                                                                                     |
| `NativeCloseAdopts`              | `close_terminal` runs `if not is_valid() and not adopt_existing_terminal() then`                                                                                                                                                                                                                                                                               |
| `NativeCloseForgetsFirst`        | `close_terminal` calls `cleanup_state()` before `vim.wait`                                                                                                                                                                                                                                                                                                     |
| `NativeCloseClearsMark`          | `close_terminal` sets `vim.b[closing_bufnr][OWNED_MARK] = nil` before `vim.wait`                                                                                                                                                                                                                                                                               |
| `NativeKeepsHiddenJob`           | `start_terminal` sets `vim.bo[new_bufnr].bufhidden = "hide"` after the mark and before `nvim_win_set_buf`, so a window that closes never unloads the buffer, and sets `vim.bo[bufnr].bufhidden = "hide"` again after `termopen`, which overrides an autocmd of the start that changed it                                                                       |
| `NativeHideKeepsLastWindow`      | `hide_terminal` checks `is_last_window(winid)` or calls `pcall(vim.api.nvim_win_close, winid, false)`                                                                                                                                                                                                                                                          |
| `NativeFailCleansUp`             | the `if failure then` branch of `start_terminal` closes `new_winid`, deletes `new_bufnr`, calls `cleanup_state()` and returns                                                                                                                                                                                                                                  |
| `NativeStartSurvivesClosedSplit` | after `jobid = termopen_result`, `start_terminal` reads the buffer of `new_winid` only `if vim.api.nvim_win_is_valid(new_winid) and ...`, sets `winid = new_winid` and `bufnr = new_bufnr`, calls `is_valid()` to find the window that shows Claude now, and focuses it only `if focus and winid then`                                                         |
| `NativeOpenSkipsDuringStart`     | `open_terminal` returns `if starting then`. `starting` is true from `starting = true` to `starting = false` around `pcall(start_terminal, ...)`, so an entry that an autocmd of the start calls before the buffer has a mark (the `vsplit` fires `WinLeave`, `WinNew` and `WinEnter`, creating the buffer fires `BufNew` and `BufAdd`) starts no second Claude |
| `NativeRunsDeferredClose`        | after `pcall(start_terminal, ...)`, `open_terminal` reads `close_after_start` into `close_requested`, clears it, and runs `pcall(close_terminal)` `if close_requested then`, also when the start raised. A close that an autocmd of the start called only set the flag (`M.close`), because the wait of a close cannot run inside `termopen`                   |
| `NativeStopsSnacksClaude`        | before it starts Claude, and in `close_terminal` when it finds none to adopt, native calls `stop_snacks_terminal()`, which calls `owned.stop_other(owned.SNACKS_MARK, "snacks")`                                                                                                                                                                               |

The snacks provider:

| Fact                          | Code it reads                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      |
| ----------------------------- | ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ |
| `SnacksOpenSkipsDuringStart`  | `M.open` returns `if starting then` while its own `Snacks.terminal.open` runs, because `terminal` is set only after that call returns                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              |
| `SnacksMarksStartedTerminal`  | after a started terminal, `M.open` sets `vim.b[term_instance.buf][OWNED_MARK] = true` before `terminal = term_instance`                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            |
| `SnacksEntriesAdopt`          | `adopt_existing_terminal` takes the marked buffer whose job has not ended (`owned.find(OWNED_MARK)`) when none is tracked, and wraps it with `wrap_terminal(buf, config)`. `M.open`, `M.simple_toggle` and `M.focus_toggle` call it first, with their config. It never asks `Snacks.terminal.list()`                                                                                                                                                                                                                                                                                                                                                               |
| `SnacksEntriesForgetEndedJob` | `adopt_existing_terminal`, the first call in `M.open`, `M.simple_toggle` and `M.focus_toggle` (`M.close` is read by `SnacksCloseAdopts`), runs `forget_ended_terminal()` first. `M.get_active_bufnr` calls it first too, but no fact reads that (see the diff bullet under "Scope and bounds"). With `auto_close`, that sets `terminal = nil` when `owned.job_ended(terminal.buf)` is true. It wipes nothing: a wipe inside `TermClose` would delete the autocmds that remain for that event                                                                                                                                                                       |
| `SnacksCloseAdopts`           | `M.close` calls `adopt_existing_terminal()` before it checks for a tracked terminal                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                |
| `SnacksExitForgets`           | with `config.auto_close`, the `TermClose` handler of `setup_terminal_events` calls `forget()` before it schedules `term_instance:close({ buf = true })`                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            |
| `SnacksForgetChecksInstance`  | `forget()` clears `terminal` only `if terminal == term_instance`                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   |
| `SnacksCloseForgetsFirst`     | `M.close` sets `terminal = nil` before `vim.wait`                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  |
| `SnacksCloseClearsMark`       | `M.close` sets `vim.b[closing_bufnr][OWNED_MARK] = nil` before `owned.wait_for_exec(jobid)` and `jobstop`, after `terminal = nil`. The model counts a closing terminal as ended, so this fact breaks a rule only together with `OwnedLiveSkipsEndedJob`                                                                                                                                                                                                                                                                                                                                                                                                            |
| `SnacksHideKeepsLastWindow`   | `cc_hide` closes a split with `if pcall(vim.api.nvim_win_close, win, false) then`                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  |
| `SnacksFailCleansUp`          | `M.open` captures the shown instance in `on_buf`, calls `Snacks.terminal.open` under `pcall`, and on a failed start sets `terminal = nil` and calls `leftover:close({ buf = true })`                                                                                                                                                                                                                                                                                                                                                                                                                                                                               |
| `SnacksStopsNativeClaude`     | before it starts Claude, and in `M.close` when it finds none to adopt, snacks calls `stop_native_terminal()`, which calls `owned.stop_other(owned.NATIVE_MARK, "native")`                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          |
| `OwnedStopOtherStops`         | `owned.stop_other` returns false when no marked buffer exists, then loops `buf = M.find(mark)` until none is left, and `stop_buffer` clears the mark, waits for the exec of the job's child (`owned.wait_for_exec`, not modeled), runs `jobstop` only `if vim.api.nvim_buf_is_valid(buf)` still holds after that wait (a callback can delete the buffer during it), waits up to 1 s for the exit, and deletes the buffer. The fact reads each of these calls in that order, including the validity check. Both providers call it before a start and in `close` (`NativeStopsSnacksClaude`, `SnacksStopsNativeClaude`), and the model's `StopAll` step relies on it |
| `SnacksAvailabilityCached`    | `snacks.lua` runs `local snacks_available, Snacks = pcall(require, "snacks")` once at load, `is_available` returns those values, and `terminal.lua` `load_provider` gets the module through `require`, which keeps it (its own `providers` table is a second cache that the fact does not need), and `get_provider` uses it for `"auto"`                                                                                                                                                                                                                                                                                                                           |

On `BROKEN`, the script prints the TLC trace as action names. Read it with the pstack `/statechart` skill:

1. Rerun with `--keep`.
2. Copy `main.cfg` from the kept dir. Set `Terms = {t1}` and one provider in `Providers`, and set every environment switch (`Reloads`, `ProviderChanges`, `AutocmdReenters`, `OpenBeforeCleanup`, `Swaps`, `Wipes`, `OnlyWindow`) to `FALSE`. Then turn on one switch at a time, and add `t2` only if the path needs a second Claude. Stop at the smallest config that still breaks the rule. Delete the kept dir when you are done.
3. Give `/statechart` the kept `TerminalLifecycle.tla`, that cfg, and the view `model/statechart-view.ts`.

The report tells the path in plain words, for example "you open Claude, termopen starts it, the start returns, the plugin reloads, you open Claude, Claude exits, you open Claude". That is bug 8 below.

Then decide which kind of failure it is:

- **Real bug.** A fact went `FALSE` because the change removed or moved a guard, or a rule broke with every fact `TRUE`, and the code can take the path. Replay the path on real Neovim before you report it (see Replays). 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. Fix the regex or the model, run `--mutants`, and say what you changed.

## Bugs this model found

The first version of this model broke five rules on seven paths. Replaying the paths on real Neovim 0.12.3 (Claude played by `sh -c 'sleep ...'`) confirmed them. An update of the model after the fixes found an eighth. A review comment on this skill found a ninth, and the model now has its step. A probe of the autocmds of a start on real Neovim found a tenth, and the model has its step too (`SplitRuns`). Each fix landed before this skill did, so the check passes on the code as merged.

| #   | Rule                      | Bug                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   | Fixed in |
| --- | ------------------------- | ----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | -------- |
| 1   | `AtMostOneClaude`         | An autocmd that calls open while snacks starts Claude (`BufEnter`, `TermOpen`) started a second Claude, because snacks set `terminal` only after `Snacks.terminal.open` returned.                                                                                                                                                                                                                                                                                                                     | #451     |
| 2   | `AtMostOneClaude`         | After a plugin reload, the next open started a second Claude: native adopted only a terminal that a window showed, snacks adopted nothing, and `auto` could pick snacks after a reload when snacks became loadable.                                                                                                                                                                                                                                                                                   | #464     |
| 3   | `CloseStopsClaude`        | `:ClaudeCodeClose` after a reload left Claude running, because `close_terminal` never tried to adopt.                                                                                                                                                                                                                                                                                                                                                                                                 | #464     |
| 4   | `OpenShowsLiveClaude`     | An open between Claude's exit and the scheduled exit cleanup (native) focused the dead terminal and started no Claude.                                                                                                                                                                                                                                                                                                                                                                                | #451     |
| 5   | `OpenShowsLiveClaude`     | After `:e file` in Claude's window (native), `:ClaudeCodeOpen` focused your file and `ensure_visible` did nothing, so Claude stayed hidden.                                                                                                                                                                                                                                                                                                                                                           | #451     |
| 6   | `HideNoError`             | The native toggle raised `E444` when Claude's window was the only window.                                                                                                                                                                                                                                                                                                                                                                                                                             | #451     |
| 7   | `ExitClosesOnlyOwnWindow` | After a wipe, the native exit cleanup closed the window that showed your file instead of Claude.                                                                                                                                                                                                                                                                                                                                                                                                      | #451     |
| 8   | `OpenShowsLiveClaude`     | The provider forgot an exited snacks Claude only in its `TermClose` handler, and found its Claude after a reload through `Snacks.terminal.list()`. An entry that ran before the scheduled close (a `TermClose` autocmd, or any entry after a reload) showed the dead terminal, and the close then wiped it. A Claude that started in that gap got the dead one's Snacks key (command, directory, env, count), and the late wipe dropped it from the list, so the next reload started a second Claude. | #482     |
| 9   | `HideNoError`             | A `BufEnter` or `TermOpen` autocmd that called `focus_toggle` while native started Claude adopted the half-started terminal and hid its window, and the start then raised `Invalid window id` at `native.lua:263`. Claude ran with no window (#527). Codex found it in review of this skill, and the model has the step (`AutocmdCalls`) since.                                                                                                                                                       |
| 10  | `AtMostOneClaude`         | A `WinLeave`, `WinNew` or `WinEnter` autocmd of native's `vsplit`, or a `BufNew` or `BufAdd` autocmd of its new buffer, that called `open`, `simple_toggle` or `focus_toggle` before the buffer had a mark found no terminal to adopt and started a second Claude. The first start then recorded its own terminal, and a close returned with one still running. The model has the phase (`begin`) and the step (`SplitRuns`) since.                                                                   | #544     |

## Replays

Each replay drives the real plugin in a headless Neovim, prints one line per step, marks the lines that show a finding with `BUG`, and ends with a count line. On the current code every replay shows no finding. A `BUG` line means the finding is back.

```bash
NVIM=<path to nvim> .agents/skills/verify-terminal-lifecycle/replays/run.sh <replay>.lua
SNACKS_NVIM=<snacks.nvim checkout> NVIM=<path to nvim> .agents/skills/verify-terminal-lifecycle/replays/run.sh snacks-<replay>.lua
```

`run.sh` gives Neovim throwaway XDG dirs and `CLAUDE_CONFIG_DIR`, and never runs the claude CLI. It exits `0` when no check shows its finding, `1` when one does, and `2` on a setup error. The snacks replays (`snacks-*.lua`, `auto-snacks-later.lua`) need a snacks.nvim checkout. They ran on snacks.nvim 882c996c, the commit `fixtures/snacks-picker/lazy-lock.json` pins.

| Bug | Replay                                                                            | Switch it needs                       |
| --- | --------------------------------------------------------------------------------- | ------------------------------------- |
| 1   | `snacks-reentrant-open.lua`                                                       | `AutocmdReenters` (snacks)            |
| 2   | `native-reload-hidden.lua`, `snacks-reload.lua`, `auto-snacks-later.lua`          | `Reloads`, `ProviderChanges` (`auto`) |
| 3   | `native-reload-close.lua`                                                         | `Reloads`                             |
| 4   | `native-open-after-exit.lua`                                                      | `OpenBeforeCleanup` (native)          |
| 5   | `native-open-after-swap.lua`                                                      | `Swaps` (native)                      |
| 6   | `native-hide-only-window.lua`                                                     | `OnlyWindow` (native)                 |
| 7   | `native-wipe-closes-your-window.lua`                                              | `Swaps` and `Wipes` (native)          |
| 8   | `snacks-reload-exit.lua`, `snacks-exit-handlers.lua`, `snacks-reload-adopted.lua` | `Reloads` and `OpenBeforeCleanup`     |
| 9   | `native-start-autocmd-hide.lua`                                                   | `AutocmdReenters` (native)            |
| 10  | `native-start-reentry.lua`                                                        | `AutocmdReenters` (native)            |

The model has no keys, tabs, backdrops or window sizes. Eight replays guard the wrapper of an adopted snacks Claude (bug 8's fix, #482): `snacks-reload-adopted.lua` above, and seven more that guard what the wrapper must keep from the instance that the provider started itself. Verification of the first drafts of #482 found each defect in those seven, and the fix landed before #482 did, so they are no model findings:

| Replay                       | Promise                                                                                                                                                                                                                                              |
| ---------------------------- | ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- |
| `snacks-reload-keys.lua`     | After a reload, a hide and a show, `q` hides Claude, `gf` hides it and leaves the file out of its window, and a function key of the user's (`self:hide()`) hides a float that was closed and opened. The wrapper maps its own keys.                  |
| `snacks-reload-tabs.lua`     | After a reload, a copy of the terminal in another tab (a diff tab) is no terminal window: a hide in the first tab and an open put Claude back in the first tab, and a toggle in the other tab hides the tracked window, not the copy.                |
| `snacks-reload-backdrop.lua` | After a reload, a float that Snacks re-created has its new backdrop hidden with it, because the provider writes the backdrop's window id each time.                                                                                                  |
| `snacks-reload-older.lua`    | After a reload, a float of an older version (no buffer variables) comes back with the configured size once an entry with a config ran, whichever entry adopted it first.                                                                             |
| `snacks-reload-edit.lua`     | After a reload, a hide and a show of a split, `:edit` in Claude's window moves the file to another window and keeps Claude, because the wrapper registers the Snacks events and the `BufWinEnter` handler at its first re-creation of a split.       |
| `snacks-reload-anchor.lua`   | After a reload, a float that is `relative = "win"` comes back anchored to its window, not to the window that was current at the adoption.                                                                                                            |
| `snacks-reload-focus.lua`    | After a reload, a hide and a show of a split, a hide of Claude leaves the cursor where Neovim puts it (the neighbor window), not in the previous window, because the wrapper registers no `WinClosed` event, which is bound to the id of one window. |

## 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 terminal's start, show, hide, close, exit handling, adoption or provider choice (for example a diff or selection change in `init.lua`), say so in the PR. Then skip to step 4.
2. If the behavior changed, change the step in `model/TerminalLifecycle.tla` that cites that code. If a guard moved, change its fact regex in `check.sh`. If the change adds a guard, add a fact, an `EXPECT` entry for the rule that must break without it, and a mutant branch in `tla_constants`.
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. If a rule breaks, replay the path (see Replays) and fix the code before you record.
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 main run uses two terminals (`Terms = {t1, t2}`), the providers `"native"` and `"auto"` (`"snacks"` resolves the same way in `get_provider`, plus a warning when it falls back), snacks.nvim loadable or not at setup, and `auto_close` true or false. Your `'hidden'` option is chosen only when the code does not set `bufhidden=hide`, because it changes nothing otherwise. Every environment switch is on: one reload that can also change the provider, one autocmd open per start, opens while callbacks are queued, `:e` in Claude's window, `:bwipeout!` of Claude's buffer, and `:only`. TLC stops exploring past a broken rule (`CONSTRAINT AllRulesHold`), which is enough because it stops at the first one anyway. With no rule broken the run explores 279,492 distinct states.
- A mutant run keeps only its guard's provider and the switches the guard needs (`tla_constants` in `check.sh`), so another switch cannot break the mutant's rule first. Each fact has an `EXPECT` entry. A guard that another guard covers for is removed together with it, as a pair. `OwnedLiveNeedsMark` and `NativeExitClearsMark`, `NativeCloseClearsMark` or `SnacksCloseClearsMark` pair with `OwnedLiveSkipsEndedJob`, because the job check alone also rejects the terminal. `NativeAdoptedExitHandled` pairs with `NativeEntriesForgetEndedJob`, and `SnacksExitForgets` with `SnacksEntriesForgetEndedJob`, because an entry runs the exit cleanup itself. `NativeExitForgetsOwnJobOnly` pairs with `NativeCloseAdopts`, and `SnacksForgetChecksInstance` with `SnacksCloseAdopts`, because a close adopts a Claude that a stray cleanup left untracked. `SnacksAvailabilityCached` pairs with `SnacksStopsNativeClaude`, because a snacks start stops the native Claude that a provider switch would leave running. `NativeMarkBeforeTermopen` and `OwnedUnstartedIsNotEnded` pair with `NativeOpenSkipsDuringStart`, because the guard of `open_terminal` also keeps an autocmd's entry from starting a second Claude while the start has no tracked terminal yet.
- One step is one run of Neovim's main loop. `vim.wait` in a close lets job exits, scheduled callbacks and a scheduled open run, and typed commands not. Neovim fires `TermClose` while it handles the exit and queues `on_exit` after it, so a callback that a `TermClose` autocmd schedules runs before the one `on_exit` schedules (`native-open-after-exit.lua` relies on this and shows it).
- A diff that opens in a float's tab hides a visible float through `terminal.hide_float(tab)` (#447, and #504 for the tab check). `M.hide_float` of `snacks` runs `cc_hide` on the tracked terminal, which is the model's hide step, so `HideKeepsClaude` and `HideNoError` cover it through the same guards. It adopts nothing itself: `diff.lua` calls `get_active_terminal_bufnr` first, which adopts after a reload. No fact reads that adoption: `M.get_active_bufnr` of both providers is hashed (`native_active`, `snacks_active`), so a change reads STALE, and the model has no step for it, because none of the eight rules depends on which entry adopts first. If a change drops it, a Snacks float stays over a diff after a reload, and callers see no active Claude. A hide through it keeps the job, and nothing shows the float again but the user's toggle.
- Snacks keys an instance by its command, directory, env and count, and clears the key when a buffer is wiped, whichever instance holds it, so `Snacks.terminal.list()` can lose a running Claude. The code finds its Claude by the mark and a live job instead, so the model needs no key. `snacks-reload-exit.lua` replays the path (both orders of a `TermClose` autocmd and the provider's handler), and `snacks-exit-handlers.lua` replays the two ways that wiping early goes wrong (a wipe inside `TermClose` deletes the autocmds that remain for that event; an exit before the first entry after a reload).
- A snacks start writes up to four buffer variables: the mark `b:claudecode_snacks_terminal`, `b:claudecode_snacks_auto_close`, `b:claudecode_snacks_window` (the resolved window options as plain data) and, for a float with a backdrop, `b:claudecode_snacks_backdrop` (the backdrop's window id). An adoption wraps the buffer in a new Snacks window built from them (`Snacks.win` with `buf`, in the `terminal` style), maps the wrapper's own keys over those of the first start (the entry's config gives the user's keys, functions included), and tracks the window of the current tab that shows the buffer, as the instance that the provider started tracks the window that it showed. The provider writes the backdrop variable again each time Snacks re-creates a float. The model sees the mark (a terminal is live when it carries it). The other variables, the keys and the window tracking decide what an adopted terminal looks and acts like, which no rule checks, and the replays `snacks-reload-adopted.lua`, `snacks-reload-keys.lua`, `snacks-reload-tabs.lua`, `snacks-reload-backdrop.lua` and `snacks-reload-older.lua` replay them. A terminal that an older version started has no variable, so the entry's config decides, and an entry without a config (`get_active_bufnr`, `close`) wraps it first and maps no key, and the first entry that brings a config maps the keys (`upgrade_wrapper`).
- The model keeps scheduled callbacks as a set, not in order. A path that needs a particular order of two plugin callbacks must be replayed before you trust it.
- `focus_toggle` is modeled as hide or focus when Claude is visible, because the model has no keyboard focus. It covers `simple_toggle`. `ensure_visible` is modeled as an open.
- Windows are modeled only as far as the rules need: whether Claude's window is open, whether it is the last window, and whether native's tracked window shows another buffer. Snacks windows are splits. Snacks floats (config-hidden on hide), tab pages, and window sizes are not modeled. Snacks' `fixbuf` is assumed, so `:e` in a snacks window is not a step.
- After the reload, the old module copy's window is tracked only while it still shows its terminal. The old copy's view of a window that you switched to another buffer is not modeled. A terminal adopted after the reload keeps the module copy that started it (`old`). Native adds a handler on adoption (`NativeAdoptedExitHandled`) that reaches the new copy's state. Snacks adds none: its entries forget an exited terminal instead (`SnacksEntriesForgetEndedJob`).
- These are not modeled. Each line says what you would see if it broke, as far as the checks that exist tell:
  - The `external`, `none` and custom table providers: Claude opens in the wrong external command, an integrated terminal opens when none should, or your own functions are called wrongly. `terminal/external_spec.lua`, `none_provider_spec.lua` and `terminal_spec.lua` test them.
  - A close that starts during another close's wait: a reentrant close targets the wrong job or returns early. No failure is known.
  - A start-time autocmd beyond one open or toggle and one close request per start (the model runs one of each per start): a `BufEnter` or `TermOpen` autocmd that calls `focus_toggle` hides the new split, a second `simple_toggle` does the same, and a `:close` of the split closes it. The model reaches the same state through its hide step. Before #527 the start then raised `Invalid window id` at `native.lua:263` and Claude ran with no window. `native-start-autocmd-hide.lua` runs all three forms, and a hide followed by a show in another window, on real Neovim (the model has no window ids).
  - A close right after a start, before the child of the job has run `exec` (`close_terminal` and `snacks.lua` `M.close` wait up to 1 s for it before `jobstop`, for a job younger than 10 s (`M.close` clears the mark before that wait, so that an `open()` among the scheduled callbacks does not adopt the terminal that is closing), and `owned.lua` `stop_buffer` waits for every job: all three call `owned.wait_for_exec`): without the wait, a loaded machine ended Neovim with `SIGHUP` or hung it in about 0.5 to 5 runs in 100 (rising with the load), in a close from an autocmd of the start and in an `open` followed by a `close`. The names come from `/proc/<pid>/comm`, or from `nvim_get_proc` (which runs `ps`) where `/proc` is missing, and a close goes on to `jobstop` when neither can be read. The model has no processes, so it cannot fail on the wait itself. Two facts read the calls around it: `OwnedStopOtherStops` reads `M.wait_for_exec(channel)` in `stop_buffer`, and `SnacksCloseClearsMark` reads the mark clear before the wait in `M.close`. No fact reads the calls in `close_terminal` and `M.close`. A change to the wait reads as a changed `close_terminal`, `snacks_close` or `owned_stop_buffer` block (STALE). `native_terminal_toggle_spec.lua`, `terminal/snacks_close_spec.lua` and `terminal/owned_wait_for_exec_spec.lua` test the order, the limit, the young-job rule, the exited job and the missing `ps`, `integration/terminal_close_young_job_spec.lua` closes each provider's job while a shim holds its child before exec, and the replay `native-start-reentry.lua` runs the close orders and the missing `ps` on real Neovim.
  - The deferral of a close during a start (`M.close` sets `close_after_start` while `starting`): without it the close waits inside `termopen`. A `BufEnter` autocmd that calls `close()` then cancels the start with "Failed to open native terminal", and a `TermOpen` autocmd that calls it aborts Neovim on the 0.8-era build (`corrupted double-linked list`, exit 139). The model has no wait nested in a start, so it reads only the second half, that the start runs the request when it returns (`NativeRunsDeferredClose`). `native_terminal_toggle_spec.lua` and the two `close()` checks of `native-start-reentry.lua` test the first half. A start whose `termopen` failed drops the request in the model, because it has no Claude to stop.
  - Which window the plugin made. The model's Claude window is any window that shows the terminal buffer. It does not say that the plugin made it. When native recovers a window of yours that shows the terminal (a `:sbuffer` of yours, found by `is_valid`), an exit with `auto_close` closes that window, and `ExitClosesOnlyOwnWindow` cannot tell. `AGENTS.md` (Code Shape) asks a cleanup to close only a window that the plugin can show it made. The model does not check that the code keeps to it.
  - A cleanup that raises. The facts read the order of the calls in the code, not that every call completes. `NativeFailCleansUp` reads `nvim_win_close(new_winid, true)`, the buffer delete and `cleanup_state()` in order, and the model takes the clean branch. When an autocmd has closed every other window, that close raises `E444`, and the buffer and the tracked state stay behind. The exit cleanup and the hide have the same limit.
  - A `TermClose` autocmd of your own that closes or deletes the terminal: the cleanup finds a deleted buffer or job. `native_terminal_toggle_spec.lua` and `snacks-exit-handlers.lua` test the orders.
  - `send_to_terminal`: text goes to the wrong job, is lost, or is sent wrongly. `send_text_spec.lua` tests it.
  - `paste_fix`: a streamed paste is duplicated, split or joined wrongly. `paste_fix_spec.lua` tests it.
  - The `<C-z>` mapping (`utils.map_terminal_suspend`): `<C-z>` reaches Claude instead of suspending Neovim, or overwrites your own key. `utils_spec.lua` tests it.
  - A second reload: adoption starts duplicate jobs, leaves old callbacks, or uses stale wrappers. The reload tests include repeated reloads.
  - The Neovim hang that the 1 s wait in close works around (neovim/neovim#42508): Neovim hangs when a close deletes a buffer whose write has not drained. The code documents the limit, and no test covers a job that stopped reading.
  - `:bdelete`: deleting the terminal buffer ends or hides Claude, and a later entry starts or adopts one. The model's wipe step is the nearest case.
  - `:q` in Claude's window: the window closes and Claude keeps or loses its job, depending on `bufhidden` and the last-window rule. The hide tests cover the exercised cases.
  - Neovim exit: cleanup hangs or leaves a process. The replays stop their jobs themselves.
- 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 content of those files reads STALE.