diff --git a/.agents/skills/verify-native-lifecycle/SKILL.md b/.agents/skills/verify-native-lifecycle/SKILL.md
new file mode 100644
index 0000000..33f47ac
--- /dev/null
+++ b/.agents/skills/verify-native-lifecycle/SKILL.md
@@ -0,0 +1,106 @@
+---
+name: verify-native-lifecycle
+description: "Model-check, with TLA+, how the libghostty-vt-node native addon keeps state across Node environments (the main thread and worker_threads Workers) and across one terminal's life (createTerminal, use, dispose, garbage collection). Use when a change touches TerminalWrap or InitAll in native/, the Terminal class or createTerminal in src/index.ts, loadNative in src/loader.ts, or the node-addon-api version, or when someone adds or tests worker-thread support."
+---
+
+# Verify the native addon lifecycle
+
+This skill checks a TLA+ model of the addon's native state against four rules. A model checker (TLC) tries every order of steps in the model, within the bounds below. Tests only try the orders that someone wrote.
+
+## The rules
+
+| Rule | In plain words | Harm when it breaks |
+|---|---|---|
+| `CreateUsesOwnClass` | `createTerminal` in a thread uses the class reference that this thread made. | The process aborts or segfaults when it creates a terminal. |
+| `LoadDeletesOnlyOwnRef` | Loading the addon in a thread never deletes another thread's reference. | One thread frees V8 state that belongs to another thread (a data race). |
+| `HandleFreedOnce` | libghostty frees each terminal handle at most once. | A double free corrupts the heap. |
+| `NoCallOnDeadHandle` | No libghostty call reaches a freed or null terminal handle. | Use after free: a crash or wrong terminal output. |
+
+## History: finding F1, fixed
+
+This check found F1 in the code before `4aa7039`. The addon kept its class in one `static Napi::FunctionReference constructor` for the whole process, and each environment's `TerminalWrap::Init` overwrote it. After the main thread and a Worker both loaded the addon, the main thread's `createTerminal` used the worker's reference: V8 aborted with `Cannot create a handle without a HandleScope`, or the process segfaulted after the worker exited. The fix keeps one reference for each environment in its instance data. `model/mutant-process-static.cfg` is the old code, and `run.sh` checks at each run that it still breaks `CreateUsesOwnClass` and `LoadDeletesOnlyOwnRef`.
+
+## Does my change touch the verified code?
+
+Run this skill when the diff since the sync commit changes any covered code:
+
+```sh
+git diff --stat 0d255369dd8233e3ed1bce0575ab98b2bbd98d07 -- native/ test/workers.test.ts src/index.ts src/loader.ts package.json package-lock.json
+```
+
+Also run it when a change adds a new place that stores a `Napi::Reference`, `Napi::FunctionReference`, or other static or global state in `native/`, or a new path that frees or uses `terminal_`. Static or global JS-facing state is the F1 bug class: keep it in the environment's instance data.
+
+## Coverage record
+
+Sync commit: `0d255369dd8233e3ed1bce0575ab98b2bbd98d07`. At this commit the model describes the code below. Move the sync commit forward only after you confirm that the model still describes the covered code at the new commit.
+
+| Code | Model |
+|---|---|
+| `native/terminal.cc` `TerminalWrap::Init` and `TerminalWrap::Create` keep the class reference in `env.SetInstanceData` / `env.GetInstanceData` | `CtorStorage = "per_env"`, variable `slot` |
+| `native/addon.cc` `InitAll`, `NODE_API_MODULE`; `native/terminal.cc` `TerminalWrap::Init` (asserts an empty instance-data slot, then `env.SetInstanceData`) | `LoadAddon(e)` |
+| `src/loader.ts` `loadNative` (caches the addon, so each env loads it once) | `LoadAddon` is enabled only while `env[e] = "idle"` |
+| `src/index.ts` `createTerminal`; `native/terminal.cc` `CreateTerminal`, `TerminalWrap::Create` (`constructor->New`), `TerminalWrap::TerminalWrap` (`ghostty_terminal_new`) | `CreateTerminal(e, t)` |
+| `src/index.ts` `feed`, `resize`, `snapshot`, `getVisibleText`, `formatPlain`, `formatHtml`, `#assertUsable`; `native/terminal.cc` the same methods and `RequireTerminal` | `Use(t)`, constants `TsDisposedGuard`, `NativeNullGuard` |
+| `src/index.ts` `dispose`; `native/terminal.cc` `TerminalWrap::Dispose`, `DisposeNative` | `Dispose(t)`, `DisposeNative(r)`, constant `DisposeClearsPtr` |
+| `native/terminal.cc` `TerminalWrap::~TerminalWrap` (ObjectWrap finalizer) | `Drop(t)`, `Finalize(t)` |
+| Node environment teardown when a Worker exits | `WorkerExit(w)` |
+| node-addon-api 8.9.2 `FunctionReference::New` (uses the env stored in the reference) and `Reference::~Reference` / `operator=` (run `napi_delete_reference` with the stored env) | `CreateTerminal` sets `refUse` with the slot's owner; `LoadAddon` sets `refUse` with the old owner |
+
+## Run
+
+Requirements: Java 11 or later on `PATH` (or `JAVA=/path/to/java`), and `curl` for the first run. The first run downloads tla2tools v1.7.4 to `vendor/tla2tools/` (git ignores `vendor/`) and checks its sha256. Set `TLA2TOOLS_JAR` to use a jar that you already have.
+
+```sh
+.agents/skills/verify-native-lifecycle/run.sh            # logs go to a new mktemp dir
+.agents/skills/verify-native-lifecycle/run.sh "$OUT_DIR" # or to a dir you name
+```
+
+It takes about 20 seconds. It runs TLC once for each config and rule, and prints one row for each with `RESULT`, `EXPECT`, and the log path. Exit `0` means that every result matches `EXPECT`. Exit `1` means that a row is marked `DIFFERS`. Exit `2` means that TLC or the model failed: read the error.
+
+| Config | What it is | Expected breaks |
+|---|---|---|
+| `model/current.cfg` | The current code. Main thread, 2 workers, 2 terminals. | none |
+| `model/mutant-process-static.cfg` | The old code: one class reference for the whole process (F1). | `CreateUsesOwnClass`, `LoadDeletesOnlyOwnRef` |
+| `model/mutant-dispose-keeps-pointer.cfg` | Current code, but `DisposeNative` does not set `terminal_ = nullptr`. | `HandleFreedOnce` |
+| `model/mutant-no-use-guards.cfg` | Current code, but no `#assertUsable` and no `RequireTerminal` null check. | `NoCallOnDeadHandle` |
+
+The mutant configs prove at each run that each rule can fail. Removing only one of the two use guards breaks nothing, because the other guard still stops the call.
+
+`test/workers.test.ts` replays the worker counterexamples against the real addon, in child processes: a live worker, a worker that exited, and two workers. `npm test` runs it. It crashed in all three scenarios before the F1 fix.
+
+## Read the result
+
+Read every result with the `/statechart` skill when your agent has it (it ships with the pstack plugin, not with this repo). Copy `model/AddonEnvLifecycle.tla`, a config, and `model/statechart-view.mjs` to a scratch folder outside the repo, and give `/statechart` that config and the view. `model/chart.cfg` has small bounds (one worker, one terminal) so that the chart fits. For a broken rule, `/statechart` gives the shortest path in plain words. For a pass, it draws how the system moves between states. If the view no longer fits `/statechart`'s view interface, rewrite it from that skill's instructions.
+
+Without `/statechart`, read the log that the row names. For a broken rule, TLC prints `Error: Invariant <rule> is violated` and then the shortest path as `State 1:`, `State 2:`, ... blocks. Each block names the action that made it (for example `<LoadAddon line 98 ...>`) and the value of every variable after that step. Tell the path as one sentence for each action, in the words of the coverage record.
+
+When a row says `DIFFERS`:
+
+1. A rule breaks that `EXPECT` says holds. Open the log that the row names and read the counterexample. Replay each step against the real code, as `test/workers.test.ts` does for F1, or with a short script in `$TMPDIR`. If each step can happen in the code, it is a bug: report it with the steps in the code's words. Do not change the model or `EXPECT` to make it pass. If a step cannot happen in the code, the model is wrong: fix the action and say what was wrong.
+2. A rule holds that `EXPECT` says breaks. The model lost the power to catch that break. Fix the model.
+3. `TypeOK` breaks, or TLC reports an error. The model is wrong. Fix it before you read any other result.
+
+## Update after an intended change
+
+Change the model from the code, before you rerun. Do not shape it by what makes the check pass.
+
+1. For each changed function in the coverage record, update its action so that the action again does what the code does. Keep one step without other JS in between as one action.
+2. When new code stores a reference or frees or uses `terminal_`, add an action for it and a row in the coverage record.
+3. When the change is meant to break a rule, the promise changed. Change the rule only with evidence (a doc comment, a test, the changelog), and write down the old and the new wording.
+4. Rerun `run.sh` and `npm test`. Then break the new code the way a rule guards against, in a scratch change, and confirm that the check catches it. Drop the scratch change.
+5. Update the coverage record and move the sync commit to the commit that you checked.
+
+## Bounds and assumptions
+
+- Bounds: the main thread and 2 workers, 2 terminals. `current.cfg` has 2,121 distinct states.
+- Each action is atomic. Different envs run on different threads. With one class reference for each env, two envs share no addon state, so treating each step as atomic hides no interleaving of addon state. With a shared slot (`mutant-process-static`), the threads also race on it: that adds bad behaviors, and the model already finds the slot bugs without it.
+- Assumption: when a Worker exits, Node runs the finalizers of its wrapped objects and invalidates the references that its env made. The model does not model the main thread's exit.
+- Assumption: each env loads the addon once. Node gives each load of the addon its own `napi_env`, even two `process.dlopen` calls in one thread, so `TerminalWrap::Init` asserts that the slot is empty. The model does not explore a second load.
+- Assumption: JS code cannot run inside a native method. This holds because `src/index.ts` passes plain option objects that it builds itself, so no getter runs in `OptionBool` or `options.Get`. A caller that reaches the native object directly is outside the model.
+
+## Not covered
+
+- libghostty itself: VT parsing and every `ghostty_*` call are trusted.
+- The content of snapshots and visible text (`ReadLine`, `ReadCellText`, `BuildCellObject`, `ResolveStyleColor`).
+- Argument validation, `getNativeInfo`, prebuild loading, and packaging.
+- More than one load of the addon in one env, for example two copies of the package at different paths.
diff --git a/.agents/skills/verify-native-lifecycle/model/AddonEnvLifecycle.tla b/.agents/skills/verify-native-lifecycle/model/AddonEnvLifecycle.tla
new file mode 100644
index 0000000..cca5227
--- /dev/null
+++ b/.agents/skills/verify-native-lifecycle/model/AddonEnvLifecycle.tla
@@ -0,0 +1,223 @@
+-------------------------- MODULE AddonEnvLifecycle --------------------------
+(***************************************************************************)
+(* How @coder/libghostty-vt-node keeps native state across Node           *)
+(* environments (the main thread and each worker_threads Worker), and     *)
+(* across one terminal's life: create, use, dispose, garbage collection.  *)
+(*                                                                         *)
+(* Each action is one step that the code takes without other JS code     *)
+(* running in between. Each action names the code it stands for.          *)
+(* The verify skill that runs this model is                               *)
+(* .agents/skills/verify-native-lifecycle/SKILL.md                        *)
+(***************************************************************************)
+EXTENDS Naturals
+
+CONSTANTS
+    Main,             \* the main thread's Node environment
+    Workers,          \* worker_threads environments
+    Terminals,        \* JS terminal objects the program can create
+    CtorStorage,      \* where the TerminalWrap class reference lives:
+                      \*  "per_env": one slot for each environment, in its
+                      \*     instance data (TerminalWrap::Init calls
+                      \*     env.SetInstanceData). This is the current code.
+                      \*  "process_static": one slot for the whole process (a
+                      \*     `static Napi::FunctionReference constructor`). This
+                      \*     was the code before the F1 fix.
+    DisposeClearsPtr, \* DisposeNative sets `terminal_ = nullptr` after
+                      \* ghostty_terminal_free (native/terminal.cc). Code: TRUE.
+    TsDisposedGuard,  \* Terminal.#assertUsable throws after dispose
+                      \* (src/index.ts). Code: TRUE.
+    NativeNullGuard   \* TerminalWrap::RequireTerminal throws when terminal_ is
+                      \* nullptr (native/terminal.cc). Code: TRUE.
+
+ASSUME CtorStorage \in {"process_static", "per_env"}
+ASSUME {DisposeClearsPtr, TsDisposedGuard, NativeNullGuard} \subseteq BOOLEAN
+ASSUME Main \notin Workers
+
+Envs == {Main} \cup Workers
+None == "none"
+
+VARIABLES
+    env,        \* env[e]: "idle" (addon not loaded yet), "loaded", or "exited"
+    slot,       \* the env that created the reference held in the constructor
+                \* slot, or None. process_static: one value. per_env: Envs -> value.
+    term,       \* term[t]: the JS Terminal, its TerminalWrap, and its handle
+    refUse,     \* the napi reference that this step touched
+    handleUse   \* the libghostty call (other than free) that this step made
+
+vars == <<env, slot, term, refUse, handleUse>>
+
+NoRefUse    == [op |-> "none", by |-> None, owner |-> None]
+NoHandleUse == [op |-> "none", t |-> None, state |-> "none"]
+
+\* in:     the env that created the terminal
+\* js:     "none" (not created), "live", "disposed" (Terminal.#disposed),
+\*         "dropped" (unreachable, not yet collected), "finalized"
+\* ptr:    TerminalWrap::terminal_ != nullptr
+\* handle: the GhosttyTerminal: "none", "live", or "freed"
+\* frees:  how many times ghostty_terminal_free ran on this handle
+Unborn == [in |-> None, js |-> "none", ptr |-> FALSE, handle |-> "none", frees |-> 0]
+
+SlotOf(e) == IF CtorStorage = "process_static" THEN slot ELSE slot[e]
+SetSlot(e, owner) ==
+    IF CtorStorage = "process_static" THEN owner ELSE [slot EXCEPT ![e] = owner]
+
+\* TerminalWrap::DisposeNative (native/terminal.cc):
+\*   if (terminal_ == nullptr) return;
+\*   ghostty_terminal_free(terminal_);
+\*   terminal_ = nullptr;
+DisposeNative(r) ==
+    IF r.ptr
+    THEN [r EXCEPT !.handle = "freed", !.frees = r.frees + 1, !.ptr = ~DisposeClearsPtr]
+    ELSE r
+
+TypeOK ==
+    /\ env \in [Envs -> {"idle", "loaded", "exited"}]
+    /\ \A t \in Terminals :
+         /\ term[t].in \in Envs \cup {None}
+         /\ term[t].js \in {"none", "live", "disposed", "dropped", "finalized"}
+         /\ term[t].ptr \in BOOLEAN
+         /\ term[t].handle \in {"none", "live", "freed"}
+         /\ term[t].frees \in 0..2
+
+Init ==
+    /\ env = [e \in Envs |-> "idle"]
+    /\ slot = IF CtorStorage = "process_static" THEN None ELSE [e \in Envs |-> None]
+    /\ term = [t \in Terminals |-> Unborn]
+    /\ refUse = NoRefUse
+    /\ handleUse = NoHandleUse
+
+(***************************************************************************)
+(* The first import of dist/index.js in env e calls loadNative            *)
+(* (src/loader.ts), so node-gyp-build loads the addon: NODE_API_MODULE ->  *)
+(* InitAll -> TerminalWrap::Init (native/addon.cc, native/terminal.cc).    *)
+(* per_env: Init asserts that this env's instance-data slot is empty, and *)
+(* stores a new reference with env.SetInstanceData. process_static:        *)
+(* `constructor =                                                          *)
+(* Napi::Persistent(func)` is a move assignment, and node-addon-api's      *)
+(* Reference::operator= runs napi_delete_reference(old _env, old _ref).    *)
+(* Each env loads the addon once: loadNative caches it.                    *)
+(***************************************************************************)
+LoadAddon(e) ==
+    /\ env[e] = "idle"
+    /\ env' = [env EXCEPT ![e] = "loaded"]
+    /\ refUse' = IF SlotOf(e) = None THEN NoRefUse
+                 ELSE [op |-> "load deletes old reference", by |-> e, owner |-> SlotOf(e)]
+    /\ slot' = SetSlot(e, e)
+    /\ handleUse' = NoHandleUse
+    /\ UNCHANGED term
+
+(***************************************************************************)
+(* createTerminal (src/index.ts) -> native CreateTerminal ->               *)
+(* TerminalWrap::Create (native/terminal.cc): per_env reads the reference  *)
+(* with env.GetInstanceData; process_static reads the static. Then         *)
+(* FunctionReference::New runs in the env stored in the reference, not in  *)
+(* the caller's env. The TerminalWrap constructor calls                    *)
+(* ghostty_terminal_new.                                                   *)
+(***************************************************************************)
+CreateTerminal(e, t) ==
+    /\ env[e] = "loaded"
+    /\ term[t].js = "none"
+    /\ refUse' = [op |-> "createTerminal uses class reference", by |-> e, owner |-> SlotOf(e)]
+    /\ term' = [term EXCEPT ![t] =
+                  [in |-> e, js |-> "live", ptr |-> TRUE, handle |-> "live", frees |-> 0]]
+    /\ handleUse' = NoHandleUse
+    /\ UNCHANGED <<env, slot>>
+
+(***************************************************************************)
+(* feed, resize, snapshot, getVisibleText, formatPlain, formatHtml         *)
+(* (src/index.ts). Terminal.#assertUsable throws after dispose. Then the   *)
+(* native method calls RequireTerminal, which throws when terminal_ is     *)
+(* nullptr. Otherwise the method calls libghostty with terminal_.          *)
+(***************************************************************************)
+Use(t) ==
+    LET r == term[t]
+        tsStops     == TsDisposedGuard /\ r.js = "disposed"
+        nativeStops == NativeNullGuard /\ ~r.ptr
+    IN /\ r.js \in {"live", "disposed"}
+       /\ env[r.in] = "loaded"
+       /\ handleUse' = IF tsStops \/ nativeStops THEN NoHandleUse
+                       ELSE [op |-> "libghostty call", t |-> t,
+                             state |-> IF r.ptr THEN r.handle ELSE "null"]
+       /\ refUse' = NoRefUse
+       /\ UNCHANGED <<env, slot, term>>
+
+(***************************************************************************)
+(* Terminal.dispose (src/index.ts): it returns at once when #disposed is   *)
+(* set. Otherwise it calls the native dispose, TerminalWrap::Dispose ->    *)
+(* DisposeNative (native/terminal.cc), and then sets #disposed.            *)
+(***************************************************************************)
+Dispose(t) ==
+    /\ term[t].js = "live"
+    /\ env[term[t].in] = "loaded"
+    /\ term' = [term EXCEPT ![t] = [DisposeNative(@) EXCEPT !.js = "disposed"]]
+    /\ refUse' = NoRefUse
+    /\ handleUse' = NoHandleUse
+    /\ UNCHANGED <<env, slot>>
+
+\* The program drops its last reference to the Terminal object.
+Drop(t) ==
+    /\ term[t].js \in {"live", "disposed"}
+    /\ env[term[t].in] = "loaded"
+    /\ term' = [term EXCEPT ![t].js = "dropped"]
+    /\ refUse' = NoRefUse
+    /\ handleUse' = NoHandleUse
+    /\ UNCHANGED <<env, slot>>
+
+\* V8 collects the object. The ObjectWrap finalizer deletes the TerminalWrap:
+\* ~TerminalWrap -> DisposeNative (native/terminal.cc).
+Finalize(t) ==
+    /\ term[t].js = "dropped"
+    /\ env[term[t].in] = "loaded"
+    /\ term' = [term EXCEPT ![t] = [DisposeNative(@) EXCEPT !.js = "finalized"]]
+    /\ refUse' = NoRefUse
+    /\ handleUse' = NoHandleUse
+    /\ UNCHANGED <<env, slot>>
+
+(***************************************************************************)
+(* A Worker exits. Node tears down its environment: it runs the finalizer  *)
+(* of each object that is still wrapped (~TerminalWrap -> DisposeNative),  *)
+(* and the references that the env created become invalid. A               *)
+(* process-static constructor slot keeps the stale value.                  *)
+(***************************************************************************)
+WorkerExit(w) ==
+    /\ env[w] = "loaded"
+    /\ env' = [env EXCEPT ![w] = "exited"]
+    /\ term' = [t \in Terminals |->
+                  IF term[t].in = w /\ term[t].js \in {"live", "disposed", "dropped"}
+                  THEN [DisposeNative(term[t]) EXCEPT !.js = "finalized"]
+                  ELSE term[t]]
+    /\ refUse' = NoRefUse
+    /\ handleUse' = NoHandleUse
+    /\ UNCHANGED slot
+
+Next ==
+    \/ \E e \in Envs : LoadAddon(e)
+    \/ \E e \in Envs, t \in Terminals : CreateTerminal(e, t)
+    \/ \E t \in Terminals : Use(t)
+    \/ \E t \in Terminals : Dispose(t)
+    \/ \E t \in Terminals : Drop(t)
+    \/ \E t \in Terminals : Finalize(t)
+    \/ \E w \in Workers : WorkerExit(w)
+
+Spec == Init /\ [][Next]_vars
+
+(***************************************************************************)
+(* Rules                                                                   *)
+(***************************************************************************)
+
+\* createTerminal in a thread uses the class reference that this thread made.
+CreateUsesOwnClass ==
+    refUse.op = "createTerminal uses class reference" => refUse.owner = refUse.by
+
+\* Loading the addon in a thread never deletes another thread's reference.
+LoadDeletesOnlyOwnRef ==
+    refUse.op = "load deletes old reference" => refUse.owner = refUse.by
+
+\* libghostty frees each terminal handle at most once.
+HandleFreedOnce == \A t \in Terminals : term[t].frees <= 1
+
+\* No libghostty call reaches a freed or null terminal handle.
+NoCallOnDeadHandle ==
+    handleUse.op = "libghostty call" => handleUse.state = "live"
+
+=============================================================================
diff --git a/.agents/skills/verify-native-lifecycle/model/chart.cfg b/.agents/skills/verify-native-lifecycle/model/chart.cfg
new file mode 100644
index 0000000..ccd9b7b
--- /dev/null
+++ b/.agents/skills/verify-native-lifecycle/model/chart.cfg
@@ -0,0 +1,17 @@
+\* Small bounds for the /statechart chart: one worker, one terminal. Current code.
+CONSTANTS
+    Main = main
+    Workers = {w1}
+    Terminals = {t1}
+    CtorStorage = "per_env"
+    DisposeClearsPtr = TRUE
+    TsDisposedGuard = TRUE
+    NativeNullGuard = TRUE
+SPECIFICATION Spec
+CHECK_DEADLOCK FALSE
+INVARIANTS
+    TypeOK
+    CreateUsesOwnClass
+    LoadDeletesOnlyOwnRef
+    HandleFreedOnce
+    NoCallOnDeadHandle
diff --git a/.agents/skills/verify-native-lifecycle/model/current.cfg b/.agents/skills/verify-native-lifecycle/model/current.cfg
new file mode 100644
index 0000000..a00c6e8
--- /dev/null
+++ b/.agents/skills/verify-native-lifecycle/model/current.cfg
@@ -0,0 +1,17 @@
+\* The current code. Run by run.sh and compared with run.sh EXPECT.
+CONSTANTS
+    Main = main
+    Workers = {w1, w2}
+    Terminals = {t1, t2}
+    CtorStorage = "per_env"
+    DisposeClearsPtr = TRUE
+    TsDisposedGuard = TRUE
+    NativeNullGuard = TRUE
+SPECIFICATION Spec
+CHECK_DEADLOCK FALSE
+INVARIANTS
+    TypeOK
+    CreateUsesOwnClass
+    LoadDeletesOnlyOwnRef
+    HandleFreedOnce
+    NoCallOnDeadHandle
diff --git a/.agents/skills/verify-native-lifecycle/model/mutant-dispose-keeps-pointer.cfg b/.agents/skills/verify-native-lifecycle/model/mutant-dispose-keeps-pointer.cfg
new file mode 100644
index 0000000..4f10f6b
--- /dev/null
+++ b/.agents/skills/verify-native-lifecycle/model/mutant-dispose-keeps-pointer.cfg
@@ -0,0 +1,17 @@
+\* Current code with one break: DisposeNative does not set terminal_ = nullptr.
+CONSTANTS
+    Main = main
+    Workers = {w1, w2}
+    Terminals = {t1, t2}
+    CtorStorage = "per_env"
+    DisposeClearsPtr = FALSE
+    TsDisposedGuard = TRUE
+    NativeNullGuard = TRUE
+SPECIFICATION Spec
+CHECK_DEADLOCK FALSE
+INVARIANTS
+    TypeOK
+    CreateUsesOwnClass
+    LoadDeletesOnlyOwnRef
+    HandleFreedOnce
+    NoCallOnDeadHandle
diff --git a/.agents/skills/verify-native-lifecycle/model/mutant-no-use-guards.cfg b/.agents/skills/verify-native-lifecycle/model/mutant-no-use-guards.cfg
new file mode 100644
index 0000000..6249def
--- /dev/null
+++ b/.agents/skills/verify-native-lifecycle/model/mutant-no-use-guards.cfg
@@ -0,0 +1,17 @@
+\* Current code with one break: no #assertUsable and no RequireTerminal null check.
+CONSTANTS
+    Main = main
+    Workers = {w1, w2}
+    Terminals = {t1, t2}
+    CtorStorage = "per_env"
+    DisposeClearsPtr = TRUE
+    TsDisposedGuard = FALSE
+    NativeNullGuard = FALSE
+SPECIFICATION Spec
+CHECK_DEADLOCK FALSE
+INVARIANTS
+    TypeOK
+    CreateUsesOwnClass
+    LoadDeletesOnlyOwnRef
+    HandleFreedOnce
+    NoCallOnDeadHandle
diff --git a/.agents/skills/verify-native-lifecycle/model/mutant-process-static.cfg b/.agents/skills/verify-native-lifecycle/model/mutant-process-static.cfg
new file mode 100644
index 0000000..31fd31c
--- /dev/null
+++ b/.agents/skills/verify-native-lifecycle/model/mutant-process-static.cfg
@@ -0,0 +1,17 @@
+\* The old code (before the F1 fix): one process-wide constructor slot. Must break the F1 rules.
+CONSTANTS
+    Main = main
+    Workers = {w1, w2}
+    Terminals = {t1, t2}
+    CtorStorage = "process_static"
+    DisposeClearsPtr = TRUE
+    TsDisposedGuard = TRUE
+    NativeNullGuard = TRUE
+SPECIFICATION Spec
+CHECK_DEADLOCK FALSE
+INVARIANTS
+    TypeOK
+    CreateUsesOwnClass
+    LoadDeletesOnlyOwnRef
+    HandleFreedOnce
+    NoCallOnDeadHandle
diff --git a/.agents/skills/verify-native-lifecycle/model/statechart-view.mjs b/.agents/skills/verify-native-lifecycle/model/statechart-view.mjs
new file mode 100644
index 0000000..22276e2
--- /dev/null
+++ b/.agents/skills/verify-native-lifecycle/model/statechart-view.mjs
@@ -0,0 +1,52 @@
+// View for /statechart: labels each model state and step in the words of a
+// package user. Used with model/chart.cfg (one worker, one terminal).
+const thread = (s) => ({ idle: "not loaded", loaded: "addon loaded", exited: "exited" })[s];
+const owner = (o) => (o === "none" ? "empty" : o === "main" ? "main's" : "worker's");
+// per_env stores one slot for each env; process_static (old code) stores one.
+const slots = (s) => (typeof s === "string" ? { "Class reference": owner(s) } : {
+  "Main's class reference": owner(s.main),
+  "Worker's class reference": owner(s.w1),
+});
+const terminal = (t) => {
+  if (t.js === "none") return "none";
+  const where = t.in === "main" ? "main" : "worker";
+  const handle = t.frees > 1 ? "freed twice" : t.handle === "freed" ? "freed" : "open";
+  const js = { live: "in use", disposed: "disposed", dropped: "unreachable", finalized: "collected" }[t.js];
+  return `${where}: ${js}, handle ${handle}`;
+};
+
+export const title = "libghostty-vt-node: the main thread and a worker, each with its own class reference";
+
+export const state = (v) => ({
+  "Main thread": thread(v.env.main),
+  Worker: thread(v.env.w1),
+  ...slots(v.slot),
+  Terminal: terminal(v.term.t1),
+});
+
+const who = (from, to) => {
+  for (const e of Object.keys(to.env)) if (from.env[e] !== to.env[e]) return e === "main" ? "main" : "the worker";
+  return "a thread";
+};
+const creator = (to) => (to.term.t1.in === "main" ? "main" : "the worker");
+
+export const step = (action, from, to) => {
+  switch (action) {
+    case "LoadAddon":
+      return `${who(from, to)} imports the package`;
+    case "CreateTerminal":
+      return `${creator(to)} calls createTerminal`;
+    case "Use":
+      return to.handleUse.op === "none" ? null : "the program feeds or reads the terminal";
+    case "Dispose":
+      return "the program calls dispose()";
+    case "Drop":
+      return "the program drops the terminal";
+    case "Finalize":
+      return "the GC collects the terminal";
+    case "WorkerExit":
+      return "the worker exits";
+    default:
+      throw new Error(`unknown action ${action}`);
+  }
+};
diff --git a/.agents/skills/verify-native-lifecycle/run.sh b/.agents/skills/verify-native-lifecycle/run.sh
new file mode 100755
index 0000000..98de60c
--- /dev/null
+++ b/.agents/skills/verify-native-lifecycle/run.sh
@@ -0,0 +1,101 @@
+#!/usr/bin/env bash
+# Model-check model/AddonEnvLifecycle.tla with TLC, one run per rule and config,
+# and compare each result with EXPECT below.
+#
+# Usage: .agents/skills/verify-native-lifecycle/run.sh [OUT_DIR]
+#   OUT_DIR keeps every TLC log (default: a new mktemp dir, printed at the end).
+# Env:   TLA2TOOLS_JAR=/path/to/tla2tools.jar  use this jar (must be v1.7.4)
+#        JAVA=/path/to/java                    Java 11 or later (default: java on PATH)
+# Exit:  0 = every result matches EXPECT, 1 = a result differs, 2 = tool or model error.
+set -euo pipefail
+
+SKILL_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)"
+ROOT="$(cd "$SKILL_DIR/../../.." && pwd)"
+MODEL_DIR="$SKILL_DIR/model"
+SPEC=AddonEnvLifecycle
+TLA_VERSION=1.7.4
+TLA_SHA256=936a262061c914694dfd669a543be24573c45d5aa0ff20a8b96b23d01e050e88
+JAVA="${JAVA:-java}"
+
+RULES=(CreateUsesOwnClass LoadDeletesOnlyOwnRef HandleFreedOnce NoCallOnDeadHandle)
+
+# EXPECT: the rules that each config must break. Every other rule must hold.
+# Each mutant is the current code with one break, and must break its rule.
+# (A function, not an associative array: macOS ships bash 3.2.)
+expect_breaks() {
+  case "$1" in
+    current) echo "" ;;
+    mutant-process-static) echo "CreateUsesOwnClass LoadDeletesOnlyOwnRef" ;;
+    mutant-dispose-keeps-pointer) echo "HandleFreedOnce" ;;
+    mutant-no-use-guards) echo "NoCallOnDeadHandle" ;;
+    *) echo "error: no EXPECT entry for config $1" >&2; exit 2 ;;
+  esac
+}
+CONFIGS=(current mutant-process-static mutant-dispose-keeps-pointer mutant-no-use-guards)
+for cfg in "${CONFIGS[@]}"; do expect_breaks "$cfg" >/dev/null; done
+
+command -v "$JAVA" >/dev/null || { echo "error: java not found; set JAVA or install Java 11+" >&2; exit 2; }
+
+jar="${TLA2TOOLS_JAR:-$ROOT/vendor/tla2tools/tla2tools-$TLA_VERSION.jar}"
+if [[ ! -f "$jar" ]]; then
+  mkdir -p "$(dirname "$jar")"
+  echo "Downloading tla2tools v$TLA_VERSION to $jar"
+  curl -fsSL -o "$jar.part" "https://github.com/tlaplus/tlaplus/releases/download/v$TLA_VERSION/tla2tools.jar"
+  mv "$jar.part" "$jar"
+fi
+if command -v sha256sum >/dev/null; then
+  actual_sha="$(sha256sum "$jar" | cut -d' ' -f1)"
+else
+  actual_sha="$(shasum -a 256 "$jar" | cut -d' ' -f1)"
+fi
+if [[ "$actual_sha" != "$TLA_SHA256" ]]; then
+  echo "error: $jar has sha256 $actual_sha, expected $TLA_SHA256 (tla2tools v$TLA_VERSION)" >&2
+  exit 2
+fi
+
+out="${1:-$(mktemp -d "${TMPDIR:-/tmp}/verify-native-lifecycle.XXXXXX")}"
+mkdir -p "$out"
+cp "$MODEL_DIR/$SPEC.tla" "$out/"
+
+status=0
+printf '%-30s %-24s %-7s %-7s %s\n' CONFIG RULE RESULT EXPECT LOG
+for cfg in "${CONFIGS[@]}"; do
+  [[ -f "$MODEL_DIR/$cfg.cfg" ]] || { echo "error: missing $MODEL_DIR/$cfg.cfg" >&2; exit 2; }
+  for rule in "${RULES[@]}"; do
+    name="$cfg.$rule"
+    # Same constants as the config; check TypeOK and this one rule only.
+    sed '/^INVARIANTS/,$d' "$MODEL_DIR/$cfg.cfg" > "$out/$name.cfg"
+    printf 'INVARIANTS\n    TypeOK\n    %s\n' "$rule" >> "$out/$name.cfg"
+    log="$out/$name.out"
+    (cd "$out" && "$JAVA" -XX:+UseParallelGC -cp "$jar" tlc2.TLC -workers 1 \
+        -metadir "$out/.states/$name" -config "$name.cfg" "$SPEC.tla") > "$log" 2>&1 || true
+
+    if grep -q "Invariant TypeOK is violated" "$log"; then
+      echo "error: TypeOK breaks in $cfg: the model is wrong, not the code. See $log" >&2
+      exit 2
+    elif grep -q "Invariant $rule is violated" "$log"; then
+      result=breaks
+    elif grep -q "Model checking completed. No error has been found." "$log"; then
+      result=holds
+    else
+      echo "error: TLC did not finish $name. See $log" >&2
+      tail -20 "$log" >&2
+      exit 2
+    fi
+
+    expect=holds
+    [[ " $(expect_breaks "$cfg") " == *" $rule "* ]] && expect=breaks
+    mark=""
+    if [[ "$result" != "$expect" ]]; then mark="  <-- DIFFERS"; status=1; fi
+    printf '%-30s %-24s %-7s %-7s %s%s\n' "$cfg" "$rule" "$result" "$expect" "$log" "$mark"
+  done
+done
+
+echo
+echo "TLC logs and counterexamples: $out"
+if [[ $status -eq 0 ]]; then
+  echo "OK: every result matches EXPECT."
+else
+  echo "DIFFERS: read each marked log. See 'Read the result' in SKILL.md."
+fi
+exit $status