diff --git a/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md b/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md
index 581a73af80..cf2f8a8312 100644
--- a/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md
+++ b/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md
@@ -160,7 +160,11 @@ the TypeScript runtime each own one spelling of the same idea.
   defined nowhere else under `loopx/`. Everyone else imports.
 - **I2 Closed sets.** Every value a registered vocabulary may carry is listed.
   The code carries no unregistered value in either runtime and the registry
-  lists no value the code does not carry.
+  lists no value the code does not carry. Stage `m0`, delivered, and blocking
+  today: the fixed literal scan exits the smoke non-zero on an unregistered
+  comparison. Its evidence is bounded to the dispatch forms the scanner
+  recognises, so a value that reaches the code by any other form is unverified,
+  not shown to be absent.
 - **I3 Cross-runtime parity.** When a vocabulary has a Python and a TypeScript
   owner, both carry the identical set.
 - **I4 Total projections.** A registered projection names every source value
@@ -205,24 +209,38 @@ the TypeScript runtime each own one spelling of the same idea.
   Only the owner defines the set and only producers write values. Mentioning,
   comparing, serializing, or displaying a value confers no ownership. An
   interpreter or pass-through that starts writing a value has become a
-  producer and must be registered as one. Enforced from M0.5.
+  producer and must be registered as one. Stage `m0_5`, delivered. Blocking
+  today for the producer half: a site that writes a kernel value without being
+  registered as a producer exits the smoke non-zero (`undeclared producer
+  sites`). Not blocking for the consumer half: interpreters and pass-throughs
+  are deliberately unregistered, so their only evidence is the advisory F3
+  inventory and no check can fail on them.
 - **I12 Every kernel value is produced.** For a `kernel` vocabulary, every
   value not listed under `compatibility_only` has at least one production site
   the fixed production forms recognise or an executable witness at a registered input decoder. A variable-source note alone is not production evidence. A
   value that is only compared is dead or compatibility-only, never canonical.
-  `skip` in `effective_action` is the first expected failure. Enforced from
-  M0.5; at M0 the literal scan accepts a compared value as carried.
+  `skip` in `effective_action` is the first expected failure. Stage `m0_5`,
+  delivered. Blocking today over the kernel tier: a registered kernel value with
+  no observed producer exits the smoke non-zero. Evidence is bounded to the
+  production forms inside the scan reach, which is F2's `verified / registered`
+  of 6 / 26, so the `cross_runtime` tier is unverified rather than passed. At M0
+  the literal scan accepted a compared value as carried.
 - **I13 Producers write registered values only.** A production site that
   writes a value outside the registered set fails closed, independently of
   whether any consumer compares it. Production is stricter than comparison: a
   consumer comparing an unregistered value is dead code, a producer writing one
-  is protocol drift. Enforced from M0.5; the M0 literal scan covers both forms
-  together.
+  is protocol drift. Stage `m0_5`, delivered. Blocking today: a recognised
+  producer writing a value outside the registered set exits the smoke non-zero,
+  over the same 6 / 26 domain as F1. Unresolved dynamic sites are reported and
+  counted, never treated as proven safe. At M0 the literal scan covered both
+  forms together.
 - **I14 Scope is declared, not inferred.** A name defined in several modules
   is a fork unless the registry declares it `bounded_context` and lists the
   contexts and one owner symbol per context. Declared names leave the fork
   budget; a rename does not change the budget's meaning and is not a fix.
-  Enforced from M0.5; at M0 `SOURCE_SURFACES` is counted as a fork and noted.
+  Stage `m0_5`, delivered. Blocking today: a declaration that does not name every
+  defining module exactly once exits the smoke non-zero, over 4 / 4 declared
+  contexts. At M0 `SOURCE_SURFACES` was counted as a fork and noted.
 
 ## 3. Scope and non-goals
 
@@ -556,13 +574,13 @@ Each obligation records the set it quantifies over in
 `formal_model.invariants[].domain`, and the smoke derives both sizes from the
 registry rather than trusting the declared numbers:
 
-| Obligation | Quantifies over | Verified / registered | Evidence bound |
-| --- | --- | --- | --- |
-| F1, F2 | `vocabularies[tier=kernel].producers` | 6 / 26 | producer scan reach |
-| F3 | `vocabularies[*]` | 0 / 26 | inventory only |
-| F4 | `scope_declarations[*].contexts` | 4 / 4 | declared defining modules |
-| F5 | `projections[*]` | 1 / 1 | executable owner function |
-| F6 | `persists_edges[*]` | 0 / 0 | unmodelled |
+| Obligation | Quantifies over | Verified / registered | Evidence bound | Stage | Blocks today |
+| --- | --- | --- | --- | --- | --- |
+| F1, F2 | `vocabularies[tier=kernel].producers` | 6 / 26 | producer scan reach | `m0_5` | Yes, within the 6 |
+| F3 | `vocabularies[*]` | 0 / 26 | inventory only | `advisory` | No |
+| F4 | `scope_declarations[*].contexts` | 4 / 4 | declared defining modules | `m0_5` | Yes |
+| F5 | `projections[*]` | 1 / 1 | executable owner function | `m0` | Yes |
+| F6 | `persists_edges[*]` | 0 / 0 | unmodelled | `unproved` | No |
 
 `verified` is the sub-domain the enforcement stage walks; `registered` is the
 whole population of the same unit. An advisory or unproved stage walks nothing,
@@ -575,6 +593,29 @@ denominator moves with any new module; the smoke prints the current ratio, the
 unresolved-site total, and the share of that total no wider scan could ever
 resolve (E21).
 
+#### Four separate readings of one obligation row
+
+A `formal_model.invariants[]` row is read four ways. This RFC states each of them
+separately, because collapsing them is exactly how validated metadata comes to
+read as an executed proof:
+
+| Reading | Where it lives | What it can say, and what it cannot |
+| --- | --- | --- |
+| Schema validation | `check_formal_model` in the drift smoke | The block has the exact key set, the five roles, the consumer hierarchy, the seven relation kinds, each of F1 to F6 stated exactly once with a non-empty statement and evidence boundary, a lane agreeing with its stage, and a domain whose two sizes the smoke recomputes from the registry. It says the claim is *well formed*. It never evaluates the claim |
+| Implementation stage | `invariants[].enforcement` and the lane name | Which milestone owns the check: `m0`, `m0_5`, `advisory`, `unproved`. A stage is a position in the delivery plan, not a result |
+| Evidence status | `invariants[].evidence`, `invariants[].domain`, and `proof_boundary` | What the check rests on and how much of the population it walks: `verified / registered` under a named `evidence_bound`, classified `established`, `bounded`, `unknown` or `unproved`. Bounded evidence over a sub-domain is not proof over the whole |
+| Blocking behaviour | whether a violation makes `examples/semantic-vocabulary-drift-smoke.py` exit non-zero | The only reading that answers "will this stop a merge". It is a property of the calls in the smoke's `main()`, not of any field in the registry |
+
+The four do not move together, and the current tree is the proof of that. F1, F2
+and F4 carry implementation stage `m0_5` and sit in the `blocking_next` lane, yet
+they block a merge today over the kernel tier and the declared scopes. F3 is
+schema-valid, carries an evidence string, and walks nothing. F6 is schema-valid
+and has no check at all. A row that validates therefore establishes exactly one
+thing: the claim is well formed. Reading a discharged proof, a delivered check or
+a merge blocker out of that validation is the failure mode this subsection
+exists to prevent, and the regressions in
+`tests/architecture/test_semantic_formal_model.py` pin the distinction in code.
+
 These are different proof obligations. M0 establishes owner-set equality,
 cross-runtime parity, the declared executable projection, and inventory
 computed from the current tracked tree. Fixed literal forms and closed-set carriers provide bounded evidence,
