From de9d68c8cf2299fe2b312e8ca3a5928b35d6f16a Mon Sep 17 00:00:00 2001
From: song <22676124+songoow@users.noreply.github.com>
Date: Thu, 17 Sep 2026 10:14:49 -0400
Subject: [PATCH 1/2] test(semantics): mutate the formal-model signature,
 hierarchy and lanes

`check_formal_model` is the only guard between a hand-written `formal_model`
block and a reader who takes it for a machine-checked proof, and exactly one
test touched it: `test_candidate_decisions_are_exhaustive_and_default_to_unknown`
reads 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, so a regression deleting any of them would
have merged green.

Adds 26 single-mutation regressions in a new file, each asserting the checker
fails closed *naming its own rule* -- a mutation that fails for an unrelated
reason proves nothing. New file rather than an append to
test_semantic_vocabulary_drift.py, which three open PRs already collide at.

One mutation escaped and is fixed here rather than asserted away: an exactly
duplicated invariant entry. 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 only the last occurrence. A second `F1_producer_closedness` carrying a
weaker statement validated, and nothing said which of the two the smoke had
walked. The list is now required to state each id exactly once.

`test_metadata_shape_is_not_an_executed_proof` pins the B0 exit condition in
executable form: a validated block asserts only that each obligation declares a
stage, a non-empty evidence boundary and a domain the smoke recomputes from the
registry -- never that the obligation holds.

Refs #4447 (B0)

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Signed-off-by: song <22676124+songoow@users.noreply.github.com>
---
 examples/semantic-vocabulary-drift-smoke.py   |  11 +-
 .../test_semantic_formal_model.py             | 311 ++++++++++++++++++
 2 files changed, 320 insertions(+), 2 deletions(-)
 create mode 100644 tests/architecture/test_semantic_formal_model.py

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"]

From 6671bc3c22a915652a5ea5b918caa2b33e920a9d Mon Sep 17 00:00:00 2001
From: song <22676124+songoow@users.noreply.github.com>
Date: Thu, 17 Sep 2026 10:20:58 -0400
Subject: [PATCH 2/2] docs(semantics): separate formula, stage, evidence and
 blocking claims

I2, I11 to I14 and the four enforcement lanes wrote schema validation,
implementation stage, evidence status and actual blocking behaviour
interchangeably. That is how a validated metadata block comes to read as an
executed proof, and it had already produced one false sentence.

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, which was measured rather than assumed: 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 is on the pull-request path. The RFC text
is what changed: the lane name still records the milestone that owns the check,
and the blocking claim moved to a column of its own.

Section 5 gains "Four separate readings of one obligation row", stating what
each reading can and cannot say, and the domain table now carries stage and
blocking beside the verified/registered counts. The `formal_model` schema rows
say schema validation only. Appendix A and Appendix B both carry a dated
2026-09-17 entry in each mirror.

The residue is stated, not hidden: moving an invariant's `enforcement` and its
policy lane together is still internally consistent, so a coordinated two-field
edit can downgrade a check with no test failing. B0 narrows the gap; closing it
needs the lane derived from the code that runs.

Refs #4447 (B0)

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Signed-off-by: song <22676124+songoow@users.noreply.github.com>
---
 .../semantic-vocabulary-convergence-v0.md     | 138 +++++++++++++++---
 ...emantic-vocabulary-convergence-v0.zh-CN.md | 111 +++++++++++---
 2 files changed, 203 insertions(+), 46 deletions(-)

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：证据登记