From c17f62893e8f9dee5da94eeef44bf11a64c81330 Mon Sep 17 00:00:00 2001
From: Federico Carrone <mail@fcarrone.com>
Date: Wed, 11 Nov 2026 13:22:07 -0300
Subject: [PATCH 1/7] docs: changelog entry for model-sync checks

---
 CHANGELOG.md | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 676edf3b..307fa35b 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -26,6 +26,11 @@
   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; a test checks that every lifecycle trace event kind maps to a
+  trace-spec action.
 - 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

From ab1cf7e90118d413e576fa036ece649ec95fcf3e Mon Sep 17 00:00:00 2001
From: Federico Carrone <mail@fcarrone.com>
Date: Wed, 11 Nov 2026 13:30:55 -0300
Subject: [PATCH 2/7] ci: model map and model-sync checks (paths, trace events)

---
 scripts/check-model-sync.py      | 564 +++++++++++++++++++++++++++++++
 scripts/tests/test_model_sync.py | 229 +++++++++++++
 verification/model-map.toml      | 202 +++++++++++
 3 files changed, 995 insertions(+)
 create mode 100755 scripts/check-model-sync.py
 create mode 100644 scripts/tests/test_model_sync.py
 create mode 100644 verification/model-map.toml

diff --git a/scripts/check-model-sync.py b/scripts/check-model-sync.py
new file mode 100755
index 00000000..37b22ba3
--- /dev/null
+++ b/scripts/check-model-sync.py
@@ -0,0 +1,564 @@
+#!/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 [--root DIR]
+
+`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.
+
+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:
+            i = m.end()
+            if m.end() == m.start():
+                i += 1
+    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)
+                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 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 exempt_change(root, base, head, path):
+    """'comments' or 'tests' if every changed line of path is a comment line
+    or inside a #[cfg(test)] module (on its side of the diff), else None."""
+    diff = git(root, "diff", "-U0", "--no-color", "--no-ext-diff", f"{base}...{head}", "--", path)
+    old_tests = test_module_lines(show(root, base, path)) if path.endswith(".rs") else []
+    new_tests = test_module_lines(show(root, head, path)) if path.endswith(".rs") else []
+    within = lambda line, ranges: any(a <= line <= b for a, b in ranges)
+    kinds = set()
+    old_line = new_line = 0
+    seen = False
+    for line in diff.splitlines():
+        hunk = re.match(r"@@ -(\d+)(?:,\d+)? \+(\d+)(?:,\d+)? @@", line)
+        if hunk:
+            old_line, new_line = int(hunk.group(1)), int(hunk.group(2))
+            continue
+        if line.startswith(("+++", "---", "diff ", "index ", "new file", "deleted file", "similarity", "rename", "old mode", "new mode", "Binary")):
+            if line.startswith("Binary"):
+                return None
+            continue
+        if line.startswith("\\"):
+            continue
+        if line[:1] not in "+-":
+            continue
+        seen = True
+        text = line[1:].strip()
+        number = new_line if line[0] == "+" else old_line
+        if line[0] == "+":
+            new_line += 1
+        else:
+            old_line += 1
+        if text == "" or text.startswith("//"):
+            kinds.add("comments")
+        elif within(number, new_tests if line[0] == "+" else old_tests):
+            kinds.add("tests")
+        else:
+            return None
+    if not seen:
+        return "comments"  # mode change or no content change
+    return "tests" if "tests" in kinds else "comments"
+
+
+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
+        base = args.base or git(root, "merge-base", "origin/main", head).strip()
+        changed = git(root, "diff", "--name-only", "--no-renames", f"{base}...{head}").split()
+    touched = {name for name, m in models.items()
+               if any(glob_match(p, g) for p in changed 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:
+        print(f"model-sync: waived by the `{LABEL}` label and: {REASON.search(body).group(0).strip()}...")
+        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", [])}
+    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 = [v for k, v in strings.items() if span and span[0] <= k < span[1]]
+                    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 (use string literals)")
+                        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):
+                if rel == "concurrency/src/lifecycle_trace.rs" or re.search(r"(struct|impl|for)\s+$", masked[max(0, m.start() - 8):m.start()]):
+                    continue
+                close = matching(masked, m.end() - 1)
+                body = masked[m.end():close] if close else ""
+                if re.search(r"(^|[,{\s])(action|a)\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", {})
+        check_py = (root / "verification/tla/trace_check.py").read_text()
+        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", []):
+            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
+
+
+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")
+    events = sub.add_parser("events")
+    parser.add_argument("--root", type=Path, default=ROOT)
+    args = parser.parse_args(argv)
+    if args.command == "paths":
+        return check_paths(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..3d3478cc
--- /dev/null
+++ b/scripts/tests/test_model_sync.py
@@ -0,0 +1,229 @@
+"""Self-tests for scripts/check-model-sync.py (both checks) and the
+repository's own trace event mapping."""
+import contextlib
+import importlib.util
+import io
+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 TraceEvents(unittest.TestCase):
+    def test_repository_events_are_mapped(self):
+        code, out = run("--root", str(ROOT), "events")
+        self.assertEqual(code, 0, out)
+
+    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
+
+    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_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)
+
+
+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", "====", "\\* updated\n====")
+        code, out = self.check()
+        self.assertEqual(code, 0, 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..8a0a8359
--- /dev/null
+++ b/verification/model-map.toml
@@ -0,0 +1,202 @@
+# 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). 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.
+
+[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/lifecycle_trace.rs",
+]
+
+[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/lifecycle_trace.rs",
+]
+
+[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",
+]
+
+[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.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.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.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",
+]
+
+# 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"]

From 4a8710952d9617452a282859a7307370509e86b2 Mon Sep 17 00:00:00 2001
From: Federico Carrone <mail@fcarrone.com>
Date: Wed, 11 Nov 2026 13:31:52 -0300
Subject: [PATCH 3/7] ci: model-sync workflow and docs (models track the code)

---
 .github/workflows/model-sync.yml | 40 ++++++++++++++++++++++++++++++++
 ROADMAP.md                       |  7 ++++++
 docs/TESTING.md                  | 36 ++++++++++++++++++++++++++++
 verification/tla/README.md       | 17 ++++++++++++++
 4 files changed, 100 insertions(+)
 create mode 100644 .github/workflows/model-sync.yml

diff --git a/.github/workflows/model-sync.yml b/.github/workflows/model-sync.yml
new file mode 100644
index 00000000..e2e03b57
--- /dev/null
+++ b/.github/workflows/model-sync.yml
@@ -0,0 +1,40 @@
+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.
+# 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
+      # 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/ROADMAP.md b/ROADMAP.md
index 8eeff166..ec4466fc 100644
--- a/ROADMAP.md
+++ b/ROADMAP.md
@@ -318,6 +318,13 @@ 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), and every lifecycle trace event must be replayed by its
+trace spec ([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..46b583bd 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 | `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,41 @@ 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 two 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), the job fails. Changes to
+  comments only, or only inside a `#[cfg(test)] mod` block, are 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: the PR run enforced it.
+- **Trace events.** Every action name the code can record with the
+  `lifecycle-trace` feature (each string literal passed to `Event::new`,
+  `Event::sup`, `TreeEvent::new` and, with PR #240, `LifeEvent`, `JobEvent`
+  and reply events) 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+.
+
+```bash
+python3 scripts/check-model-sync.py events
+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/verification/tla/README.md b/verification/tla/README.md
index c4d28fe5..996fc77d 100644
--- a/verification/tla/README.md
+++ b/verification/tla/README.md
@@ -107,6 +107,23 @@ 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.
+
 ## Trace coverage
 
 Trace validation says every recorded run is a behavior of the model. Trace

From b2bc53bd6f40ff0bf529501b99ebd94c8c075f4d Mon Sep 17 00:00:00 2001
From: Federico Carrone <mail@fcarrone.com>
Date: Wed, 11 Nov 2026 13:32:14 -0300
Subject: [PATCH 4/7] ci: print the full waiver reason

---
 scripts/check-model-sync.py | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/scripts/check-model-sync.py b/scripts/check-model-sync.py
index 37b22ba3..e7a88b9c 100755
--- a/scripts/check-model-sync.py
+++ b/scripts/check-model-sync.py
@@ -376,7 +376,8 @@ def check_paths(args, root):
     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:
-        print(f"model-sync: waived by the `{LABEL}` label and: {REASON.search(body).group(0).strip()}...")
+        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.

From 94d928005da76f8deea02d0148ae4370aa529986 Mon Sep 17 00:00:00 2001
From: Federico Carrone <mail@fcarrone.com>
Date: Wed, 11 Nov 2026 13:35:23 -0300
Subject: [PATCH 5/7] ci: model inventory check (trace validation or allowlist)
 and coverage floors

---
 .github/workflows/model-sync.yml |   5 +-
 CHANGELOG.md                     |   6 +-
 ROADMAP.md                       |   7 +-
 docs/TESTING.md                  |  17 ++++-
 scripts/check-model-sync.py      | 127 ++++++++++++++++++++++++++++++-
 scripts/tests/test_model_sync.py |  65 ++++++++++++++--
 verification/model-map.toml      |  36 +++++++++
 verification/tla/README.md       |   6 ++
 8 files changed, 256 insertions(+), 13 deletions(-)

diff --git a/.github/workflows/model-sync.yml b/.github/workflows/model-sync.yml
index e2e03b57..7655ad00 100644
--- a/.github/workflows/model-sync.yml
+++ b/.github/workflows/model-sync.yml
@@ -2,7 +2,8 @@ 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.
+# 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:
@@ -33,6 +34,8 @@ jobs:
         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
diff --git a/CHANGELOG.md b/CHANGELOG.md
index 307fa35b..23c2cf9a 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -29,8 +29,10 @@
 - 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; a test checks that every lifecycle trace event kind maps to a
-  trace-spec action.
+  <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 ec4466fc..b5a27f68 100644
--- a/ROADMAP.md
+++ b/ROADMAP.md
@@ -322,8 +322,11 @@ 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), and every lifecycle trace event must be replayed by its
-trace spec ([model sync](docs/TESTING.md#model-sync)).
+<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`,
diff --git a/docs/TESTING.md b/docs/TESTING.md
index 46b583bd..5878d77b 100644
--- a/docs/TESTING.md
+++ b/docs/TESTING.md
@@ -114,7 +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 | `model-sync` job on every PR. See [model sync](#model-sync) |
+| 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 |
@@ -1153,9 +1153,24 @@ updates the model in the same PR, and drift is a bug. The `model-sync` job
   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 checked against real runs.** Every model in `verification/tla`
+  needs a map entry and trace validation: a `Trace*.tla` spec that
+  `trace_check.py` runs and that recorded events reach. 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. Today that
+  list is `Coordinator` (abstract fault model, no events recorded) and
+  `Lifecycle`, `DeferredReplies` and `DeferredJobs` (their trace validation
+  comes with PR #240), plus `DynamicSupervisor` once PR #245 lands.
+- **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
diff --git a/scripts/check-model-sync.py b/scripts/check-model-sync.py
index e7a88b9c..836c0bad 100755
--- a/scripts/check-model-sync.py
+++ b/scripts/check-model-sync.py
@@ -3,7 +3,8 @@
 
     check-model-sync.py paths [--base REF] [--head REF] [--files PATH...]
                               [--labels L,...] [--body TEXT] [--pr N]
-    check-model-sync.py events [--root DIR]
+    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
@@ -20,6 +21,12 @@
 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).
 """
@@ -543,6 +550,119 @@ def check_events(args, root):
     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 = 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:
+            return None, f"{rel} exists but trace_check.py never runs it"
+        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(v for k, v in strings.items() if span and span[0] <= k < span[1])
+            for how in t.get("translated", {}).values():
+                if isinstance(how, dict):
+                    emitted.update(how.get("into", []))
+            mapped = emitted & arms
+            if mapped:
+                return rel, mapped
+        return None, f"{rel} exists but no recorded event reaches it"
+    return None, "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 = [], [], []
+    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:
+            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 = len(baseline.get(key, []))
+            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 models.get(m, {}).get("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)
@@ -553,11 +673,14 @@ def main(argv=None):
     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")
-    events = sub.add_parser("events")
+    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)
 
 
diff --git a/scripts/tests/test_model_sync.py b/scripts/tests/test_model_sync.py
index 3d3478cc..2c270937 100644
--- a/scripts/tests/test_model_sync.py
+++ b/scripts/tests/test_model_sync.py
@@ -3,6 +3,7 @@
 import contextlib
 import importlib.util
 import io
+import json
 import os
 import shutil
 import subprocess
@@ -26,11 +27,7 @@ def run(*argv, env=None):
     return code, out.getvalue()
 
 
-class TraceEvents(unittest.TestCase):
-    def test_repository_events_are_mapped(self):
-        code, out = run("--root", str(ROOT), "events")
-        self.assertEqual(code, 0, out)
-
+class RepoCopy(unittest.TestCase):
     def copy(self):
         tmp = Path(tempfile.mkdtemp())
         self.addCleanup(shutil.rmtree, tmp)
@@ -40,6 +37,12 @@ def copy(self):
         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")
@@ -96,6 +99,58 @@ def test_spec_arm_without_emitter_warns(self):
         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_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
diff --git a/verification/model-map.toml b/verification/model-map.toml
index 8a0a8359..e8860ad1 100644
--- a/verification/model-map.toml
+++ b/verification/model-map.toml
@@ -8,6 +8,14 @@
 # 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,
@@ -25,6 +33,7 @@ code = [
     "concurrency/src/supervision.rs",
     "concurrency/src/lifecycle_trace.rs",
 ]
+coverage_floor = 36   # of 40 action keys
 
 [models.Cohorts]
 # OneForAll/RestForOne rounds (selection, stop, cleanup, join barrier,
@@ -42,6 +51,7 @@ code = [
     "concurrency/src/supervision.rs",
     "concurrency/src/lifecycle_trace.rs",
 ]
+coverage_floor = 40   # of 46 action keys
 
 [models.NestedSupervision]
 # Subtree ownership, attachment, parent join after descendants, shutdown
@@ -60,6 +70,8 @@ code = [
     "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
@@ -73,6 +85,9 @@ files = [
 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
@@ -95,6 +110,9 @@ code = [
     "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.
@@ -107,6 +125,9 @@ 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,
@@ -122,6 +143,21 @@ code = [
     "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
diff --git a/verification/tla/README.md b/verification/tla/README.md
index 996fc77d..8541c7ed 100644
--- a/verification/tla/README.md
+++ b/verification/tla/README.md
@@ -123,6 +123,12 @@ in the same PR; the `model-sync` CI job enforces it
   `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 trace-validated (a `Trace*.tla` that `trace_check.py` runs and
+  recorded events reach), or allowlisted as `tlc_only` with a reason and a
+  tracking item, and keeps each model's covered action keys in
+  `coverage-baseline.json` at or above its `coverage_floor`. TLC-only today:
+  `Coordinator`, `Lifecycle`, `DeferredReplies`, `DeferredJobs`.
 
 ## Trace coverage
 

From 513c2c73a8189e959f4b07ba1da796795ec25697 Mon Sep 17 00:00:00 2001
From: Federico Carrone <mail@fcarrone.com>
Date: Wed, 11 Nov 2026 13:35:40 -0300
Subject: [PATCH 6/7] ci: list only models still TLC-only

---
 scripts/check-model-sync.py | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/scripts/check-model-sync.py b/scripts/check-model-sync.py
index 836c0bad..afec1ec5 100755
--- a/scripts/check-model-sync.py
+++ b/scripts/check-model-sync.py
@@ -610,7 +610,7 @@ def check_models(args, root):
     models = config["models"]
     baseline_path = root / BASELINE
     baseline = json.loads(baseline_path.read_text()) if baseline_path.exists() else {}
-    errors, warnings, rows = [], [], []
+    errors, warnings, rows, tlc_only = [], [], [], set()
     for model in base_models(root):
         entry = models.get(model)
         if entry is None:
@@ -623,6 +623,7 @@ def check_models(args, root):
             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', '?')})"
@@ -653,7 +654,7 @@ def check_models(args, root):
             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 models.get(m, {}).get("tlc_only")]
+    allowlisted = [m for m in base_models(root) if models.get(m, {}).get("tlc_only") and m in tlc_only]
     if allowlisted:
         print(f"\nTLC-only models (no trace validation; these can drift from the code): {', '.join(allowlisted)}")
     if errors:

From 39ac3f9a194190d8b3b11d0bd45aefd683d2823e Mon Sep 17 00:00:00 2001
From: Federico Carrone <mail@fcarrone.com>
Date: Wed, 11 Nov 2026 13:42:24 -0300
Subject: [PATCH 7/7] ci: address review (exact action values, stricter test
 exemption, comment-only model edits, robustness)

---
 docs/TESTING.md                  |  35 ++++---
 scripts/check-model-sync.py      | 173 +++++++++++++++++++++----------
 scripts/tests/test_model_sync.py |  58 ++++++++++-
 verification/model-map.toml      |   5 +-
 verification/tla/README.md       |  10 +-
 5 files changed, 199 insertions(+), 82 deletions(-)

diff --git a/docs/TESTING.md b/docs/TESTING.md
index 5878d77b..8ee05cfb 100644
--- a/docs/TESTING.md
+++ b/docs/TESTING.md
@@ -1130,22 +1130,26 @@ single-use macros.
 
 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 two things mechanically.
+(`.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), the job fails. Changes to
-  comments only, or only inside a `#[cfg(test)] mod` block, are exempt; when
-  the script cannot tell, it requires the waiver. The waiver is the
+  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: the PR run enforced it.
+  <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 (each string literal passed to `Event::new`,
-  `Event::sup`, `TreeEvent::new` and, with PR #240, `LifeEvent`, `JobEvent`
-  and reply events) must be an `e.a = "..."` arm of its trace spec, or be
+  `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`
@@ -1153,14 +1157,13 @@ updates the model in the same PR, and drift is a bug. The `model-sync` job
   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 checked against real runs.** Every model in `verification/tla`
-  needs a map entry and trace validation: a `Trace*.tla` spec that
-  `trace_check.py` runs and that recorded events reach. 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. Today that
-  list is `Coordinator` (abstract fault model, no events recorded) and
-  `Lifecycle`, `DeferredReplies` and `DeferredJobs` (their trace validation
-  comes with PR #240), plus `DynamicSupervisor` once PR #245 lands.
+- **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
diff --git a/scripts/check-model-sync.py b/scripts/check-model-sync.py
index afec1ec5..22a288e3 100755
--- a/scripts/check-model-sync.py
+++ b/scripts/check-model-sync.py
@@ -98,7 +98,7 @@ 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]*")
+    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:
@@ -120,9 +120,9 @@ def parse_toml(text):
             value, i = _toml_value(text, m.end())
             current[m.group(3)] = value
         else:
+            if m.end() == i:
+                break  # end of text
             i = m.end()
-            if m.end() == m.start():
-                i += 1
     return data
 
 
@@ -211,6 +211,7 @@ def blank(a, b):
         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] == "'":
@@ -258,6 +259,51 @@ def call_argument(masked, open_paren, index):
     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)
@@ -282,45 +328,40 @@ def show(root, rev, path):
     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 every changed line of path is a comment line
-    or inside a #[cfg(test)] module (on its side of the diff), else None."""
-    diff = git(root, "diff", "-U0", "--no-color", "--no-ext-diff", f"{base}...{head}", "--", path)
-    old_tests = test_module_lines(show(root, base, path)) if path.endswith(".rs") else []
-    new_tests = test_module_lines(show(root, head, path)) if path.endswith(".rs") else []
-    within = lambda line, ranges: any(a <= line <= b for a, b in ranges)
-    kinds = set()
-    old_line = new_line = 0
-    seen = False
-    for line in diff.splitlines():
-        hunk = re.match(r"@@ -(\d+)(?:,\d+)? \+(\d+)(?:,\d+)? @@", line)
-        if hunk:
-            old_line, new_line = int(hunk.group(1)), int(hunk.group(2))
-            continue
-        if line.startswith(("+++", "---", "diff ", "index ", "new file", "deleted file", "similarity", "rename", "old mode", "new mode", "Binary")):
-            if line.startswith("Binary"):
-                return None
-            continue
-        if line.startswith("\\"):
-            continue
-        if line[:1] not in "+-":
-            continue
-        seen = True
-        text = line[1:].strip()
-        number = new_line if line[0] == "+" else old_line
-        if line[0] == "+":
-            new_line += 1
-        else:
-            old_line += 1
-        if text == "" or text.startswith("//"):
-            kinds.add("comments")
-        elif within(number, new_tests if line[0] == "+" else old_tests):
-            kinds.add("tests")
-        else:
-            return None
-    if not seen:
-        return "comments"  # mode change or no content change
-    return "tests" if "tests" in kinds else "comments"
+    """'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):
@@ -358,10 +399,20 @@ def check_paths(args, root):
         changed, base, head = list(args.files), None, None
     else:
         head = args.head
-        base = args.base or git(root, "merge-base", "origin/main", head).strip()
+        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 changed for g in m["files"])}
+               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"]))
@@ -440,6 +491,7 @@ def check_events(args, root):
     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 = {}
@@ -463,19 +515,23 @@ def check_events(args, root):
                         continue
                     line = masked.count("\n", 0, m.start()) + 1
                     span = call_argument(masked, m.end() - 1, e["arg"])
-                    literals = [v for k, v in strings.items() if span and span[0] <= k < span[1]]
+                    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 (use string 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):
-                if rel == "concurrency/src/lifecycle_trace.rs" or re.search(r"(struct|impl|for)\s+$", masked[max(0, m.start() - 8):m.start()]):
+                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|a)\s*[:,}]", body) or not close:
+                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 = {}
@@ -488,7 +544,6 @@ def check_events(args, root):
         arms = {a: spec for spec, text in specs.items() for a in spec_arms(text)}
         rejected = t.get("rejected", {})
         translated = t.get("translated", {})
-        check_py = (root / "verification/tla/trace_check.py").read_text()
         for action, sites in sorted(emitted.items()):
             if action in arms:
                 continue
@@ -511,6 +566,9 @@ def check_events(args, root):
         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:
@@ -574,7 +632,7 @@ def trace_validation(root, config, model):
     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 = None
+    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)
@@ -582,7 +640,8 @@ def trace_validation(root, config, model):
             continue
         rel = spec_path.relative_to(root).as_posix()
         if spec_path.name not in check_py:
-            return None, f"{rel} exists but trace_check.py never runs it"
+            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:
@@ -594,15 +653,15 @@ def trace_validation(root, config, model):
                 for e in t["emitters"]:
                     for m in re.finditer(e["call"], masked):
                         span = call_argument(masked, m.end() - 1, e["arg"])
-                        emitted.update(v for k, v in strings.items() if span and span[0] <= k < span[1])
-            for how in t.get("translated", {}).values():
-                if isinstance(how, dict):
+                        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
-        return None, f"{rel} exists but no recorded event reaches it"
-    return None, "no trace spec"
+        reasons.append(f"{rel} exists but no recorded event reaches it")
+    return None, "; ".join(reasons) or "no trace spec"
 
 
 def check_models(args, root):
@@ -635,7 +694,7 @@ def check_models(args, root):
         floor = entry.get("coverage_floor")
         key = entry.get("coverage_key", model)
         if floor is not None:
-            covered = len(baseline.get(key, []))
+            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}. "
@@ -654,7 +713,7 @@ def check_models(args, root):
             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 models.get(m, {}).get("tlc_only") and m in tlc_only]
+    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:
diff --git a/scripts/tests/test_model_sync.py b/scripts/tests/test_model_sync.py
index 2c270937..ab06e4d3 100644
--- a/scripts/tests/test_model_sync.py
+++ b/scripts/tests/test_model_sync.py
@@ -1,5 +1,5 @@
-"""Self-tests for scripts/check-model-sync.py (both checks) and the
-repository's own trace event mapping."""
+"""Self-tests for scripts/check-model-sync.py (paths, events, models) and
+the repository's own map."""
 import contextlib
 import importlib.util
 import io
@@ -68,6 +68,33 @@ def test_non_literal_action_fails(self):
         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, \\"\\")";')