@@ -658,9 +699,9 @@ vocabulary key fails the smoke.
 | `vocabularies.<name>.input_producer` | Fixed executable decoder witness, currently `turn_result_kind` only | Every registered input produces the matching typed member and invalid probes reject; arbitrary callable selection is forbidden |
 | `vocabularies.<name>.producers` (M0.5) | `path::Symbol` sites that write the field, required for `kernel` | Every site writes registered values only; every value not under `compatibility_only` has at least one source site or executable input witness (I12, I13) |
 | `vocabularies.<name>.compatibility_only` (M0.5) | values retained for persisted readers or a legacy typed caller interface | Subset of `values`; zero production sites; each carries a `value_notes` reason and a retirement milestone |
-| `formal_model` | finite universes, role relations and hierarchy, semantic obligations, candidate decisions, and established/bounded/unknown/unproved claims | Exact schema, role hierarchy, candidate decisions, and invariant ids are checked by the drift smoke; enforcement stages cannot be mistaken for completed proofs |
+| `formal_model` | finite universes, role relations and hierarchy, semantic obligations, candidate decisions, and established/bounded/unknown/unproved claims | Schema validation only. The drift smoke checks the exact key set, the role hierarchy, the candidate decisions, and that each of F1 to F6 is stated exactly once with a non-empty statement, evidence boundary and derived domain; `tests/architecture/test_semantic_formal_model.py` mutates each of those rules. A validated block is a well-formed claim, never an executed proof, and what blocks a merge is the code in the smoke's `main()`, not this field (Section 5, "Four separate readings of one obligation row") |
 | `formal_model.invariants[].domain` | the set the obligation quantifies over: `quantifies_over` selector, `verified` and `registered` sizes, `evidence_bound` | Selector and bound are code-owned names pinned per invariant by `FORMAL_DOMAIN_ANCHOR`; both sizes are derived from the registry and must equal the declared ones; an advisory or unproved stage must declare `verified: 0`, an enforced stage a non-empty domain |
-| `formal_model.enforcement_policy` | blocking-now, blocking-next, advisory, and unproved lanes | Every formal invariant appears exactly once and its lane agrees with its enforcement stage |
+| `formal_model.enforcement_policy` | blocking-now, blocking-next, advisory, and unproved lanes | Every formal invariant appears in exactly one lane and its lane agrees with its `enforcement` stage. The lane records the implementation stage that owns the check, not whether a violation blocks a merge today; the two are tabulated separately in Section 11 |
 | `vocabularies.<name>.value_notes`, `deprecated_values` | per-value review notes; values slated for removal | Names must be registered values |
 | `relations.same_concept` | groups of `vocabulary.value` members | Every member resolves |
 | `relations.shared_field_names` | one field name, its slots and the vocabulary or values each carries | Every slot resolves |
