diff --git a/.github/workflows/model-sync.yml b/.github/workflows/model-sync.yml
new file mode 100644
index 00000000..7655ad00
--- /dev/null
+++ b/.github/workflows/model-sync.yml
@@ -0,0 +1,43 @@
+name: Model sync
+
+# Models track the code: a PR that changes code a TLA+ model covers
+# (verification/model-map.toml) updates the model in the same PR, and every
+# lifecycle trace event the code records is replayed by its trace spec, and
+# every model is checked against real runs (or explicitly allowlisted).
+# See docs/TESTING.md (verification layers) and verification/tla/README.md.
+on:
+  pull_request:
+    branches: ["main"]
+    # labeled/unlabeled/edited: adding `no-model-change` or the
+    # `Model: no change because ...` line re-runs the check.
+    types: [opened, synchronize, reopened, labeled, unlabeled, edited, ready_for_review]
+  merge_group:
+  push:
+    branches: ["main"]
+
+permissions:
+  contents: read
+
+concurrency:
+  group: model-sync-${{ github.event.pull_request.number || github.sha }}
+  cancel-in-progress: true
+
+jobs:
+  model-sync:
+    runs-on: ubuntu-latest
+    timeout-minutes: 5
+    steps:
+      - uses: actions/checkout@v4
+        with:
+          fetch-depth: 0
+      - name: Self-tests
+        run: python3 -m unittest scripts/tests/test_model_sync.py
+      - name: Every trace event is mapped
+        run: python3 scripts/check-model-sync.py events
+      - name: Every model is trace-validated (or allowlisted), coverage floors hold
+        run: python3 scripts/check-model-sync.py models
+      # On merge_group and push the script passes: the pull_request run
+      # already enforced it (labels are not visible in the merge queue).
+      - name: Modelled code changes update their model
+        if: github.event_name != 'push'
+        run: python3 scripts/check-model-sync.py paths
diff --git a/CHANGELOG.md b/CHANGELOG.md
index 676edf3b..23c2cf9a 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -26,6 +26,13 @@
   console in every binary, targeted at 0.9) with tiers and target versions, and the OTP features Spawned will
   not add as non-goals; the comparison is in
   `docs/research/otp-elixir-gleam.md`.
+- CI: model-sync checks. A `model-sync` job fails a PR that changes code a TLA+
+  model covers (`verification/model-map.toml`) without touching that model,
+  unless it carries the `no-model-change` label and a `Model: no change because
+  <reason>` line. Every lifecycle trace event kind must map to a trace-spec
+  action; every model must be trace-validated or allowlisted as TLC-only with
+  a tracking item (Coordinator, Lifecycle, DeferredReplies, DeferredJobs);
+  per-model trace coverage has a floor that may only go up.
 - Tests: coverage follow-ups. `restart_modes_distinguish_normal_shutdown_and_panic`
   now sends a real `Normal` exit; a per-PR `MCSupervisionTemporary` TLC
   configuration makes `TemporaryStartsOnce` non-vacuous, with a negative
diff --git a/ROADMAP.md b/ROADMAP.md
index 8eeff166..b5a27f68 100644
--- a/ROADMAP.md
+++ b/ROADMAP.md
@@ -318,6 +318,16 @@ without each other's findings), containing:
    benchmark against main; anything costly is opt-in.
 8. **A client mapping:** the Ethrex and Ethlambda call sites it changes.
 