@@ -140,6 +167,13 @@ def test_unrun_trace_spec_is_not_validation(self):
         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"
@@ -206,10 +240,28 @@ def test_code_change_without_model_fails(self):
 
     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", "====", "\\* updated\n====")
+        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")
diff --git a/verification/model-map.toml b/verification/model-map.toml
index e8860ad1..315c6ada 100644
--- a/verification/model-map.toml
+++ b/verification/model-map.toml
@@ -3,7 +3,8 @@
 # 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). Otherwise the PR needs the `no-model-change` label and a
+# 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
@@ -31,6 +32,7 @@ files = [
 ]
 code = [
     "concurrency/src/supervision.rs",
+    "concurrency/src/supervision/**",
     "concurrency/src/lifecycle_trace.rs",
 ]
 coverage_floor = 36   # of 40 action keys
@@ -49,6 +51,7 @@ files = [
 ]
 code = [
     "concurrency/src/supervision.rs",
+    "concurrency/src/supervision/**",
     "concurrency/src/lifecycle_trace.rs",
 ]
 coverage_floor = 40   # of 46 action keys
diff --git a/verification/tla/README.md b/verification/tla/README.md
index 8541c7ed..6425df78 100644
--- a/verification/tla/README.md
+++ b/verification/tla/README.md
@@ -124,11 +124,11 @@ in the same PR; the `model-sync` CI job enforces it
   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 trace-validated (a `Trace*.tla` that `trace_check.py` runs and
-  recorded events reach), or allowlisted as `tlc_only` with a reason and a
-  tracking item, and keeps each model's covered action keys in
-  `coverage-baseline.json` at or above its `coverage_floor`. TLC-only today:
-  `Coordinator`, `Lifecycle`, `DeferredReplies`, `DeferredJobs`.
+  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