@@ -952,14 +993,25 @@ Track B: scope + producer model + metric boundaries ─────────
 ```
 
 The formal model uses four enforcement lanes so a difficult property does not
-become an accidental merge blocker:
+become an accidental merge blocker. A lane name records the **implementation
+stage** that owns the check. It is not a statement about what blocks a merge,
+and the two are listed in separate columns because they have diverged:
 
-| Lane | Properties | Current meaning |
-| --- | --- | --- |
-| `blocking_now` | F5 projection totality | Enforced by the M0 smoke today |
-| `blocking_next` | F1 producer closedness, F2 canonical liveness, F4 scope separation | Planned blocking checks after M0.5; not claimed by M0 |
-| `advisory` | F3 consumer domain closedness | Reported evidence; it does not block ordinary consumer edits |
-| `unproved` | F6 persistence/version compatibility | An explicit proof gap; it cannot be reported as passed |
+| Lane | Properties | Implementation stage | Blocks a pull request today |
+| --- | --- | --- | --- |
+| `blocking_now` | F5 projection totality | `m0`, delivered | Yes. A source value the projection neither maps nor rejects exits the smoke non-zero |
+| `blocking_next` | F1 producer closedness, F2 canonical liveness, F4 scope separation | `m0_5`, delivered for the kernel tier and for declared scopes | Yes, inside their declared domains. An unregistered produced value, a registered kernel value with no observed producer, and a scope declaration that does not name every defining module each exit the smoke non-zero. Outside those domains nothing is walked, which is unverified, not passed |
+| `advisory` | F3 consumer domain closedness | `advisory`, no analysis written | No. Consumer and interpreter edges are inventory output; nothing can fail on them |
+| `unproved` | F6 persistence/version compatibility | `unproved`, not modelled | No, and it cannot be reported as passed either |
+
+The `blocking_next` row previously read *planned blocking checks after M0.5; not
+claimed by M0*. That was true when the lane was named and false once M0.5b
+shipped: `check_producers` and `check_scope_declarations` are called from the
+drift smoke's `main()`, and by I10 that smoke fails closed on every pull request
+that runs the Python tests. The lane name is deliberately unchanged -- it still
+records which milestone owns the check -- and the blocking claim has moved to
+its own column. A lane is a schedule position; only the code in `main()` decides
+what stops a merge.
 
 The exit condition for a phase is its evidence row, not the existence of a
 formula or a registry entry. A property moves from `unproved` to `advisory` only
@@ -1071,6 +1123,45 @@ introduce a competing target state.
 
 ## Appendix A: Execution ledger (non-normative)
 
+### 2026-09-17 — Formula, role and enforcement claims separated; formal signature mutated
+
+Normative for the enforcement-lane wording; the checks are unchanged except for
+one added rule. Track B slice B0 of #4447.
+
+- **One measured inconsistency, fixed in the prose.** The Section 11 lane table
+  glossed `blocking_next` as *planned blocking checks after M0.5; not claimed by
+  M0*. F1, F2 and F4 sit in that lane and all three fail closed today: dropping a
+  registered value that `executor.py::_run_turn` writes raises `producer writes
+  unregistered values`; adding a kernel value nobody produces raises `decoder
+  does not produce registered input`; removing one context from the
+  `SOURCE_SURFACES` declaration raises `contexts must name every defining module
+  exactly once`. Each exits the smoke non-zero, and by I10 the smoke runs on the
+  pull-request path. The lane name is a milestone label, so it was kept and the
+  blocking claim moved to a column of its own.
+- **Four readings now stated separately** wherever I2 and I11 to I14 and the
+  lanes are described: schema validation, implementation stage, evidence status,
+  and actual blocking behaviour. A validated `formal_model` row establishes only
+  that the claim is well formed; it is not a delivered check, not an executed
+  proof, and not a merge blocker.
+- **The formal signature was almost untested.** One test touched
+  `check_formal_model`, and it read two fields of `candidate_decisions`. The key
+  set, the five roles, the consumer hierarchy, the six invariant ids, the
+  per-invariant shape and the four-lane partition were unmutated.
+  `tests/architecture/test_semantic_formal_model.py` adds 26 single-mutation
+  regressions, each asserting the checker fails closed naming its own rule.
+- **One mutation escaped and the check was tightened.** An exactly duplicated
+  invariant entry passed: the id set and the lane partition are both sets, so a
+  repeat leaves them unchanged, and every dict `check_formal_model` builds by id
+  keeps the last occurrence only. A second `F1_producer_closedness` carrying a
+  weaker statement validated, and nothing recorded which of the two the smoke had
+  walked. The list must now state each id exactly once.
+- **Not addressed here.** The grounding gap the 2026-09-17 domain entry named is
+  still open: moving an invariant's `enforcement` and its policy lane together
+  stays internally consistent, so a coordinated two-field edit can still
+  downgrade a check without any test failing. Closing it needs the lane to be
+  derived from the code that runs, not declared beside it. B0 narrows the gap to
+  a coordinated edit and documents the residue; it does not close it.
+
 ### 2026-09-17 — Invariant statements bounded to their verified domains
 
 Normative; requires kernel-maintainer approval. No check changes its pass/fail
@@ -1280,6 +1371,7 @@ result on the current tree; what changes is what the invariants claim.
 | 2026-09-16 | Q9: compute the full inventory on demand; retire the committed census | Implementation for [maintainer feedback](https://github.com/huangruiteng/loopx/pull/4360#issuecomment-5692062394); PR review pending | Committed snapshot with post-merge regeneration; diff-only scan rejected | 1, I6, 3, 5, 9, 10, 12 |
 | 2026-09-16 | B2: bind one unrenamed re-export hop in the Python producer scanner | Implementation, Refs [#4447](https://github.com/huangruiteng/loopx/issues/4447) B2; PR review pending | Require every consumer to import the owner module (fragile; failed silently in M2); unbounded multi-hop resolution rejected | 5, Appendix A |
 | 2026-09-16 | B1 rename invariance: add the name-keyed divergence advisory; state the limit it does not close | Implementation, Refs [#4447](https://github.com/huangruiteng/loopx/issues/4447) B1; PR review pending | Keying the budget on value sets (rejected: `CONFIDENCE_LEVELS` and `EDGE_CASE_COMPLEXITIES` share `high/low/medium` with different meanings); a committed name ledger (rejected at M0: Q9 retired the committed census). The advisory lists surviving forks by name; it was first described as catching a one-sided rename, which measurement disproved, so both mirrors state the limit as it behaves | 9 |
+| 2026-09-17 | B0: state schema validation, implementation stage, evidence status and blocking behaviour separately for I2/I11-I14 and the enforcement lanes; require each formal invariant id exactly once | Implementation, Refs [#4447](https://github.com/huangruiteng/loopx/issues/4447) B0; PR review pending | Rename the `blocking_next` lane to match its behaviour (rejected: the lane name is the milestone that owns the check, and renaming it would lose that and collapse the two readings the other way); add a `blocks_today` boolean to `formal_model` (rejected: it would be one more declared field a reader could mistake for a measurement, and the fact is a property of the smoke's `main()`, which no registry edit can change); leave the lane gloss and note the gap in the ledger only (rejected: the gloss is the sentence a reviewer quotes) | 2, 5, 11, Appendix A, Appendix B |
 | 2026-09-17 | Bound F1/F2 to the kernel tier and the scan reach, restate F4 as scope enumeration completeness, and give every obligation a derived `domain` | Implementation, Refs [#4447](https://github.com/huangruiteng/loopx/issues/4447); **kernel-maintainer approval required, not yet given** | Leave the unconditional statements and record the gap in prose only (rejected: the statement was stronger than `validate_production`'s own docstring); restate F4 as per-context value-set disjointness (rejected: refuted by the repo's own data, since `scope_declarations` exists to permit legitimate same-name reuse); widen the scan so the unconditional claim becomes true (rejected: a separate change with its own risk) | 5, 9, Appendix B, Appendix C |
 
 ## Appendix C: Evidence registry
diff --git a/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.zh-CN.md b/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.zh-CN.md
index abb3c455ec..be87c33c2d 100644
--- a/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.zh-CN.md
+++ b/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.zh-CN.md
@@ -136,7 +136,9 @@ todos、capabilities 与 TypeScript 运行时各自拥有同一想法的一种
 - **I1 单一 owner。** 每个注册词表或常量，恰有注册表列出的定义模块，且注册的
   符号名在 `loopx/` 下别无定义。其余模块一律 import。
 - **I2 闭集。** 注册词表可携带的每个值都被列出。任一运行时的代码都不携带未
-  注册的值，注册表也不列出代码不携带的值。
+  注册的值，注册表也不列出代码不携带的值。阶段 `m0`，已交付，且今天即阻断：
+  固定字面量扫描遇到未注册的比较会让 smoke 以非零退出。它的证据以扫描器识别的
+  分发形式为界，因此以其他形式进入代码的值是未验证，而不是已证明不存在。
 - **I3 跨运行时一致。** 词表同时有 Python 与 TypeScript owner 时，两侧集合完全
   相同。
 - **I4 完整投影。** 注册投影为每个源值恰好命名一次：要么映射，要么声明拒绝。
@@ -169,21 +171,28 @@ todos、capabilities 与 TypeScript 运行时各自拥有同一想法的一种
 - **I11 角色互异。** 一个词表有一个 owner、若干生产者、若干解释者与若干透传者
   （第 5 节"词表的角色"）。只有 owner 定义集合，只有生产者写入值。提及、
   比较、序列化或展示一个值不带来任何所有权。开始写入值的解释者或透传者已经
-  变成生产者，必须登记为生产者。自 M0.5 起强制。
+  变成生产者，必须登记为生产者。阶段 `m0_5`，已交付。生产者这一半今天即阻断：
+  写入 kernel 值却未登记为生产者的位点会让 smoke 以非零退出
+  （`undeclared producer sites`）。消费者这一半不阻断：解释者与透传者刻意不登记，
+  因此它们唯一的证据是建议性的 F3 清单，没有任何检查能在其上失败。
 - **I12 每个内核值都被生产。** 对 `kernel` 词表，未列入 `compatibility_only`
   的每个值至少有一个固定生产形式能识别的生产位点，或已登记输入解码器的
   可执行见证。变量来源备注本身不能作为生产证据。只被比较的值是死值或兼容值，
   绝不是 canonical。
-  `effective_action` 的 `skip` 是第一个预期失败。自 M0.5 起强制；M0 的字面量
-  扫描把被比较的值当作已携带。
+  `effective_action` 的 `skip` 是第一个预期失败。阶段 `m0_5`，已交付。在 kernel
+  层上今天即阻断：没有观察到生产者的已注册 kernel 值会让 smoke 以非零退出。证据以
+  扫描范围内的生产形式为界，即 F2 的 `verified / registered` 为 6 / 26，因此
+  `cross_runtime` 层是未验证而不是通过。M0 时字面量扫描把被比较的值当作已携带。
 - **I13 生产者只写注册值。** 写入注册集合之外值的生产位点失败即关闭，与是否
   有消费者比较它无关。生产比比较更严：消费者比较一个未注册值是死代码，生产
-  者写一个未注册值是协议漂移。自 M0.5 起强制；M0 的字面量扫描把两种形式合在
-  一起覆盖。
+  者写一个未注册值是协议漂移。阶段 `m0_5`，已交付。今天即阻断：被识别的生产者
+  写入注册集合之外的值会让 smoke 以非零退出，值域与 F1 相同，为 6 / 26。未解析的
+  动态位点被报告并计数，绝不当作已证明安全。M0 时字面量扫描把两种形式合在一起覆盖。
 - **I14 作用域靠声明而非推断。** 在多个模块中定义的名字是分叉，除非注册表把它
   声明为 `bounded_context` 并列出各上下文及每个上下文一个 owner 符号。已声明
-  的名字离开分叉预算；改名不改变预算的含义，不算修复。自 M0.5 起强制；M0 把
-  `SOURCE_SURFACES` 计为分叉并加备注。
+  的名字离开分叉预算；改名不改变预算的含义，不算修复。阶段 `m0_5`，已交付。
+  今天即阻断：没有把每个定义模块恰好枚举一次的声明会让 smoke 以非零退出，值域为
+  4 / 4 个已声明上下文。M0 时 `SOURCE_SURFACES` 被计为分叉并加了备注。
 
 ## 3. 范围与非目标
 
@@ -449,13 +458,13 @@ R ⊆ L × V × Version               将值持久化
 每条义务在 `formal_model.invariants[].domain` 中记录它量化的集合，smoke 从注册表
 推导两个规模数字，而不是相信声明值：
 
-| 义务 | 量化范围 | 已验证 / 已注册 | 证据边界 |
-| --- | --- | --- | --- |
-| F1、F2 | `vocabularies[tier=kernel].producers` | 6 / 26 | producer 扫描范围 |
-| F3 | `vocabularies[*]` | 0 / 26 | 仅清单证据 |
-| F4 | `scope_declarations[*].contexts` | 4 / 4 | 声明的定义模块 |
-| F5 | `projections[*]` | 1 / 1 | 可执行 owner 函数 |
-| F6 | `persists_edges[*]` | 0 / 0 | 未建模 |
+| 义务 | 量化范围 | 已验证 / 已注册 | 证据边界 | 实施阶段 | 今天是否阻断 |
+| --- | --- | --- | --- | --- | --- |
+| F1、F2 | `vocabularies[tier=kernel].producers` | 6 / 26 | producer 扫描范围 | `m0_5` | 是，在这 6 个之内 |
+| F3 | `vocabularies[*]` | 0 / 26 | 仅清单证据 | `advisory` | 否 |
+| F4 | `scope_declarations[*].contexts` | 4 / 4 | 声明的定义模块 | `m0_5` | 是 |
+| F5 | `projections[*]` | 1 / 1 | 可执行 owner 函数 | `m0` | 是 |
+| F6 | `persists_edges[*]` | 0 / 0 | 未建模 | `unproved` | 否 |
 
 `verified` 是该实施阶段真正走到的子值域，`registered` 是同一单位的全体总数。
 建议性（advisory）与未证明（unproved）阶段什么都不走，因此 `verified` 必须为 0；
@@ -465,6 +474,25 @@ R ⊆ L × V × Version               将值持久化
 因为分母会随任何新模块移动；smoke 会打印当前比值、未解析位点总数，以及其中
 再宽的扫描也永远无法解析的那一部分（E21）。
 
+#### 同一条义务行的四种读法
+
+`formal_model.invariants[]` 的一行有四种读法。本 RFC 分别陈述每一种，因为把它们
+混在一起，正是被校验过的元数据变成“已执行的证明”的方式：
+
+| 读法 | 它存在于哪里 | 它能说什么、不能说什么 |
+| --- | --- | --- |
+| Schema 校验 | 漂移 smoke 里的 `check_formal_model` | 该块具有精确的键集合、五个角色、consumer 层级、七种关系边、F1 到 F6 各恰好陈述一次且 statement 与证据边界非空、层级与阶段一致，以及两个规模由 smoke 从注册表重新推导的 domain。它说明这条声明是*格式良好*的。它从不对声明本身求值 |
+| 实施阶段 | `invariants[].enforcement` 与层级名字 | 哪个里程碑拥有这项检查：`m0`、`m0_5`、`advisory`、`unproved`。阶段是交付计划里的位置，不是结果 |
+| 证据状态 | `invariants[].evidence`、`invariants[].domain` 与 `proof_boundary` | 检查依托什么，以及它走过总体的多少：具名 `evidence_bound` 下的 `verified / registered`，分类为 `established`、`bounded`、`unknown` 或 `unproved`。子值域上的有界证据不是全体上的证明 |
+| 阻断行为 | 违例是否让 `examples/semantic-vocabulary-drift-smoke.py` 以非零退出 | 唯一回答“这会不会拦住合并”的读法。它是 smoke `main()` 里那些调用的性质，而不是注册表任何字段的性质 |
+
+这四者并不同步移动，当前源码树本身就是证据。F1、F2、F4 的实施阶段是 `m0_5`、位于
+`blocking_next` 层级，却在今天就会阻断合并——在 kernel 层与已声明作用域之上。F3 通过
+schema 校验、带有证据字符串，却什么都不走。F6 通过 schema 校验，而根本没有检查。
+因此一行通过校验只确立一件事：这条声明格式良好。从这次校验里读出“已完成的证明”、
+“已交付的检查”或“合并阻断项”，正是本小节要防止的失效模式；
+`tests/architecture/test_semantic_formal_model.py` 里的回归把这个区分钉在代码里。
+
 这些是不同的证明义务。M0 已建立 owner 集合相等、跨运行时 parity、声明的可执行投影
 和基于当前已跟踪源码树计算的清单。固定字面量形式与闭集载体只提供有界证据，不是全程序证明。M0.5
 增加有界的生产者和作用域检查。动态代码中的完整生产者发现、`same_concept` 的行为等价、
@@ -534,9 +562,9 @@ external_input | compatibility_only | unknown
 | `vocabularies.<name>.input_producer` | 固定的可执行解码入口，目前仅用于 `turn_result_kind` | 每个注册输入必须产生匹配的类型化成员，非法探测输入必须拒绝；禁止任意选择执行入口 |
 | `vocabularies.<name>.producers`（M0.5） | 写入该字段的 `path::Symbol` 位点，`kernel` 必填 | 每个位点只写注册值；未列入 `compatibility_only` 的每个值至少有一个源码生产位点或可执行输入见证（I12、I13） |
 | `vocabularies.<name>.compatibility_only`（M0.5） | 为持久化读者或旧类型化调用接口保留的值 | `values` 的子集；零生产位点；每个值带 `value_notes` 理由与退休里程碑 |
-| `formal_model` | 有限的集合、角色关系与层次、语义义务、候选决策，以及已建立/有界/unknown/未证明的声明 | 漂移 smoke 校验精确 schema、角色层次、候选决策和不变量 ID；属性实施阶段不能冒充已完成证明 |
+| `formal_model` | 有限的集合、角色关系与层次、语义义务、候选决策，以及已建立/有界/unknown/未证明的声明 | 仅 schema 校验。漂移 smoke 校验精确键集合、角色层次、候选决策，以及 F1 到 F6 各恰好陈述一次且带非空 statement、证据边界与可推导 domain；`tests/architecture/test_semantic_formal_model.py` 对以上每条规则做突变。通过校验的块是格式良好的声明，绝不是已执行的证明；决定是否阻断合并的是 smoke `main()` 里的代码，而不是这个字段（第 5 节“同一条义务行的四种读法”） |
 | `formal_model.invariants[].domain` | 义务量化的集合：`quantifies_over` selector、`verified` 与 `registered` 规模、`evidence_bound` | selector 与证据边界都是代码所有的名字，并由 `FORMAL_DOMAIN_ANCHOR` 逐不变量钉住；两个规模都从注册表推导并必须与声明值相等；advisory 与 unproved 阶段必须声明 `verified: 0`，已强制阶段不得声明空值域 |
-| `formal_model.enforcement_policy` | 当前阻断、下一阶段阻断、建议性和未证明层级 | 每个形式不变量恰好出现一次，且层级与其实施阶段一致 |
+| `formal_model.enforcement_policy` | 当前阻断、下一阶段阻断、建议性和未证明层级 | 每个形式不变量恰好出现在一个层级中，且层级与其 `enforcement` 实施阶段一致。层级记录的是拥有这项检查的实施阶段，而不是违例今天是否阻断合并；两者在第 11 节分列 |
 | `vocabularies.<name>.value_notes`、`deprecated_values` | 逐值评审备注；计划删除的值 | 名字必须是已注册值 |
 | `relations.same_concept` | `vocabulary.value` 成员组 | 每个成员可解析 |
 | `relations.shared_field_names` | 一个字段名、其槽位及各槽位承载的词表或值 | 每个槽位可解析 |
@@ -782,12 +810,19 @@ TypeScript effective-action 绑定与[术语表](../../reference/glossary.md)通
 
 形式模型使用四个强制层级，避免困难性质意外变成合并阻断：
 
-| 层级 | 性质 | 当前含义 |
-| --- | --- | --- |
-| `blocking_now` | F5 投影全性 | 当前 M0 smoke 已强制 |
-| `blocking_next` | F1 生产闭包、F2 规范值存活、F4 作用域分离 | M0.5 后计划强制；M0 不宣称已经做到 |
-| `advisory` | F3 消费者定义域闭包 | 只报告证据，不阻断普通消费者改动 |
-| `unproved` | F6 持久化/版本兼容性 | 明确的证明缺口，不能报告为已通过 |
+| 层级 | 性质 | 实施阶段 | 今天是否阻断 PR |
+| --- | --- | --- | --- |
+| `blocking_now` | F5 投影全性 | `m0`，已交付 | 是。投影既不映射也不拒绝的源值会让 smoke 以非零退出 |
+| `blocking_next` | F1 生产闭包、F2 规范值存活、F4 作用域分离 | `m0_5`，已针对 kernel 层与已声明作用域交付 | 是，在各自声明的值域之内。未注册的被生产值、没有观察到生产者的已注册 kernel 值、以及没有枚举全部定义模块的作用域声明，都会让 smoke 以非零退出。这些值域之外什么都不走，那是未验证，不是通过 |
+| `advisory` | F3 消费者定义域闭包 | `advisory`，尚未写出分析 | 否。消费者与解释者的边只是清单输出，不可能在其上失败 |
+| `unproved` | F6 持久化/版本兼容性 | `unproved`，尚未建模 | 否；同时也不能报告为已通过 |
+
+`blocking_next` 一行原先写作*“M0.5 后计划强制；M0 不宣称已经做到”*。这在该层级被
+命名时是对的，在 M0.5b 交付之后就是错的：`check_producers` 与
+`check_scope_declarations` 都由漂移 smoke 的 `main()` 调用，而按 I10，该 smoke 在
+每个运行 Python 测试的 PR 上失败即关闭。层级名字刻意保持不变——它记录的是哪个里程碑
+拥有这项检查——阻断性的断言则移到了单独一列。层级是日程上的位置；只有 `main()` 里的
+代码决定什么会拦住合并。
 
 阶段完成条件是验收表中的证据，而不是出现一个公式或注册表条目。有界的源码到结果
 分析存在之后，性质才可从 `unproved` 移到 `advisory`；只有记录误报/漏报边界并用突变
@@ -871,6 +906,35 @@ PR review 保留这些层级。普通改动记录检查范围和理由，无共
 
 ## 附录 A：执行账本（非规范）
 
+### 2026-09-17 — 分离公式、角色与强制性声明；对形式签名做突变
+
+强制层级的表述是规范性变更；除新增一条规则外，检查本身不变。#4447 Track B 的 B0 切片。
+
+- **实测到一处不一致，在正文中修正。** 第 11 节层级表把 `blocking_next` 注解为
+  *“M0.5 后计划强制；M0 不宣称已经做到”*。F1、F2、F4 都在该层级，而三者今天都失败
+  即关闭：删掉一个 `executor.py::_run_turn` 确实写入的已注册值，会抛出
+  `producer writes unregistered values`；加入一个没人生产的 kernel 值，会抛出
+  `decoder does not produce registered input`；从 `SOURCE_SURFACES` 声明中移除一个
+  上下文，会抛出 `contexts must name every defining module exactly once`。每一个都让
+  smoke 以非零退出，而按 I10，该 smoke 就在 PR 路径上。层级名字是里程碑标签，因此
+  保留，阻断性的断言移到了它自己的一列。
+- **四种读法现已分别陈述**，覆盖 I2、I11 到 I14 以及各强制层级被描述的每一处：
+  schema 校验、实施阶段、证据状态、实际阻断行为。一行通过校验的 `formal_model` 只
+  确立该声明格式良好；它不是已交付的检查，不是已执行的证明，也不是合并阻断项。
+- **形式签名此前几乎没有测试。** 只有一个测试触及 `check_formal_model`，而它读的是
+  `candidate_decisions` 的两个字段。键集合、五个角色、consumer 层级、六个不变量 ID、
+  逐条不变量的形状以及四层划分都未被突变过。
+  `tests/architecture/test_semantic_formal_model.py` 新增 26 条单点突变回归，每条都
+  断言检查器失败即关闭并指名它自己的那条规则。
+- **有一个突变逃逸，检查已收紧。** 完全重复的不变量条目原本能通过：ID 集合与层级
+  划分都是集合，重复不改变它们，而 `check_formal_model` 按 ID 构造的每个字典都只保留
+  最后一次出现。第二条带有更弱 statement 的 `F1_producer_closedness` 能通过校验，且
+  没有任何东西记录 smoke 实际走过的是哪一条。现在列表必须让每个 ID 恰好陈述一次。
+- **本次未处理。** 2026-09-17 那条值域条目指出的接地缺口仍然存在：同时挪动某条不变量
+  的 `enforcement` 与它的 policy 层级仍然自洽，因此一次协调的双字段修改依然能在不让
+  任何测试失败的情况下降级一项检查。要闭合它，层级必须由真正运行的代码推导，而不是
+  声明在它旁边。B0 把缺口收窄到“需要协调修改”并记录了残留，但没有闭合它。
+
 ### 2026-09-17 — 不变量表述收敛到各自已验证的值域
 
 规范性变更；需要内核维护者批准。当前源码树上没有任何检查的通过/失败结果改变，
@@ -1043,6 +1107,7 @@ PR review 保留这些层级。普通改动记录检查范围和理由，无共
 | 2026-09-16 | Q9：全树按需计算；移除已提交结构清单 | 根据[维护者反馈](https://github.com/huangruiteng/loopx/pull/4360#issuecomment-5692062394)实现，PR 评审待完成 | 取代合并后补再生成；拒绝只扫描 diff | 1、I6、3、5、9、10、12 |
 | 2026-09-16 | B2：Python producer 扫描器绑定一跳未改名再导出 | 实现，Refs [#4447](https://github.com/huangruiteng/loopx/issues/4447) B2；PR 评审待完成 | 要求每个消费者都从 owner 模块导入（脆弱；M2 中已静默失效）；拒绝无界多跳解析 | 5、附录 A |
 | 2026-09-16 | B1 改名不变性：新增按名字归组的分歧报告；写明它未闭合的边界 | 实现，Refs [#4447](https://github.com/huangruiteng/loopx/issues/4447) B1；PR 评审待完成 | 把预算改按值集归组（否决：`CONFIDENCE_LEVELS` 与 `EDGE_CASE_COMPLEXITIES` 共享 `high/low/medium` 而含义不同）；提交名字账本（M0 否决：Q9 已退役提交式清单）。该报告列出仍然存在的分叉；初稿称它能抓住单侧改名，实测证否，故两份镜像按真实行为写明边界 | 9 |
+| 2026-09-17 | B0：为 I2/I11-I14 与各强制层级分别陈述 schema 校验、实施阶段、证据状态与阻断行为；要求每个形式不变量 ID 恰好出现一次 | 实现，Refs [#4447](https://github.com/huangruiteng/loopx/issues/4447) B0；PR 评审待完成 | 把 `blocking_next` 层级改名以匹配其行为（否决：层级名字表示拥有该检查的里程碑，改名会丢掉这层含义，并从另一个方向把两种读法重新合并）；在 `formal_model` 中加一个 `blocks_today` 布尔字段（否决：那只会多出一个可被读者误当作度量的声明字段，而该事实是 smoke `main()` 的性质，任何注册表修改都改不了它）；保留原注解、只在账本里记一笔缺口（否决：评审者引用的正是那句注解） | 2、5、11、附录 A、附录 B |
 | 2026-09-17 | 将 F1/F2 限定在 kernel 层与扫描范围，把 F4 重述为作用域枚举完备性，并给每条义务加上可推导的 `domain` | 实现，Refs [#4447](https://github.com/huangruiteng/loopx/issues/4447)；**需要内核维护者批准，尚未获得** | 保留无条件表述、只在正文记一笔缺口（否决：该表述比 `validate_production` 自己的 docstring 还强）；把 F4 重述为各上下文值集互斥（否决：会被仓库自身数据推翻，`scope_declarations` 恰恰就是为了允许合理的同名复用）；扒宽扫描让无条件声明成立（否决：那是自带风险的另一个变更） | 5、9、附录 B、附录 C |
 
 ## 附录 C：证据登记
diff --git a/examples/semantic-vocabulary-drift-smoke.py b/examples/semantic-vocabulary-drift-smoke.py
index 9452472c85..0acd64d75f 100755
--- a/examples/semantic-vocabulary-drift-smoke.py
+++ b/examples/semantic-vocabulary-drift-smoke.py
@@ -334,8 +334,15 @@ def check_formal_model(model: dict[str, Any], registry: dict[str, Any]) -> None:
             "formal_model role_hierarchy must classify interpreter and pass_through as consumers")
     require(set(model["relations"]) == FORMAL_RELATIONS, "formal_model relations must be the declared edge kinds")
     invariants = model["invariants"]
-    require(isinstance(invariants, list) and {item.get("id") for item in invariants} == FORMAL_INVARIANTS,
-            "formal_model invariants must cover exactly F1-F6")
+    require(isinstance(invariants, list), "formal_model invariants must be a list")
+    invariant_ids = [item.get("id") for item in invariants]
+    require(set(invariant_ids) == FORMAL_INVARIANTS, "formal_model invariants must cover exactly F1-F6")
+    # Every dict below is built by id, so a repeated entry is silently reduced to
+    # its last occurrence: two entries for one id would both validate while only
+    # one of them is reported, and a reader could not tell which statement,
+    # evidence boundary or stage the smoke actually walked.
+    require(len(invariant_ids) == len(set(invariant_ids)),
+            "formal_model invariants must state each of F1-F6 exactly once")
     require(set(FORMAL_DOMAIN_ANCHOR) == FORMAL_INVARIANTS,
             "FORMAL_DOMAIN_ANCHOR must pin a domain for every formal invariant")
     for item in invariants:
diff --git a/tests/architecture/test_semantic_formal_model.py b/tests/architecture/test_semantic_formal_model.py
new file mode 100644
index 0000000000..755369d07d
--- /dev/null
+++ b/tests/architecture/test_semantic_formal_model.py
@@ -0,0 +1,311 @@
+"""Focused regressions for the `formal_model` signature, hierarchy, and lanes.
+
+`examples/semantic-vocabulary-drift-smoke.py::check_formal_model` is the only
+guard standing between a hand-written metadata block and a reader who takes it
+for a machine-checked proof. Before this file, exactly one test touched it
+(`test_candidate_decisions_are_exhaustive_and_default_to_unknown`), and that test
+reads two fields of `candidate_decisions`. Everything else the checker does --
+the exact key set, the five roles, the consumer hierarchy, the six invariant ids,
+the per-invariant shape, and the four-lane partition -- was unmutated, so a
+regression that deleted any of it would have merged green.
+
+Each case below mutates exactly one thing and asserts the checker fails closed
+*naming that rule*. The `match` string is part of the contract: a mutation that
+fails for an unrelated reason proves nothing, and the regression would rot into
+a test that only asserts "something, somewhere, raised".
+
+These tests are deliberately about the *schema* of the claim, not the claim.
+`check_formal_model` validates that an obligation declares a stage, an evidence
+string and a derived domain; it never executes the obligation. The distinction
+is the point of slice B0 of #4447, and
+``test_metadata_shape_is_not_an_executed_proof`` pins it so no later reader can
+recover the conflation from this file.
+"""
+
+from __future__ import annotations
+
+import copy
+import runpy
+from pathlib import Path
+from typing import Any, Callable
+
+import pytest
+
+REPO_ROOT = Path(__file__).resolve().parents[2]
+SMOKE = REPO_ROOT / "examples" / "semantic-vocabulary-drift-smoke.py"
+
+Mutation = Callable[[dict[str, Any], dict[str, Any]], None]
+
+
+@pytest.fixture(scope="module")
+def smoke() -> dict[str, Any]:
+    """Load the smoke once; every test deep-copies the registry before mutating."""
+    return runpy.run_path(str(SMOKE))
+
+
+@pytest.fixture()
+def registry(smoke: dict[str, Any]) -> dict[str, Any]:
+    return copy.deepcopy(smoke["load_registry"]())
+
+
+# --- one mutation per row; the match string names the rule that must fire ------------
+
+
+def drop_required_key(model: dict[str, Any], _registry: dict[str, Any]) -> None:
+    model.pop("proof_boundary")
+
+
+def add_unknown_key(model: dict[str, Any], _registry: dict[str, Any]) -> None:
+    # An unreviewed lane smuggled in as data is how a fifth enforcement class
+    # would arrive without a code edit.
+    model["blocking_eventually"] = ["F6_persistence_version_compatibility"]
+
+
+def drop_universe(model: dict[str, Any], _registry: dict[str, Any]) -> None:
+    model["universes"].pop("roles")
+
+
+def drop_role(model: dict[str, Any], _registry: dict[str, Any]) -> None:
+    model["roles"].remove("pass_through")
+
+
+def drop_subrole_from_hierarchy(model: dict[str, Any], _registry: dict[str, Any]) -> None:
+    # The subrole survives in `roles` but stops being a consumer, which is how a
+    # pass-through would quietly acquire a role of its own.
+    model["role_hierarchy"]["consumer"].remove("pass_through")
+
+
+def empty_role_hierarchy(model: dict[str, Any], _registry: dict[str, Any]) -> None:
+    model["role_hierarchy"] = {}
+
+
+def reparent_hierarchy_to_owner(model: dict[str, Any], _registry: dict[str, Any]) -> None:
+    model["role_hierarchy"] = {"owner": ["interpreter", "pass_through"]}
+
+
+def drop_relation_kind(model: dict[str, Any], _registry: dict[str, Any]) -> None:
+    # `persists` is the edge F6 is stated over; dropping it would leave F6
+    # quantifying over a relation the model no longer declares.
+    model["relations"].pop("persists")
+
+
+def add_relation_kind(model: dict[str, Any], _registry: dict[str, Any]) -> None:
+    model["relations"]["validates"] = "X ⊆ L × V: a site validates a value"
+
+
+def drop_invariant(model: dict[str, Any], _registry: dict[str, Any]) -> None:
+    model["invariants"] = [i for i in model["invariants"] if i["id"] != "F4_scope_separation"]
+    model["enforcement_policy"]["blocking_next"].remove("F4_scope_separation")
+
+
+def duplicate_invariant_id(model: dict[str, Any], _registry: dict[str, Any]) -> None:
+    # Two entries for one id: both validate, and the last one silently wins every
+    # dict the checker builds from the list. See the dedicated test below.
+    original = next(i for i in model["invariants"] if i["id"] == "F1_producer_closedness")
+    model["invariants"].append(copy.deepcopy(original))
+
+
+def unknown_enforcement_stage(model: dict[str, Any], _registry: dict[str, Any]) -> None:
+    invariant(model, "F3_consumer_domain_closedness")["enforcement"] = "mostly_blocking"
+
+
+def empty_statement(model: dict[str, Any], _registry: dict[str, Any]) -> None:
+    invariant(model, "F1_producer_closedness")["statement"] = "   "
+
+
+def empty_evidence(model: dict[str, Any], _registry: dict[str, Any]) -> None:
+    # An obligation with no evidence string is the exact shape B0 exists to stop:
+    # a stage label with nothing behind it reads as a discharged proof.
+    invariant(model, "F5_projection_totality")["evidence"] = ""
+
+
+def invariant_missing_domain(model: dict[str, Any], _registry: dict[str, Any]) -> None:
+    invariant(model, "F5_projection_totality").pop("domain")
+
+
+def invariant_extra_field(model: dict[str, Any], _registry: dict[str, Any]) -> None:
+    invariant(model, "F5_projection_totality")["proved"] = True
+
+
+def invariant_in_two_lanes(model: dict[str, Any], _registry: dict[str, Any]) -> None:
+    model["enforcement_policy"]["advisory"].append("F5_projection_totality")
+
+
+def lane_disagrees_with_enforcement(model: dict[str, Any], _registry: dict[str, Any]) -> None:
+    # F5 is the one obligation the M0 smoke blocks on today; moving its id into
+    # the advisory lane without touching its stage is how a blocking check would
+    # be downgraded in a data-only diff.
+    model["enforcement_policy"]["blocking_now"].remove("F5_projection_totality")
+    model["enforcement_policy"]["advisory"].append("F5_projection_totality")
+
+
+def drop_policy_lane(model: dict[str, Any], _registry: dict[str, Any]) -> None:
+    model["enforcement_policy"].pop("unproved")
+    model["enforcement_policy"]["advisory"].append("F6_persistence_version_compatibility")
+
+
+def unproved_stage_claims_verified_members(model: dict[str, Any], _registry: dict[str, Any]) -> None:
+    invariant(model, "F6_persistence_version_compatibility")["domain"]["verified"] = 1
+
+
+def advisory_stage_claims_verified_members(model: dict[str, Any], _registry: dict[str, Any]) -> None:
+    invariant(model, "F3_consumer_domain_closedness")["domain"]["verified"] = 26
+
+
+def widen_declared_domain(model: dict[str, Any], _registry: dict[str, Any]) -> None:
+    # Restating F1 over every vocabulary rather than the kernel tier is a
+    # normative widening; FORMAL_DOMAIN_ANCHOR must make it a code edit.
+    invariant(model, "F1_producer_closedness")["domain"]["quantifies_over"] = "vocabularies[*]"
+
+
+def proof_boundary_empty_claim(model: dict[str, Any], _registry: dict[str, Any]) -> None:
+    model["proof_boundary"]["unproved"].append("  ")
+
+
+def drop_proof_boundary_class(model: dict[str, Any], _registry: dict[str, Any]) -> None:
+    model["proof_boundary"].pop("unknown")
+
+
+def schema_version_drift(model: dict[str, Any], _registry: dict[str, Any]) -> None:
+    model["schema_version"] = "loopx_semantic_formal_model_v1"
+
+
+def candidate_default_is_not_unknown(model: dict[str, Any], _registry: dict[str, Any]) -> None:
+    model["candidate_decisions"]["default"] = "reuse_existing"
+
+
+def invariant(model: dict[str, Any], name: str) -> dict[str, Any]:
+    return next(item for item in model["invariants"] if item["id"] == name)
+
+
+MUTATIONS: dict[str, tuple[Mutation, str]] = {
+    # --- the signature itself ---
+    "missing_key": (drop_required_key, "keys must be exactly"),
+    "extra_key": (add_unknown_key, "keys must be exactly"),
+    "schema_version_drift": (schema_version_drift, "schema_version drift"),
+    "dropped_universe": (drop_universe, "universes must name the declared sets"),
+    # --- roles and hierarchy ---
+    "dropped_role": (drop_role, "roles must include the consumer role"),
+    "dropped_subrole": (drop_subrole_from_hierarchy, "must classify interpreter and pass_through"),
+    "empty_role_hierarchy": (empty_role_hierarchy, "must classify interpreter and pass_through"),
+    "hierarchy_reparented_to_owner": (reparent_hierarchy_to_owner, "must classify interpreter and pass_through"),
+    # --- relations ---
+    "dropped_relation_kind": (drop_relation_kind, "relations must be the declared edge kinds"),
+    "extra_relation_kind": (add_relation_kind, "relations must be the declared edge kinds"),
+    # --- invariant entries ---
+    "missing_invariant": (drop_invariant, "must cover exactly F1-F6"),
+    "duplicated_invariant_id": (duplicate_invariant_id, "exactly once"),
+    "unknown_enforcement_stage": (unknown_enforcement_stage, "unknown enforcement stage"),
+    "empty_statement": (empty_statement, "needs a statement and evidence"),
+    "empty_evidence": (empty_evidence, "needs a statement and evidence"),
+    "invariant_missing_domain": (invariant_missing_domain, "invalid shape"),
+    "invariant_extra_field": (invariant_extra_field, "invalid shape"),
+    # --- the four lanes ---
+    "invariant_in_two_lanes": (invariant_in_two_lanes, "partition all invariants exactly once"),
+    "lane_disagrees_with_enforcement": (lane_disagrees_with_enforcement, "disagrees with invariant enforcement stage"),
+    "dropped_policy_lane": (drop_policy_lane, "must separate current, next, advisory, and unproved"),
+    # --- stage versus walked domain ---
+    "unproved_claims_verified": (unproved_stage_claims_verified_members, "an unenforced stage walks nothing"),
+    "advisory_claims_verified": (advisory_stage_claims_verified_members, "an unenforced stage walks nothing"),
+    "widened_domain": (widen_declared_domain, "FORMAL_DOMAIN_ANCHOR"),
+    # --- proof boundary and candidate decisions ---
+    "proof_boundary_empty_claim": (proof_boundary_empty_claim, "must contain non-empty claim names"),
+    "dropped_proof_boundary_class": (drop_proof_boundary_class, "must separate established, bounded, unknown"),
+    "candidate_default_changed": (candidate_default_is_not_unknown, "default unresolved candidates to unknown"),
+}
+
+
+def test_committed_formal_model_passes_its_own_checker(
+    smoke: dict[str, Any], registry: dict[str, Any]
+) -> None:
+    """The baseline must be green, or every mutation below proves nothing."""
+    smoke["check_formal_model"](registry["formal_model"], registry)
+
+
+@pytest.mark.parametrize("case", sorted(MUTATIONS))
+def test_formal_model_mutation_fails_closed(
+    smoke: dict[str, Any], registry: dict[str, Any], case: str
+) -> None:
+    mutate, expected = MUTATIONS[case]
+    mutate(registry["formal_model"], registry)
+    with pytest.raises(smoke["Drift"], match=expected):
+        smoke["check_formal_model"](registry["formal_model"], registry)
+
+
+def test_duplicate_invariant_entry_cannot_restate_an_obligation(
+    smoke: dict[str, Any], registry: dict[str, Any]
+) -> None:
+    """Two entries for one id must fail, even when both entries are individually valid.
+
+    The id set and the lane partition are both sets, so a repeated entry leaves
+    them unchanged, and every dict the checker builds by id keeps only the last
+    entry. A second `F1_producer_closedness` carrying a weaker statement was
+    therefore accepted, and a reader of the registry could not tell which of the
+    two the smoke was reporting on. This is the duplicate-entry case B0 names.
+    """
+    model = registry["formal_model"]
+    weakened = copy.deepcopy(invariant(model, "F1_producer_closedness"))
+    weakened["statement"] = "Producers are closed over every registered vocabulary."
+    model["invariants"].append(weakened)
+    with pytest.raises(smoke["Drift"], match="exactly once"):
+        smoke["check_formal_model"](model, registry)
+
+
+def test_role_hierarchy_keeps_both_subroles_under_consumer(
+    smoke: dict[str, Any], registry: dict[str, Any]
+) -> None:
+    """Interpreter and pass-through are consumers (I11), not roles of their own."""
+    model = registry["formal_model"]
+    assert model["role_hierarchy"] == {"consumer": ["interpreter", "pass_through"]}
+    assert set(model["role_hierarchy"]) <= set(model["roles"])
+    for subrole in model["role_hierarchy"]["consumer"]:
+        assert subrole in model["roles"], subrole
+
+
+def test_every_invariant_sits_in_exactly_one_lane_matching_its_stage(
+    smoke: dict[str, Any], registry: dict[str, Any]
+) -> None:
+    model = registry["formal_model"]
+    stage_for_lane = {
+        "blocking_now": "m0",
+        "blocking_next": "m0_5",
+        "advisory": "advisory",
+        "unproved": "unproved",
+    }
+    stages = {item["id"]: item["enforcement"] for item in model["invariants"]}
+    placed = [item_id for ids in model["enforcement_policy"].values() for item_id in ids]
+    assert sorted(placed) == sorted(stages), (sorted(placed), sorted(stages))
+    assert len(placed) == len(set(placed)), placed
+    for lane, ids in model["enforcement_policy"].items():
+        for item_id in ids:
+            assert stages[item_id] == stage_for_lane[lane], (lane, item_id, stages[item_id])
+
+
+def test_metadata_shape_is_not_an_executed_proof(
+    smoke: dict[str, Any], registry: dict[str, Any]
+) -> None:
+    """Every obligation keeps stage, evidence and walked domain separately readable.
+
+    This is the B0 exit condition in executable form. A validated `formal_model`
+    block asserts only that each obligation *declares* an implementation stage, a
+    non-empty evidence boundary and a domain whose sizes the smoke recomputes
+    from the registry. It never asserts that the obligation holds. The two
+    unenforced stages must walk nothing, and the enforced ones must walk a
+    strictly smaller-or-equal sub-domain than the population they are stated
+    over -- so a full ratio can never be inferred from the stage label alone.
+    """
+    model = registry["formal_model"]
+    unenforced = {"advisory", "unproved"}
+    for item in model["invariants"]:
+        stage, domain = item["enforcement"], item["domain"]
+        assert item["statement"].strip(), item["id"]
+        assert item["evidence"].strip(), item["id"]
+        assert domain["verified"] <= domain["registered"], item["id"]
+        if stage in unenforced:
+            assert domain["verified"] == 0, (item["id"], stage, domain)
+        else:
+            assert domain["verified"] > 0, (item["id"], stage, domain)
+    # The proof boundary must keep an explicit unproved class; an empty one would
+    # mean the model claims nothing is left to prove.
+    assert model["proof_boundary"]["unproved"], model["proof_boundary"]
+    assert "unknown" in model["proof_boundary"], model["proof_boundary"]