+Models track the code. A PR that changes modelled behaviour updates the model
+in the same PR; drift is a bug. The `model-sync` CI check enforces it: code
+mapped to a model in `verification/model-map.toml` may not change without
+that model (or the `no-model-change` label and a `Model: no change because
+<reason>` line), every lifecycle trace event must be replayed by its
+trace spec, every model must be trace-validated against real runs or
+allowlisted with a tracking item (TLC-only today: Coordinator, Lifecycle,
+DeferredReplies, DeferredJobs), and per-model trace coverage may only grow
+([model sync](docs/TESTING.md#model-sync)).
+
 **Production arm (rank 5c).** Trace validation checks test runs. After the
 Ethlambda canary, the same invariants (`AtMostOneGeneration`,
 `PublishedIsLive`, `BudgetBounded`, `ReverseShutdown`, and, once the base
diff --git a/docs/TESTING.md b/docs/TESTING.md
index 8b01a34e..8ee05cfb 100644
--- a/docs/TESTING.md
+++ b/docs/TESTING.md
@@ -114,6 +114,7 @@ Status of each layer. "Planned" items are tracked in the
 | Design, any size | TLAPS or Veil | An invariant that fails only for larger configurations | Planned ([verification tools](research/verification-tools.md)) |
 | Spec and code | Trace validation | The implementation doing something the model forbids | Real OneForOne, cohort and nested traces plus invalid-trace and model-mutation controls |
 | Spec and code coverage | Trace coverage (`verification/tla/trace_coverage.py`) | Model actions, states and transitions no test ever reaches | Report on every PR (actions covered by the dedicated trace tests may not regress); whole test suite weekly. See [trace coverage](#trace-coverage) |
+| Spec and code in sync | `scripts/check-model-sync.py`, `verification/model-map.toml` | A PR changing modelled code without its model; a trace event no trace spec replays; a model no real run is checked against; trace coverage going down | `model-sync` job on every PR. See [model sync](#model-sync) |
 | Primitives | Loom | Atomic and memory-ordering bugs in cancellation, ready gate and wakeups | In CI; expand to reply slots and mailbox publication versus shutdown |
 | Whole runtime, deterministic | Simulation backend for `spawned-rt::tasks` (random, PCT, bounded DFS) | Async races, replayed from a seed with virtual time | In CI (`sim` job, [simulated suites in CI](#simulated-suites-in-ci)) |
 | Resource stability | Soak tests | Memory, file descriptors, threads, tasks and registry entries growing over hours of actor churn and restarts | Planned |
@@ -1125,6 +1126,59 @@ feature that compiles a mutated line before treating it as a gap. Code inside
 `macro_rules!` bodies is not mutated at all, so keep lifecycle code out of
 single-use macros.
 
+### Model sync
+
+Models track the code: a PR that changes behaviour a TLA+ model specifies
+updates the model in the same PR, and drift is a bug. The `model-sync` job
+(`.github/workflows/model-sync.yml`) checks four things mechanically.
+
+- **Paths.** `verification/model-map.toml` maps code to the models that
+  cover it (for example `actor_cleanup.rs`, `link.rs`, `monitor.rs` and the
+  actor loops to `Lifecycle`; `supervision.rs` to `Supervision`, `Cohorts`
+  and `NestedSupervision`; `system.rs` to `Coordinator`). If a PR changes a
+  mapped file but none of its models (the model, its MC configurations,
+  inductive or coverage modules, or trace spec; a comment-only model edit
+  does not count, and one covering model is enough), the job fails. Changes to
+  comments only, or only inside a `#[cfg(test)] mod` block, are exempt (the
+  file's code outside test modules must be unchanged, so removing
+  `#[cfg(test)]` is not exempt); when the script cannot tell, it requires
+  the waiver. The waiver is the
+  `no-model-change` label AND a PR body line `Model: no change because
+  <reason>`. In the merge queue the step passes, which is sound because
+  `model-sync` is a required check on the PR.
+- **Trace events.** Every action name the code can record with the
+  `lifecycle-trace` feature (the string literal, or the literals of an
+  `if .. else` chain, passed to each emitter listed in the map, such as
+  `Event::new`, `Event::sup` and `TreeEvent::new`) must be an `e.a = "..."` arm of its trace spec, or be
+  declared in the map as translated by `trace_check.py` or rejected on
+  purpose (`Unmodelled`). A non-literal action name, an event struct with no
+  map entry, or a cohort event filter that differs from `TraceCohorts.tla`
+  fails. Warnings list spec arms no code emits and model actions no trace
+  spec takes (except those declared unlogged, such as `WindowExpire`). The
+  event names are strings, not an enum, so this is a source scan rather than
+  a compile-time `match`; the mapping it checks lives in TLA+.
+- **Models with trace validation.** Every model in `verification/tla` needs
+  a map entry and trace validation, checked statically: a `Trace*.tla` that
+  extends the model, is named in `trace_check.py`, and has arms that events
+  the code emits reach (the `tla-traces` job replays the recorded traces). A
+  model checked by TLC alone can drift from the code unnoticed, so it fails
+  unless it has a `tlc_only` allowlist entry with a reason and a tracking
+  item. `check-model-sync.py models` prints the current list.
+- **Coverage floors.** Each trace-validated model has a `coverage_floor`: the
+  action keys the dedicated trace tests cover in
+  `verification/tla/coverage-baseline.json` (Supervision 36 of 40, Cohorts
+  40 of 46, Nested 11 of 11). The `tla` job already fails when a baseline key
+  stops being covered; this check fails when the baseline shrinks below the
+  floor, so coverage only grows. Raise the floor when coverage grows.
+
+```bash
+python3 scripts/check-model-sync.py events
+python3 scripts/check-model-sync.py models                      # inventory: trace validation and coverage floors
+python3 scripts/check-model-sync.py paths                       # this branch against origin/main
+python3 scripts/check-model-sync.py paths --pr 123              # with that PR's labels and body
+python3 -m unittest scripts/tests/test_model_sync.py            # self-tests and negative controls
+```
+
 ## Planted-bug sensitivity
 
 Mutation testing breaks one operator at a time. To measure whether the stack
diff --git a/scripts/check-model-sync.py b/scripts/check-model-sync.py
new file mode 100755
index 00000000..22a288e3
--- /dev/null
+++ b/scripts/check-model-sync.py
@@ -0,0 +1,748 @@
+#!/usr/bin/env python3
+"""Check that the TLA+ models track the code (verification/model-map.toml).
+
+    check-model-sync.py paths [--base REF] [--head REF] [--files PATH...]
+                              [--labels L,...] [--body TEXT] [--pr N]
+    check-model-sync.py events
+    check-model-sync.py models
+
+`paths`: fails if the PR changes a code file a model covers without changing
+any of that file's models (model, MC configurations, inductive/coverage
+modules or trace spec). Exempt: changes to comments only or only inside a
+`#[cfg(test)] mod` block, and PRs with the `no-model-change` label AND a body
+line `Model: no change because <reason>`. Labels and body come from
+`GITHUB_EVENT_PATH` in Actions, `--pr N` (gh CLI) or `--labels`/`--body`.
+In a merge queue (`GITHUB_EVENT_NAME=merge_group`) it passes: the PR-level
+run already enforced it.
+
+`events`: every action string the code can record in a lifecycle trace must
+be replayed by a trace spec arm (or be declared translated/rejected in the
+map); unmapped events, non-literal action names and unconfigured event
+structs fail. Spec arms no code emits and model actions no trace reaches are
+printed as warnings.
+
+`models`: every model in verification/tla must be in the map and have trace
+validation (a Trace*.tla spec that trace_check.py runs and recorded events
+reach), unless it has a `tlc_only` allowlist entry with a reason and a
+tracking item; and each model's covered action keys in
+coverage-baseline.json may not drop below its `coverage_floor`.
+
+Standard library only; Python 3.9+ (a TOML subset parser is used when
+`tomllib` is unavailable).
+"""
+import argparse
+import json
+import os
+import re
+import subprocess
+import sys
+from pathlib import Path
+
+ROOT = Path(__file__).resolve().parent.parent
+MAP = "verification/model-map.toml"
+LABEL = "no-model-change"
+REASON = re.compile(r"^\s*Model:\s*no change because\s+(?!<reason>)\S", re.I | re.M)
+
+
+# --------------------------------------------------------------------------
+# Config
+
+def _toml_value(text, i):
+    """Parse one TOML value (string, int, bool, array, inline table)."""
+    def skip(i):
+        while i < len(text):
+            if text[i] in " \t\r\n,":
+                i += 1
+            elif text[i] == "#":
+                while i < len(text) and text[i] != "\n":
+                    i += 1
+            else:
+                break
+        return i
+    c = text[i]
+    if c == "'":
+        j = text.index("'", i + 1)
+        return text[i + 1:j], j + 1
+    if c == '"':
+        j = i + 1
+        out = []
+        while text[j] != '"':
+            if text[j] == "\\":
+                out.append({"n": "\n", "t": "\t"}.get(text[j + 1], text[j + 1]))
+                j += 2
+            else:
+                out.append(text[j])
+                j += 1
+        return "".join(out), j + 1
+    if c == "[":
+        items, i = [], skip(i + 1)
+        while text[i] != "]":
+            value, i = _toml_value(text, i)
+            items.append(value)
+            i = skip(i)
+        return items, i + 1
+    if c == "{":
+        table, i = {}, skip(i + 1)
+        while text[i] != "}":
+            m = re.compile(r"\s*([A-Za-z0-9_-]+)\s*=\s*").match(text, i)
+            value, i = _toml_value(text, m.end())
+            table[m.group(1)] = value
+            i = skip(i)
+        return table, i + 1
+    m = re.compile(r"true|false|-?\d+").match(text, i)
+    word = m.group(0)
+    return (word == "true" if word in ("true", "false") else int(word)), m.end()
+
+
+def parse_toml(text):
+    """The TOML subset model-map.toml uses: [a.b], [[a.b]], key = value."""
+    data, i = {}, 0
+    current = data
+    line = re.compile(r"[ \t]*(?:#[^\n]*)?(?:\n|$)|[ \t]*(\[\[?)([A-Za-z0-9_.-]+)\]\]?[ \t]*(?:#[^\n]*)?(?:\n|$)|[ \t]*([A-Za-z0-9_-]+)[ \t]*=[ \t]*")
+    while i < len(text):
+        m = line.match(text, i)
+        if not m:
+            raise ValueError(f"model map: cannot parse at {text[i:i + 40]!r}")
+        if m.group(2):
+            parts = m.group(2).split(".")
+            node = data
+            for part in parts[:-1]:
+                node = node.setdefault(part, {})
+                if isinstance(node, list):
+                    node = node[-1]
+            if m.group(1) == "[[":
+                node.setdefault(parts[-1], []).append({})
+                current = node[parts[-1]][-1]
+            else:
+                current = node.setdefault(parts[-1], {})
+            i = m.end()
+        elif m.group(3):
+            value, i = _toml_value(text, m.end())
+            current[m.group(3)] = value
+        else:
+            if m.end() == i:
+                break  # end of text
+            i = m.end()
+    return data
+
+
+def load_map(root):
+    text = (root / MAP).read_text()
+    try:
+        import tomllib
+        return tomllib.loads(text)
+    except ImportError:
+        return parse_toml(text)
+
+
+def glob_match(path, pattern):
+    regex = ""
+    k = 0
+    while k < len(pattern):
+        if pattern.startswith("**", k):
+            regex += ".*"
+            k += 2
+        elif pattern[k] == "*":
+            regex += "[^/]*"
+            k += 1
+        elif pattern[k] == "?":
+            regex += "[^/]"
+            k += 1
+        else:
+            regex += re.escape(pattern[k])
+            k += 1
+    return re.fullmatch(regex, path) is not None
+
+
+# --------------------------------------------------------------------------
+# Rust source scanning
+
+def rust_mask(src):
+    """Copy of src with comments, string and char literal contents blanked
+    (same length, newlines kept), so brace and call matching ignores them.
+    Returns (masked, strings) where strings maps literal start -> value."""
+    out = list(src)
+    strings = {}
+    i, n = 0, len(src)
+
+    def blank(a, b):
+        for k in range(a, b):
+            if out[k] != "\n":
+                out[k] = " "
+    while i < n:
+        c = src[i]
+        if src.startswith("//", i):
+            j = src.find("\n", i)
+            j = n if j < 0 else j
+            blank(i, j)
+            i = j
+        elif src.startswith("/*", i):
+            depth, j = 1, i + 2
+            while j < n and depth:
+                if src.startswith("/*", j):
+                    depth, j = depth + 1, j + 2
+                elif src.startswith("*/", j):
+                    depth, j = depth - 1, j + 2
+                else:
+                    j += 1
+            blank(i, j)
+            i = j
+        elif c in "rb" and (i == 0 or not (src[i - 1].isalnum() or src[i - 1] == "_")) and \
+                re.match(r"b?r(#*)\"", src[i:i + 260]):
+            m = re.match(r"b?r(#*)\"", src[i:])
+            close = '"' + m.group(1)
+            j = src.find(close, i + m.end())
+            j = n if j < 0 else j
+            strings[i] = src[i + m.end():j]
+            blank(i + m.end(), j)
+            i = j + len(close)
+        elif c == '"':
+            j, value = i + 1, []
+            while j < n and src[j] != '"':
+                if src[j] == "\\":
+                    value.append(src[j:j + 2])
+                    j += 2
+                else:
+                    value.append(src[j])
+                    j += 1
+            strings[i] = "".join(value)
+            blank(i + 1, j)
+            i = j + 1
+        elif c == "'":
+            if src.startswith("\\", i + 1):
+                j = src.find("'", i + 3)
+                j = n - 1 if j < 0 else j
+                blank(i + 1, j)
+                i = j + 1
+            elif i + 2 < n and src[i + 2] == "'":
+                blank(i + 1, i + 2)
+                i += 3
+            else:
+                i += 1  # lifetime
+        else:
+            i += 1
+    return "".join(out), strings
+
+
+def matching(masked, open_at):
+    pairs = {"(": ")", "{": "}", "[": "]"}
+    stack = []
+    for k in range(open_at, len(masked)):
+        c = masked[k]
+        if c in pairs:
+            stack.append(pairs[c])
+        elif c in ")}]":
+            if not stack or stack.pop() != c:
+                return None
+            if not stack:
+                return k
+    return None
+
+
+def call_argument(masked, open_paren, index):
+    """(start, end) of the index-th top-level argument of the call whose '('
+    is at open_paren, or None."""
+    close = matching(masked, open_paren)
+    if close is None:
+        return None
+    depth, start, arg = 0, open_paren + 1, 0
+    for k in range(open_paren + 1, close + 1):
+        c = masked[k]
+        if c in "([{":
+            depth += 1
+        elif c in ")]}" and k != close:
+            depth -= 1
+        elif (c == "," and depth == 0) or k == close:
+            if arg == index:
+                return start, k
+            arg, start = arg + 1, k + 1
+    return None
+
+
+def action_values(masked, strings, a, b):
+    """Action names an argument expression can evaluate to: a string literal
+    or `if .. { <values> } else { <values> }` (also `else if`). None if
+    anything else could decide the value (a variable, a call, a match)."""
+    while a < b and masked[a].isspace():
+        a += 1
+    while b > a and masked[b - 1].isspace():
+        b -= 1
+    if a >= b:
+        return None
+    if masked[a] == '"' and a in strings:
+        if masked.find('"', a + 1) == b - 1:
+            return [strings[a]]
+        return None
+    if re.match(r"if\b", masked[a:b]):
+        k = a + 2
+        depth = 0
+        while k < b:
+            c = masked[k]
+            if c in "([":
+                depth += 1
+            elif c in ")]":
+                depth -= 1
+            elif c == "{" and depth == 0:
+                break
+            k += 1
+        close = matching(masked, k) if k < b else None
+        if close is None or close >= b:
+            return None
+        then = action_values(masked, strings, k + 1, close)
+        rest = re.match(r"\s*else\b\s*", masked[close + 1:b])
+        if then is None or not rest:
+            return None
+        start = close + 1 + rest.end()
+        if masked[start:start + 1] == "{":
+            end = matching(masked, start)
+            if end != b - 1:
+                return None
+            other = action_values(masked, strings, start + 1, end)
+        else:
+            other = action_values(masked, strings, start, b)
+        return None if other is None else then + other
+    return None
+
+
+def test_module_lines(src):
+    """1-based inclusive line ranges of `#[cfg(test)] mod name { ... }`."""
+    masked, _ = rust_mask(src)
+    ranges = []
+    for m in re.finditer(r"#\[cfg\(test\)\]\s*(?:#\[[^\]]*\]\s*)*(?:pub(?:\([^)]*\))?\s+)?mod\s+\w+\s*\{", masked):
+        close = matching(masked, m.end() - 1)
+        if close is None:
+            return []  # cannot tell: no exemption
+        ranges.append((masked.count("\n", 0, m.start()) + 1, masked.count("\n", 0, close) + 1))
+    return ranges
+
+
+# --------------------------------------------------------------------------
+# paths
+
+def git(root, *args):
+    return subprocess.run(["git", *args], cwd=root, check=True, capture_output=True, text=True).stdout
+
+
+def show(root, rev, path):
+    r = subprocess.run(["git", "show", f"{rev}:{path}"], cwd=root, capture_output=True, text=True)
+    return r.stdout if r.returncode == 0 else ""
+
+
+def production_lines(src):
+    """Non-blank, non-`//` lines outside `#[cfg(test)] mod` blocks."""
+    ranges = test_module_lines(src)
+    return [l.strip() for n, l in enumerate(src.splitlines(), 1)
+            if l.strip() and not l.strip().startswith("//") and not any(x <= n <= y for x, y in ranges)]
+
+
+def exempt_change(root, base, head, path):
+    """'comments' or 'tests' if the change leaves the file's production code
+    (outside `#[cfg(test)] mod` blocks, ignoring `//` comment lines and
+    blank lines) identical, else None. Removing `#[cfg(test)]` or moving
+    code into a test module changes the production lines, so it is not
+    exempt; an unparseable file has no test blocks (no exemption)."""
+    if not path.endswith(".rs"):
+        return None
+    old, new = show(root, base, path), show(root, head, path)
+    if production_lines(old) != production_lines(new):
+        return None
+    strip = lambda src: [l.strip() for l in src.splitlines() if l.strip() and not l.strip().startswith("//")]
+    return "comments" if strip(old) == strip(new) else "tests"
+
+
+def tla_content(src):
+    """A TLA+ module without comments and blank lines."""
+    src = re.sub(r"\(\*.*?\*\)", " ", src, flags=re.S)
+    src = re.sub(r"\\\*[^\n]*", "", src)
+    return [l.strip() for l in src.splitlines() if l.strip()]
+
+
+def model_file_changed(root, base, head, path):
+    """A model-side file counts as updated unless its change is comments only."""
+    if base is None or not path.endswith(".tla"):
+        return True
+    return tla_content(show(root, base, path)) != tla_content(show(root, head, path))
+
+
+def pr_context(args):
+    """(labels, body, event_name) from flags, Actions or gh."""
+    event = os.environ.get("GITHUB_EVENT_NAME", "")
+    labels, body = None, None
+    if args.labels is not None:
+        labels = [l for l in args.labels.split(",") if l]
+    if args.body is not None:
+        body = args.body
+    if (labels is None or body is None) and os.environ.get("GITHUB_EVENT_PATH"):
+        with open(os.environ["GITHUB_EVENT_PATH"]) as f:
+            pr = json.load(f).get("pull_request") or {}
+        if labels is None:
+            labels = [l["name"] for l in pr.get("labels", [])]
+        if body is None:
+            body = pr.get("body") or ""
+    if (labels is None or body is None) and args.pr:
+        info = json.loads(subprocess.check_output(["gh", "pr", "view", str(args.pr), "--json", "labels,body"], text=True))
+        if labels is None:
+            labels = [l["name"] for l in info["labels"]]
+        if body is None:
+            body = info["body"] or ""
+    return labels or [], body or "", event
+
+
+def check_paths(args, root):
+    labels, body, event = pr_context(args)
+    if event == "merge_group":
+        print("model-sync: merge queue run; the pull_request run already enforced the check")
+        return 0
+    config = load_map(root)
+    models = config["models"]
+    if args.files is not None:
+        changed, base, head = list(args.files), None, None
+    else:
+        head = args.head
+        try:
+            base = git(root, "merge-base", args.base or "origin/main", head).strip()
+        except subprocess.CalledProcessError:
+            print(f"model-sync: no merge base between {args.base or 'origin/main'} and {head}; fetch it or pass --base")
+            return 2
+        changed = git(root, "diff", "--name-only", "--no-renames", f"{base}...{head}").split()
+    model_changes = [p for p in changed
+                     if any(glob_match(p, g) for m in models.values() for g in m["files"])]
+    for p in model_changes:
+        if not model_file_changed(root, base, head, p):
+            print(f"note    {p}: comments only, does not count as a model update")
+    model_changes = [p for p in model_changes if model_file_changed(root, base, head, p)]
+    touched = {name for name, m in models.items()
+               if any(glob_match(p, g) for p in model_changes for g in m["files"])}
+    missing = {}
+    for path in changed:
+        covering = sorted(name for name, m in models.items() if any(glob_match(path, g) for g in m["code"]))
+        if not covering:
+            continue
+        if touched.intersection(covering):
+            print(f"ok      {path}: model updated ({', '.join(sorted(touched.intersection(covering)))})")
+            continue
+        kind = exempt_change(root, base, head, path) if base else None
+        if kind:
+            print(f"ok      {path}: {kind} only")
+            continue
+        missing[path] = covering
+    if not missing:
+        print("model-sync: every changed modelled file has its model updated (or is exempt)")
+        return 0
+    has_label = LABEL in labels
+    has_reason = bool(REASON.search(body))
+    for path, covering in missing.items():
+        print(f"{'waived' if has_label and has_reason else 'MISSING'} {path}: covered by {', '.join(covering)}, none changed")
+    if has_label and has_reason:
+        line = body[REASON.search(body).start():].strip().splitlines()[0]
+        print(f"model-sync: waived by the `{LABEL}` label and: {line}")
+        return 0
+    print(f"""
+model-sync: this PR changes modelled code without changing its model.
+Models track the code: update the model (verification/tla/) in this PR, or,
+if the behaviour the model specifies is unchanged, add the `{LABEL}` label
+AND a PR body line `Model: no change because <reason>`.
+Missing now: {'' if has_label else f'the `{LABEL}` label; '}{'' if has_reason else 'the `Model: no change because ...` line'}
+Mapping: {MAP}""")
+    return 1
+
+
+# --------------------------------------------------------------------------
+# events
+
+def spec_arms(text):
+    return set(re.findall(r"\be\.a\s*=\s*\"([A-Za-z0-9_]+)\"", text))
+
+
+def model_actions(model_text):
+    """Actions reachable from Next: expand operator references from Next,
+    stopping at an operator that is not a pure disjunction (its body primes
+    a variable, says UNCHANGED or has a conjunction)."""
+    model_text = re.sub(r"\(\*.*?\*\)", lambda m: re.sub(r"[^\n]", " ", m.group(0)), model_text, flags=re.S)
+    model_text = re.sub(r"\\\*[^\n]*", "", model_text)
+    defs = {}
+    for m in re.finditer(r"^([A-Za-z_]\w*)(?:\([^)]*\))?\s*==", model_text, re.M):
+        defs[m.group(1)] = m.end()
+    names = sorted(defs, key=defs.get)
+    bodies = {}
+    for k, name in enumerate(names):
+        end = len(model_text)
+        nxt = re.compile(r"^(?:[A-Za-z_]\w*(?:\([^)]*\))?\s*==|-{4,}|={4,}|\\\* )", re.M).search(model_text, defs[name])
+        if nxt:
+            end = nxt.start()
+        bodies[name] = model_text[defs[name]:end]
+    leaves, todo, seen = set(), ["Next"], set()
+    while todo:
+        name = todo.pop()
+        if name in seen or name not in bodies:
+            continue
+        seen.add(name)
+        body = bodies[name]
+        if name != "Next" and ("'" in body or "UNCHANGED" in body or "/\\" in body):
+            leaves.add(name)
+            continue
+        todo += [w for w in re.findall(r"\b[A-Za-z_]\w*\b", body) if w in bodies]
+    return leaves
+
+
+def check_events(args, root):
+    config = load_map(root)
+    trace_rs = (root / "concurrency/src/lifecycle_trace.rs").read_text()
+    structs = set(re.findall(r"pub struct (\w*Event)\b", trace_rs))
+    errors, warnings, notes = [], [], []
+    configured = {t["struct"] for t in config.get("trace", [])}
+    check_py = (root / "verification/tla/trace_check.py").read_text()
+    for s in sorted(structs - configured):
+        errors.append(f"event struct `{s}` in lifecycle_trace.rs has no [[trace]] table in {MAP}")
+    sources = {}
+    for path in sorted((root / "concurrency/src").rglob("*.rs")):
+        src = path.read_text()
+        sources[path.relative_to(root).as_posix()] = (src, *rust_mask(src))
+    for t in config.get("trace", []):
+        name = t["struct"]
+        if name not in structs:
+            notes.append(f"{name}: not in lifecycle_trace.rs yet, skipped")
+            continue
+        emitted = {}
+        for rel, (src, masked, strings) in sources.items():
+            done = set()
+            for e in t["emitters"]:
+                for m in re.finditer(e["call"], masked):
+                    if m.start() in done:
+                        continue
+                    done.add(m.start())
+                    if re.search(r"\bfn\s+\w*$", masked[max(0, m.start() - 20):m.start()]):
+                        continue
+                    line = masked.count("\n", 0, m.start()) + 1
+                    span = call_argument(masked, m.end() - 1, e["arg"])
+                    literals = action_values(masked, strings, *span) if span else None
+                    if not literals or not all(re.fullmatch(r"\w+", v) for v in literals):
+                        errors.append(f"{rel}:{line}: cannot tell which action `{m.group(0)}` records "
+                                      f"(pass a string literal or `if .. {{ \"A\" }} else {{ \"B\" }}`)")
+                        continue
+                    for v in literals:
+                        emitted.setdefault(v, []).append(f"{rel}:{line}")
+            # A struct literal setting the action field directly bypasses the emitters.
+            for m in re.finditer(r"\b%s\s*\{" % re.escape(name), masked):
+                before = masked[max(0, m.start() - 40):m.start()]
+                if rel == "concurrency/src/lifecycle_trace.rs" or re.search(r"(struct|impl|for|->|\blet|\bif let|\bwhile let|matches!\(\s*[\w.]+\s*,)\s*(\w+::)*$", before):
+                    continue
+                close = matching(masked, m.end() - 1)
+                if close is not None and re.match(r"\s*(=>|=[^=])", masked[close + 1:close + 4]):
+                    continue  # a pattern, not a construction
+                body = masked[m.end():close] if close else ""
+                if re.search(r"(^|[,{\s])action\s*[:,}]", body) or not close:
+                    line = masked.count("\n", 0, m.start()) + 1
+                    errors.append(f"{rel}:{line}: `{name} {{ .. }}` sets the action directly; build it with an emitter so the action can be checked")
+        specs = {}
+        for spec in t["specs"]:
+            path = root / spec
+            if not path.exists():
+                errors.append(f"{name}: trace spec {spec} does not exist")
+                continue
+            specs[spec] = path.read_text()
+        arms = {a: spec for spec, text in specs.items() for a in spec_arms(text)}
+        rejected = t.get("rejected", {})
+        translated = t.get("translated", {})
+        for action, sites in sorted(emitted.items()):
+            if action in arms:
+                continue
+            if action in rejected:
+                notes.append(f"{name}: `{action}` is rejected by design ({rejected[action]}); emitted at {', '.join(sites)}")
+            elif action in translated:
+                how = translated[action]
+                into = how.get("into", []) if isinstance(how, dict) else []
+                if f'"{action}"' not in check_py:
+                    errors.append(f"{name}: `{action}` is declared translated but trace_check.py never mentions it ({', '.join(sites)})")
+                for target in into:
+                    if target not in arms:
+                        errors.append(f"{name}: `{action}` is translated into `{target}`, which no spec arm replays")
+            else:
+                errors.append(f"{name}: event `{action}` (emitted at {', '.join(sites)}) is not mapped by {' or '.join(t['specs'])}")
+        produced = set(emitted)
+        for action, how in translated.items():
+            if action in emitted and isinstance(how, dict):
+                produced.update(how.get("into", []))
+        for action in sorted(set(arms) - produced):
+            warnings.append(f"{name}: {arms[action]} replays `{action}`, which no code emits")
+        for f in t.get("filters", []):
+            if not (root / f["file"]).exists():
+                errors.append(f"{name}: filter file {f['file']} does not exist")
+                continue
+            text = (root / f["file"]).read_text()
+            start = re.search(f["start"], text)
+            if not start:
+                errors.append(f"{name}: filter start `{f['start']}` not found in {f['file']}")
+                continue
+            end = re.compile(f["end"]).search(text, start.end())
+            listed = set(re.findall(r'"(\w+)"', text[start.end():end.start() if end else len(text)]))
+            want = spec_arms(specs.get(f["spec"], ""))
+            if listed != want:
+                errors.append(f"{name}: the event filter in {f['file']} differs from the arms of {f['spec']}: "
+                              f"missing {sorted(want - listed)}, extra {sorted(listed - want)}")
+        unlogged = t.get("unlogged", {})
+        for spec, text in specs.items():
+            ext = re.search(r"EXTENDS\s+([\w, ]+)", text)
+            model = next((m.strip() for m in ext.group(1).split(",") if (root / f"verification/tla/{m.strip()}.tla").exists()), None) if ext else None
+            if not model:
+                continue
+            refs = set(re.findall(r"\b[A-Za-z_]\w*\b", re.sub(r"\(\*.*?\*\)|\\\*[^\n]*", "", text, flags=re.S)))
+            for action in sorted(model_actions((root / f"verification/tla/{model}.tla").read_text()) - refs):
+                if action in unlogged:
+                    notes.append(f"{name}: {model} action `{action}` has no trace event by design ({unlogged[action]})")
+                else:
+                    warnings.append(f"{name}: {model} action `{action}` is never taken by {spec}: no trace can reach it")
+        print(f"{name}: {len(emitted)} event kinds emitted, {len(arms)} spec arms ({', '.join(t['specs'])})")
+    for n in notes:
+        print(f"note    {n}")
+    for w in warnings:
+        print(f"WARNING {w}")
+        if os.environ.get("GITHUB_ACTIONS"):
+            print(f"::warning title=model-sync events::{w}")
+    for e in errors:
+        print(f"ERROR   {e}")
+    if errors:
+        print(f"\nmodel-sync events: {len(errors)} error(s). Every event the code records must be replayed by its trace spec; see {MAP}.")
+        return 1
+    print("model-sync events: every emitted trace event is mapped")
+    return 0
+
+
+# --------------------------------------------------------------------------
+# models
+
+BASELINE = "verification/tla/coverage-baseline.json"
+
+
+def base_models(root):
+    """Models proper: verification/tla/*.tla minus MC*, Trace*, Cov*, *Ind and
+    *Coverage helper modules."""
+    names = []
+    for path in sorted((root / "verification/tla").glob("*.tla")):
+        name = path.stem
+        if re.match(r"(MC|Trace|Cov)[A-Z]", name) or name.endswith(("Ind", "Coverage")):
+            continue
+        names.append(name)
+    return names
+
+
+def trace_validation(root, config, model):
+    """(spec, mapped event kinds) of a trace spec that replays recorded Rust
+    events against `model`, or (None, reason)."""
+    check_py = (root / "verification/tla/trace_check.py").read_text()
+    trace_rs = (root / "concurrency/src/lifecycle_trace.rs").read_text()
+    structs = set(re.findall(r"pub struct (\w*Event)\b", trace_rs))
+    sources, reasons = None, []
+    for spec_path in sorted((root / "verification/tla").glob("Trace*.tla")):
+        text = spec_path.read_text()
+        ext = re.search(r"EXTENDS\s+([\w, ]+)", text)
+        if not ext or model not in [m.strip() for m in ext.group(1).split(",")]:
+            continue
+        rel = spec_path.relative_to(root).as_posix()
+        if spec_path.name not in check_py:
+            reasons.append(f"{rel} exists but trace_check.py never runs it")
+            continue
+        arms = spec_arms(text)
+        for t in config.get("trace", []):
+            if rel not in t["specs"] or t["struct"] not in structs:
+                continue
+            if sources is None:
+                sources = {p: rust_mask(p.read_text()) for p in (root / "concurrency/src").rglob("*.rs")}
+            emitted = set()
+            for masked, strings in sources.values():
+                for e in t["emitters"]:
+                    for m in re.finditer(e["call"], masked):
+                        span = call_argument(masked, m.end() - 1, e["arg"])
+                        emitted.update((action_values(masked, strings, *span) or []) if span else [])
+            for action, how in t.get("translated", {}).items():
+                if action in emitted and isinstance(how, dict):
+                    emitted.update(how.get("into", []))
+            mapped = emitted & arms
+            if mapped:
+                return rel, mapped
+        reasons.append(f"{rel} exists but no recorded event reaches it")
+    return None, "; ".join(reasons) or "no trace spec"
+
+
+def check_models(args, root):
+    config = load_map(root)
+    models = config["models"]
+    baseline_path = root / BASELINE
+    baseline = json.loads(baseline_path.read_text()) if baseline_path.exists() else {}
+    errors, warnings, rows, tlc_only = [], [], [], set()
+    for model in base_models(root):
+        entry = models.get(model)
+        if entry is None:
+            errors.append(f"model {model} has no [models.{model}] entry in {MAP} (which code does it cover?)")
+            continue
+        spec, detail = trace_validation(root, config, model)
+        allow = entry.get("tlc_only")
+        if spec:
+            status = f"trace-validated by {spec} ({len(detail)} event kinds)"
+            if allow:
+                warnings.append(f"{model} has trace validation now; remove its `tlc_only` allowlist entry")
+        elif allow:
+            tlc_only.add(model)
+            if not allow.get("reason") or not allow.get("tracking"):
+                errors.append(f"{model}: a `tlc_only` entry needs both `reason` and `tracking`")
+            status = f"TLC ONLY (allowlisted: {allow.get('reason', '?')}; tracking: {allow.get('tracking', '?')})"
+        else:
+            errors.append(f"{model} has no trace validation ({detail}): a model no real run is checked against can drift "
+                          f"from the code. Add a trace spec and recorded traces, or a [models.{model}.tlc_only] "
+                          f"entry with `reason` and `tracking`")
+            status = f"TLC ONLY, not allowlisted ({detail})"
+        floor = entry.get("coverage_floor")
+        key = entry.get("coverage_key", model)
+        if floor is not None:
+            covered = sum(1 for k in baseline.get(key, []) if k.startswith("A|"))
+            status += f"; covered action keys {covered} (floor {floor})"
+            if covered < floor:
+                errors.append(f"{model}: {BASELINE} covers {covered} action keys of {key}, below the floor {floor}. "
+                              f"Trace coverage may only grow: restore the lost tests, or lower `coverage_floor` "
+                              f"in {MAP} with a reason in the PR")
+            elif covered > floor:
+                warnings.append(f"{model}: coverage grew to {covered} action keys; raise `coverage_floor` to {covered}")
+        elif spec and key in baseline:
+            errors.append(f"{model}: trace-validated with a coverage baseline but no `coverage_floor` in {MAP}")
+        rows.append(f"{model:18} {status}")
+    for r in rows:
+        print(r)
+    for w in warnings:
+        print(f"WARNING {w}")
+        if os.environ.get("GITHUB_ACTIONS"):
+            print(f"::warning title=model-sync models::{w}")
+    for e in errors:
+        print(f"ERROR   {e}")
+    allowlisted = [m for m in base_models(root) if m in tlc_only]
+    if allowlisted:
+        print(f"\nTLC-only models (no trace validation; these can drift from the code): {', '.join(allowlisted)}")
+    if errors:
+        print(f"\nmodel-sync models: {len(errors)} error(s)")
+        return 1
+    print("model-sync models: every model is trace-validated or allowlisted, and no coverage floor is broken")
+    return 0
+
+
+def main(argv=None):
+    parser = argparse.ArgumentParser(description=__doc__.splitlines()[0])
+    sub = parser.add_subparsers(dest="command", required=True)
+    paths = sub.add_parser("paths")
+    paths.add_argument("--base", help="base revision (default: merge-base with origin/main)")
+    paths.add_argument("--head", default="HEAD")
+    paths.add_argument("--files", nargs="*", help="changed files instead of a git diff (no comment/test exemption)")
+    paths.add_argument("--labels", help="comma-separated PR labels")
+    paths.add_argument("--body", help="PR body")
+    paths.add_argument("--pr", type=int, help="read labels and body with gh")
+    sub.add_parser("events")
+    sub.add_parser("models")
+    parser.add_argument("--root", type=Path, default=ROOT)
+    args = parser.parse_args(argv)
+    if args.command == "paths":
+        return check_paths(args, args.root)
+    if args.command == "models":
+        return check_models(args, args.root)
+    return check_events(args, args.root)
+
+
+if __name__ == "__main__":
+    sys.exit(main())
diff --git a/scripts/tests/test_model_sync.py b/scripts/tests/test_model_sync.py
new file mode 100644
index 00000000..ab06e4d3
--- /dev/null
+++ b/scripts/tests/test_model_sync.py
@@ -0,0 +1,336 @@
+"""Self-tests for scripts/check-model-sync.py (paths, events, models) and
+the repository's own map."""
+import contextlib
+import importlib.util
+import io
+import json
+import os
+import shutil
+import subprocess
+import tempfile
+import unittest
+from pathlib import Path
+from unittest.mock import patch
+
+ROOT = Path(__file__).resolve().parents[2]
+spec = importlib.util.spec_from_file_location("check_model_sync", ROOT / "scripts" / "check-model-sync.py")
+sync = importlib.util.module_from_spec(spec)
+spec.loader.exec_module(sync)
+
+
+def run(*argv, env=None):
+    out = io.StringIO()
+    environ = {k: v for k, v in os.environ.items() if not k.startswith("GITHUB_")}
+    environ.update(env or {})
+    with patch.dict(os.environ, environ, clear=True), contextlib.redirect_stdout(out):
+        code = sync.main(list(argv))
+    return code, out.getvalue()
+
+
+class RepoCopy(unittest.TestCase):
+    def copy(self):
+        tmp = Path(tempfile.mkdtemp())
+        self.addCleanup(shutil.rmtree, tmp)
+        shutil.copytree(ROOT / "concurrency" / "src", tmp / "concurrency" / "src")
+        (tmp / "concurrency" / "tests").mkdir()
+        shutil.copy(ROOT / "concurrency" / "tests" / "cohort_trace.rs", tmp / "concurrency" / "tests")
+        shutil.copytree(ROOT / "verification", tmp / "verification")
+        return tmp
+
+
+class TraceEvents(RepoCopy):
+    def test_repository_events_are_mapped(self):
+        code, out = run("--root", str(ROOT), "events")
+        self.assertEqual(code, 0, out)
+
+    def inject(self, tmp, code):
+        path = tmp / "concurrency" / "src" / "supervision.rs"
+        path.write_text(path.read_text() + "\nfn injected() {\n" + code + "\n}\n")
+
+    def test_unmapped_event_fails(self):
+        tmp = self.copy()
+        self.inject(tmp, 'let _ = Event::new(\n    "BogusStep", 1, "");')
+        code, out = run("--root", str(tmp), "events")
+        self.assertEqual(code, 1, out)
+        self.assertIn("event `BogusStep`", out)
+
+    def test_unmapped_event_in_a_branch_fails(self):
+        tmp = self.copy()
+        self.inject(tmp, 'let _ = Event::new(if x { "Close" } else { "BogusBranch" }, 0, "");')
+        code, out = run("--root", str(tmp), "events")
+        self.assertEqual(code, 1, out)
+        self.assertIn("event `BogusBranch`", out)
+
+    def test_non_literal_action_fails(self):
+        tmp = self.copy()
+        self.inject(tmp, "let _ = Event::new(name, 0, \"\");")
+        code, out = run("--root", str(tmp), "events")
+        self.assertEqual(code, 1, out)
+        self.assertIn("cannot tell which action", out)
+
+    def test_partly_dynamic_action_fails(self):
+        tmp = self.copy()
+        self.inject(tmp, 'let _ = Event::new(if c { "Close" } else { name }, 0, "");')
+        code, out = run("--root", str(tmp), "events")
+        self.assertEqual(code, 1, out)
+        self.assertIn("cannot tell which action", out)
+
+    def test_action_from_a_call_fails(self):
+        tmp = self.copy()
+        self.inject(tmp, 'let _ = Event::new(helper("Close"), 0, "");')
+        code, out = run("--root", str(tmp), "events")
+        self.assertEqual(code, 1, out)
+        self.assertIn("cannot tell which action", out)
+
+    def test_destructuring_is_not_a_construction(self):
+        tmp = self.copy()
+        self.inject(tmp, 'let Event { action, .. } = ev;\nlet _ = matches!(e, Event { action: "X", .. });\nmatch e { Event { action, .. } => (), }')
+        code, out = run("--root", str(tmp), "events")
+        self.assertEqual(code, 0, out)
+
+    def test_struct_literal_setting_action_fails(self):
+        tmp = self.copy()
+        self.inject(tmp, 'let _ = Event { action: name, child: 0, arg: "", count: 0, round: 0 };')
+        code, out = run("--root", str(tmp), "events")
+        self.assertEqual(code, 1, out)
+        self.assertIn("sets the action directly", out)
+
+    def test_comments_and_strings_are_not_events(self):
+        tmp = self.copy()
+        self.inject(tmp, '// Event::new("InComment", 0, "")\nlet _ = "Event::new(\\"InString\\", 0, \\"\\")";')
+        code, out = run("--root", str(tmp), "events")
+        self.assertEqual(code, 0, out)
+
+    def test_unconfigured_event_struct_fails(self):
+        tmp = self.copy()
+        path = tmp / "concurrency" / "src" / "lifecycle_trace.rs"
+        path.write_text(path.read_text() + "\npub struct NewEvent { pub action: &'static str }\n")
+        code, out = run("--root", str(tmp), "events")
+        self.assertEqual(code, 1, out)
+        self.assertIn("`NewEvent`", out)
+
+    def test_cohort_filter_drift_fails(self):
+        tmp = self.copy()
+        path = tmp / "concurrency" / "src" / "lifecycle_trace.rs"
+        path.write_text(path.read_text().replace('"CDone",\n', "", 1))
+        code, out = run("--root", str(tmp), "events")
+        self.assertEqual(code, 1, out)
+        self.assertIn("missing ['CDone']", out)
+
+    def test_spec_arm_without_emitter_warns(self):
+        tmp = self.copy()
+        path = tmp / "verification" / "tla" / "TraceNested.tla"
+        path.write_text(path.read_text().replace(' [] OTHER -> FALSE', ' [] e.a = "TGhost" -> FALSE\n [] OTHER -> FALSE'))
+        code, out = run("--root", str(tmp), "events")
+        self.assertEqual(code, 0, out)
+        self.assertIn("replays `TGhost`, which no code emits", out)
+
+
+class ModelInventory(RepoCopy):
+    def test_repository_models_pass(self):
+        code, out = run("--root", str(ROOT), "models")
+        self.assertEqual(code, 0, out)
+        self.assertIn("TLC-only models", out)
+
+    def edit_map(self, tmp, old, new):
+        path = tmp / "verification" / "model-map.toml"
+        text = path.read_text()
+        self.assertIn(old, text)
+        path.write_text(text.replace(old, new, 1))
+
+    def test_unmapped_model_fails(self):
+        tmp = self.copy()
+        (tmp / "verification" / "tla" / "Brand.tla").write_text("---- MODULE Brand ----\n====\n")
+        code, out = run("--root", str(tmp), "models")
+        self.assertEqual(code, 1, out)
+        self.assertIn("model Brand has no [models.Brand] entry", out)
+
+    def test_tlc_only_model_without_allowlist_fails(self):
+        tmp = self.copy()
+        self.edit_map(tmp, "[models.Coordinator.tlc_only]", "[models.Coordinator.not_allowlisted]")
+        code, out = run("--root", str(tmp), "models")
+        self.assertEqual(code, 1, out)
+        self.assertIn("Coordinator has no trace validation", out)
+
+    def test_allowlist_needs_tracking(self):
+        tmp = self.copy()
+        self.edit_map(tmp, 'tracking = "work item to be filed', 'untracked = "work item to be filed')
+        code, out = run("--root", str(tmp), "models")
+        self.assertEqual(code, 1, out)
+        self.assertIn("needs both `reason` and `tracking`", out)
+
+    def test_unrun_trace_spec_is_not_validation(self):
+        tmp = self.copy()
+        path = tmp / "verification" / "tla" / "trace_check.py"
+        path.write_text(path.read_text().replace("TraceNested.tla", "TraceTree.tla"))
+        code, out = run("--root", str(tmp), "models")
+        self.assertEqual(code, 1, out)
+        self.assertIn("NestedSupervision has no trace validation", out)
+
+    def test_second_trace_spec_can_validate(self):
+        tmp = self.copy()
+        (tmp / "verification" / "tla" / "TraceAaNested.tla").write_text(
+            "---- MODULE TraceAaNested ----\nEXTENDS NestedSupervision\n====\n")
+        code, out = run("--root", str(tmp), "models")
+        self.assertEqual(code, 0, out)
+
+    def test_coverage_below_floor_fails(self):
+        tmp = self.copy()
+        path = tmp / "verification" / "tla" / "coverage-baseline.json"
+        data = json.loads(path.read_text())
+        data["Supervision"] = data["Supervision"][1:]
+        path.write_text(json.dumps(data))
+        code, out = run("--root", str(tmp), "models")
+        self.assertEqual(code, 1, out)
+        self.assertIn("below the floor 36", out)
+
+
+ACTOR_CLEANUP = """//! Shared terminal publication.
+pub fn publish(x: u32) -> u32 {
+    x + 1
+}
+
+#[cfg(test)]
+mod tests {
+    #[test]
+    fn publishes() {
+        assert_eq!(super::publish(1), 2);
+    }
+}
+"""
+
+
+class ModelPaths(unittest.TestCase):
+    def setUp(self):
+        self.repo = Path(tempfile.mkdtemp())
+        self.addCleanup(shutil.rmtree, self.repo)
+        (self.repo / "verification" / "tla").mkdir(parents=True)
+        (self.repo / "concurrency" / "src").mkdir(parents=True)
+        shutil.copy(ROOT / "verification" / "model-map.toml", self.repo / "verification")
+        self.write("verification/tla/Lifecycle.tla", "---- MODULE Lifecycle ----\n====\n")
+        self.write("concurrency/src/actor_cleanup.rs", ACTOR_CLEANUP)
+        self.write("concurrency/src/registry.rs", "pub fn lookup() {}\n")
+        self.git("init", "-q")
+        self.git("add", "-A")
+        self.git("-c", "user.name=t", "-c", "user.email=t@t", "commit", "-qm", "base")
+        self.base = self.git("rev-parse", "HEAD").strip()
+
+    def git(self, *args):
+        return subprocess.run(["git", *args], cwd=self.repo, check=True, capture_output=True, text=True).stdout
+
+    def write(self, rel, text):
+        (self.repo / rel).write_text(text)
+
+    def edit(self, rel, old, new):
+        path = self.repo / rel
+        text = path.read_text()
+        self.assertIn(old, text)
+        path.write_text(text.replace(old, new, 1))
+
+    def check(self, labels="", body="", env=None):
+        self.git("add", "-A")
+        self.git("-c", "user.name=t", "-c", "user.email=t@t", "commit", "-qm", "change", "--allow-empty")
+        return run("--root", str(self.repo), "paths", "--base", self.base, "--labels", labels, "--body", body, env=env)
+
+    def test_code_change_without_model_fails(self):
+        self.edit("concurrency/src/actor_cleanup.rs", "x + 1", "x + 2")
+        code, out = self.check()
+        self.assertEqual(code, 1, out)
+        self.assertIn("MISSING concurrency/src/actor_cleanup.rs: covered by Lifecycle", out)
+
+    def test_code_change_with_model_passes(self):
+        self.edit("concurrency/src/actor_cleanup.rs", "x + 1", "x + 2")
+        self.edit("verification/tla/Lifecycle.tla", "====", "Step == TRUE\n====")
+        code, out = self.check()
+        self.assertEqual(code, 0, out)
+
+    def test_comment_only_model_change_does_not_count(self):
+        self.edit("concurrency/src/actor_cleanup.rs", "x + 1", "x + 2")
+        self.edit("verification/tla/Lifecycle.tla", "====", "\\* updated\n(* also *)\n====")
+        code, out = self.check()
+        self.assertEqual(code, 1, out)
+        self.assertIn("comments only, does not count", out)
+
+    def test_removing_cfg_test_is_not_exempt(self):
+        self.edit("concurrency/src/actor_cleanup.rs", "#[cfg(test)]\n", "")
+        code, out = self.check()
+        self.assertEqual(code, 1, out)
+
+    def test_moving_code_into_test_module_is_not_exempt(self):
+        self.edit("concurrency/src/actor_cleanup.rs", "pub fn publish(x: u32) -> u32 {\n    x + 1\n}\n", "")
+        self.edit("concurrency/src/actor_cleanup.rs", "mod tests {\n", "mod tests {\n    pub fn publish(x: u32) -> u32 {\n        x + 1\n    }\n")
+        code, out = self.check()
+        self.assertEqual(code, 1, out)
+
+    def test_label_and_reason_waive(self):
+        self.edit("concurrency/src/actor_cleanup.rs", "x + 1", "x + 2")
+        code, out = self.check("no-model-change", "Refactor.\n\nModel: no change because the publication order is unchanged.\n")
+        self.assertEqual(code, 0, out)
+        self.assertIn("waived", out)
+
+    def test_label_alone_does_not_waive(self):
+        self.edit("concurrency/src/actor_cleanup.rs", "x + 1", "x + 2")
+        code, out = self.check("no-model-change", "Refactor.")
+        self.assertEqual(code, 1, out)
+
+    def test_reason_alone_does_not_waive(self):
+        self.edit("concurrency/src/actor_cleanup.rs", "x + 1", "x + 2")
+        code, out = self.check("", "Model: no change because nothing changed.")
+        self.assertEqual(code, 1, out)
+
+    def test_template_placeholder_is_not_a_reason(self):
+        self.edit("concurrency/src/actor_cleanup.rs", "x + 1", "x + 2")
+        code, out = self.check("no-model-change", "Model: no change because <reason>")
+        self.assertEqual(code, 1, out)
+
+    def test_comment_only_change_passes(self):
+        self.edit("concurrency/src/actor_cleanup.rs", "//! Shared terminal publication.", "//! Shared terminal publication,\n//! for futures and threads.")
+        code, out = self.check()
+        self.assertEqual(code, 0, out)
+        self.assertIn("comments only", out)
+
+    def test_test_module_change_passes(self):
+        self.edit("concurrency/src/actor_cleanup.rs", "assert_eq!(super::publish(1), 2);", "assert_eq!(super::publish(1), 2);\n        assert_eq!(super::publish(2), 3);")
+        code, out = self.check()
+        self.assertEqual(code, 0, out)
+        self.assertIn("tests only", out)
+
+    def test_code_and_test_change_fails(self):
+        self.edit("concurrency/src/actor_cleanup.rs", "x + 1", "x + 2")
+        self.edit("concurrency/src/actor_cleanup.rs", "publish(1), 2", "publish(1), 3")
+        code, out = self.check()
+        self.assertEqual(code, 1, out)
+
+    def test_unmapped_code_passes(self):
+        self.edit("concurrency/src/registry.rs", "{}", "{ let _ = 1; }")
+        code, out = self.check()
+        self.assertEqual(code, 0, out)
+
+    def test_merge_queue_passes(self):
+        self.edit("concurrency/src/actor_cleanup.rs", "x + 1", "x + 2")
+        code, out = self.check(env={"GITHUB_EVENT_NAME": "merge_group"})
+        self.assertEqual(code, 0, out)
+
+    def test_actions_event_payload(self):
+        self.edit("concurrency/src/actor_cleanup.rs", "x + 1", "x + 2")
+        event = self.repo / "event.json"
+        event.write_text('{"pull_request": {"labels": [{"name": "no-model-change"}], "body": "Model: no change because tests."}}')
+        self.git("add", "-A")
+        self.git("-c", "user.name=t", "-c", "user.email=t@t", "commit", "-qm", "change")
+        code, out = run("--root", str(self.repo), "paths", "--base", self.base,
+                        env={"GITHUB_EVENT_NAME": "pull_request", "GITHUB_EVENT_PATH": str(event)})
+        self.assertEqual(code, 0, out)
+
+
+class TomlSubset(unittest.TestCase):
+    def test_fallback_parser_matches_tomllib(self):
+        try:
+            import tomllib
+        except ImportError:
+            self.skipTest("tomllib needs Python 3.11")
+        text = (ROOT / "verification" / "model-map.toml").read_text()
+        self.assertEqual(sync.parse_toml(text), tomllib.loads(text))
+
+
+if __name__ == "__main__":
+    unittest.main()
diff --git a/verification/model-map.toml b/verification/model-map.toml
new file mode 100644
index 00000000..315c6ada
--- /dev/null
+++ b/verification/model-map.toml
@@ -0,0 +1,241 @@
+# Which TLA+ models cover which code, read by scripts/check-model-sync.py.
+#
+# Rule: models track the code. A PR that changes a file listed under a
+# model's `code` must also change one of the `files` of at least one model
+# covering it (the model, its MC configurations, inductive/coverage modules
+# or trace spec); one covering model is enough, and a comment-only model
+# change does not count. Otherwise the PR needs the `no-model-change` label and a
+# body line `Model: no change because <reason>`. Changes to comments only,
+# or only inside a `#[cfg(test)] mod` block, are exempt. Globs: `*` stays
+# within a path segment, `**` crosses segments. Paths that do not exist yet
+# (code still on an open PR) are harmless.
+#
+# Every model in verification/tla needs an entry here, and either trace
+# validation (a Trace*.tla spec that trace_check.py runs against events the
+# code records) or a `tlc_only` allowlist entry with a reason and a tracking
+# item: a model no real run is checked against can drift from the code.
+# `coverage_floor` is the number of action keys (`A|...`) the dedicated trace
+# tests cover in verification/tla/coverage-baseline.json (key
+# `coverage_key`, default the model name); it may only go up.
+
+[models.Supervision]
+# OneForOne: run_supervisor/run_child, restart table, budget, ordered start,
+# reverse shutdown, deadlines, cleanup-stuck failures.
+files = [
+    "verification/tla/Supervision.tla",
+    "verification/tla/SupervisionInd.tla",
+    "verification/tla/SupervisionCoverage.tla",
+    "verification/tla/MCSupervision*",
+    "verification/tla/TraceSupervision.tla",
+    "verification/tla/CovSupervision.tla",
+    "verification/tla/CovTraceSupervision.tla",
+]
+code = [
+    "concurrency/src/supervision.rs",
+    "concurrency/src/supervision/**",
+    "concurrency/src/lifecycle_trace.rs",
+]
+coverage_floor = 36   # of 40 action keys
+
+[models.Cohorts]
+# OneForAll/RestForOne rounds (selection, stop, cleanup, join barrier,
+# resume, supersession, retirement), in supervision.rs.
+files = [
+    "verification/tla/Cohorts.tla",
+    "verification/tla/CohortsInd.tla",
+    "verification/tla/CohortsCoverage.tla",
+    "verification/tla/MCCohorts*",
+    "verification/tla/TraceCohorts.tla",
+    "verification/tla/CovCohorts.tla",
+    "verification/tla/CovTraceCohorts.tla",
+]
+code = [
+    "concurrency/src/supervision.rs",
+    "concurrency/src/supervision/**",
+    "concurrency/src/lifecycle_trace.rs",
+]
+coverage_floor = 40   # of 46 action keys
+
+[models.NestedSupervision]
+# Subtree ownership, attachment, parent join after descendants, shutdown
+# propagation: supervision.rs (TBegin..TDone) and supervision/nested.rs.
+files = [
+    "verification/tla/NestedSupervision.tla",
+    "verification/tla/NestedSupervisionInd.tla",
+    "verification/tla/NestedCoverage.tla",
+    "verification/tla/MCNested*",
+    "verification/tla/TraceNested.tla",
+    "verification/tla/CovNested.tla",
+    "verification/tla/CovTraceNested.tla",
+]
+code = [
+    "concurrency/src/supervision.rs",
+    "concurrency/src/supervision/**",
+    "concurrency/src/lifecycle_trace.rs",
+]
+coverage_key = "Nested"
+coverage_floor = 11   # of 11 observable action keys (Deliver has no event)
+
+[models.Coordinator]
+# ActorSystem::begin_shutdown: ordered stop of admitted roots, emergency
+# fallback, failure recording, runtime ownership. Execution groups
+# (system/group.rs) are explicitly outside the model.
+files = [
+    "verification/tla/Coordinator.tla",
+    "verification/tla/CoordinatorInd.tla",
+    "verification/tla/MCCoordinator*",
+]
+code = [
+    "concurrency/src/system.rs",
+]
+[models.Coordinator.tlc_only]
+reason = "abstract fault model of begin_shutdown; no coordinator events are recorded, so no real run is replayed against it"
+tracking = "work item to be filed from the model-sync inventory (PR #260)"
+
+[models.Lifecycle]
+# Base actor lifecycle: phases and the death point, request admission and
+# answers around death, dispatch after stop (#182, #185), links, monitors,
+# trap_exit, exit signals, administrative stops (ChildHandle), Exit/Down
+# ordering, terminal publication.
+files = [
+    "verification/tla/Lifecycle.tla",
+    "verification/tla/MCLifecycle*",
+    "verification/tla/TraceLifecycle.tla",
+]
+code = [
+    "concurrency/src/actor_cleanup.rs",
+    "concurrency/src/tasks/actor.rs",
+    "concurrency/src/threads/actor.rs",
+    "concurrency/src/link.rs",
+    "concurrency/src/monitor.rs",
+    "concurrency/src/child_handle.rs",
+    "concurrency/src/mailbox.rs",
+    "concurrency/src/mailbox_admission.rs",
+    "concurrency/src/lifecycle_trace.rs",
+]
+[models.Lifecycle.tlc_only]
+reason = "models the proposed v0.8 exit-signal contract; the code on main is v0.7, so there are no lifecycle trace events yet"
+tracking = "PR #240 adds LifeEvent and TraceLifecycle.tla; remove this entry once it merges"
+
+[models.DeferredReplies]
+# Rank 11: reply slots, deadlines, deferral credits, owner exit and death.
+files = [
+    "verification/tla/DeferredReplies.tla",
+    "verification/tla/MCDeferredReplies*",
+    "verification/tla/TraceReplies.tla",
+]
+code = [
+    "concurrency/src/reply/**",
+    "concurrency/src/lifecycle_trace.rs",
+]
+[models.DeferredReplies.tlc_only]
+reason = "rank 11 design model; the implementation is not on main yet"
+tracking = "PR #240 adds reply events and TraceReplies.tla; remove this entry once it merges"
+
+[models.DeferredJobs]
+# Rank 11: pipe jobs, keyed replacement, ActorId and cancellation fencing,
+# emit credits, terminal message last.
+files = [
+    "verification/tla/DeferredJobs.tla",
+    "verification/tla/MCDeferredJobs*",
+    "verification/tla/TraceJobs.tla",
+]
+code = [
+    "concurrency/src/reply/**",
+    "concurrency/src/tasks/jobs.rs",
+    "concurrency/src/threads/jobs.rs",
+    "concurrency/src/lifecycle_trace.rs",
+]
+[models.DeferredJobs.tlc_only]
+reason = "rank 11 design model; the implementation is not on main yet"
+tracking = "PR #240 adds JobEvent and TraceJobs.tla; remove this entry once it merges"
+
+[models.DynamicSupervisor]
+# Rank 12a design model (PR #245); no code yet.
+files = [
+    "verification/tla/DynamicSupervisor*.tla",
+    "verification/tla/MCDynamicSupervisor*",
+    "verification/tla/TraceDynamicSupervisor.tla",
+]
+code = []
+[models.DynamicSupervisor.tlc_only]
+reason = "rank 12a design model; the dynamic supervisor is not implemented"
+tracking = "trace validation is part of implementing rank 12a (design: PR #245)"
+
+# Trace events. Each [[trace]] table names one event struct of
+# concurrency/src/lifecycle_trace.rs, the calls that create one (a regex
+# matched in concurrency/src, and the 0-based index of the argument holding
+# the action name) and the trace specs that replay it. Every action string
+# the code can pass must be one of:
+#   - a `e.a = "..."` arm of one of the specs;
+#   - `translated`: rewritten by trace_check.py (which must mention it) into
+#     the spec arms listed in `into`;
+#   - `rejected`: the spec rejects it on purpose.
+# Every `*Event` struct in lifecycle_trace.rs needs a table; a table whose
+# struct does not exist yet is skipped. `unlogged` lists model actions with
+# no event by design (others are reported as warnings).
+
+[[trace]]
+struct = "Event"
+emitters = [
+    { call = '\bEvent::new\(', arg = 0 },
+    { call = '\bEvent::sup\(', arg = 0 },
+]
+specs = [
+    "verification/tla/TraceSupervision.tla",
+    "verification/tla/TraceCohorts.tla",
+]
+# Cohort tapes keep only these events; both lists must equal the arms of
+# TraceCohorts.tla.
+[[trace.filters]]
+spec = "verification/tla/TraceCohorts.tla"
+file = "concurrency/src/lifecycle_trace.rs"
+start = 'const COHORT_EVENTS'
+end = '\];'
+[[trace.filters]]
+spec = "verification/tla/TraceCohorts.tla"
+file = "concurrency/tests/cohort_trace.rs"
+start = 'matches!\(\s*event\.action,'
+end = '\)'
+[trace.rejected]
+Unmodelled = "placement failure, execution-group closure, controller and coordinator panics: outside Supervision.tla, so the trace is rejected"
+[trace.unlogged]
+WindowExpire = "the rolling restart window has no observable event; TraceSupervision stutters it before BackoffDone/RetryReserve"
+
+[[trace]]
+struct = "TreeEvent"
+emitters = [
+    { call = '\bTreeEvent::new\(', arg = 0 },
+]
+specs = ["verification/tla/TraceNested.tla"]
+[trace.unlogged]
+Deliver = "fairness device for shutdown delivery, no trace event (see README, Trace coverage)"
+
+# Added by the exit-signals and deferred-replies work (PR #240); skipped
+# until the structs exist.
+[[trace]]
+struct = "LifeEvent"
+emitters = [
+    { call = '\bLifeEvent::new\(', arg = 0 },
+]
+specs = ["verification/tla/TraceLifecycle.tla"]
+[trace.rejected]
+Held = "a signal held while started() runs (phase 0) is outside Lifecycle.tla; the trace is rejected"
+[trace.translated]
+Spawn = { into = [], why = "trace_check.py numbers actors from Spawn events" }
+Send = { into = ["Request", "Enqueue"], why = "trace_check.py splits Send into Request and Enqueue" }
+
+[[trace]]
+struct = "JobEvent"
+emitters = [
+    { call = '\bJobEvent::new\(', arg = 0 },
+]
+specs = ["verification/tla/TraceJobs.tla"]
+
+[[trace]]
+struct = "ReplyEvent"
+emitters = [
+    { call = '\blifecycle_trace::reply\(', arg = 1 },
+    { call = '\btrace::reply\(', arg = 1 },
+]
+specs = ["verification/tla/TraceReplies.tla"]
diff --git a/verification/tla/README.md b/verification/tla/README.md
index c4d28fe5..6425df78 100644
--- a/verification/tla/README.md
+++ b/verification/tla/README.md
@@ -107,6 +107,29 @@ child), and a trace edited back to failing the tree is a negative control. Hand-
 before an `Attempt`, a restart after a Transient normal exit, forward shutdown
 order, budget exhaustion with a free retry) are rejected at the edited event.
 
+## Model sync
+
+Models track the code. A PR that changes modelled behaviour updates the model
+in the same PR; the `model-sync` CI job enforces it
+([details](../../docs/TESTING.md#model-sync)):
+
+- `verification/model-map.toml` lists, per model, its files here (model, MC
+  configurations, `*Ind`, coverage and trace modules) and the code it covers.
+  A PR changing covered code without touching any covering model fails,
+  unless the change is comments or `#[cfg(test)]` only, or the PR has the
+  `no-model-change` label and a body line `Model: no change because <reason>`.
+- `scripts/check-model-sync.py events` checks that every trace event the
+  code can emit is an arm of its trace spec (`TraceSupervision`,
+  `TraceCohorts`, `TraceNested`), or is declared translated or rejected in
+  the map. It warns about arms no code emits and model actions no trace spec
+  takes. When adding an event or an action, update the spec and the map.
+- `scripts/check-model-sync.py models` requires every model here to be in
+  the map and to have a trace spec (a `Trace*.tla` named in
+  `trace_check.py` whose arms emitted events reach), or a `tlc_only`
+  allowlist entry with a reason and a tracking item. It also keeps each
+  model's covered action keys in `coverage-baseline.json` at or above its
+  `coverage_floor`. It prints the TLC-only models.
+
 ## Trace coverage
 
 Trace validation says every recorded run is a behavior of the model. Trace