diff --git a/tests/Tests.FSharp/Formal/Tlc.Runner.Tests.fs b/tests/Tests.FSharp/Formal/Tlc.Runner.Tests.fs
index 133ff5dba..0b2eb5119 100644
--- a/tests/Tests.FSharp/Formal/Tlc.Runner.Tests.fs
+++ b/tests/Tests.FSharp/Formal/Tlc.Runner.Tests.fs
@@ -232,31 +232,26 @@ let ``TLC validates DbspSpec`` () =
     // InvDistinctIdempotent / InvHCorrectness) over the cfg's
     // configured state space.
     //
-    // **Coverage scope (verbatim from DbspSpec.cfg):**
-    //   * Keys K = {"k1", "k2"} (2-key universe)
-    //   * Weights W = {0, 1, 2, 3, 4, 5, 6, 7, 8, 9} — POSITIVE
+    // Coverage scope (from DbspSpec.cfg):
+    //   - Keys K = {"k1", "k2"} (2-key universe)
+    //   - Weights W = {0, 1, 2, 3, 4, 5, 6, 7, 8, 9} — POSITIVE
     //     ONLY. Retraction (negative-weight) cases are NOT
     //     exercised by this model-check; they are covered separately
     //     by the FsCheck property-tests over Z-set algebra in
-    //     `tests/Tests.FSharp/Algebra/ZSetTests.fs` and by the
-    //     Lean proof of Prop 3.2 (`tools/lean4/Lean4/
-    //     DbspChainRule.lean`) which is general over abelian-group
-    //     weights.
-    //   * Explores ~1M distinct initial states in ~11s wall on dev
-    //     hardware; full state-space coverage of the positive-
-    //     weight subset.
+    //     tests/Tests.FSharp/Algebra/ZSetTests.fs and by the Lean
+    //     proof of Prop 3.2 (tools/lean4/Lean4/DbspChainRule.lean)
+    //     which is general over abelian-group weights.
     //
-    // Adding negative-weight coverage to this cfg would either
-    // require enlarging W (linear blow-up in state space) or
-    // refining the spec model — captured as a future-work refinement
-    // for whoever lands the chain_rule_poly (3-group) follow-on.
-    //
-    // Closes the first of the 4 deferred specs in B1 (#1383
-    // math-proofs honest assessment outstanding-work matrix). The
-    // other 3 (SpineAsyncProtocol, CircuitRegistration,
-    // SpineMergeInvariants) have known issues per a 2026-05-03
-    // verify-then-claim sweep — SpineAsyncProtocol +
-    // SpineMergeInvariants produce trace files (counterexamples);
-    // CircuitRegistration has a config bug (invariant Safety
-    // not defined in spec). Tracked as B-0179 + B-0180 + B-0181.
+    // Adding negative-weight coverage would require enlarging W
+    // (linear blow-up in state space) or refining the spec model —
+    // future work tied to the chain_rule_poly (3-group) follow-on.
     assertSpecValid "DbspSpec"
+
+
+[<Fact>]
+let ``TLC validates CircuitRegistration`` () =
+    // Circuit's Register/Build interleaving — verifies the
+    // composite safety invariant `Safety == TypeOK /\
+    // NoRegisterAfterBuild` (matching the spec's stated THEOREM
+    // `Spec => [](TypeOK /\ NoRegisterAfterBuild)`).
+    assertSpecValid "CircuitRegistration"
diff --git a/tools/tla/specs/CircuitRegistration.tla b/tools/tla/specs/CircuitRegistration.tla
index 9bfafe5a6..117bc63d5 100644
--- a/tools/tla/specs/CircuitRegistration.tla
+++ b/tools/tla/specs/CircuitRegistration.tla
@@ -82,6 +82,12 @@ Spec == Init /\ [][Next]_vars /\ WF_vars(Build)
 NoRegisterAfterBuild ==
   built => \A t \in Threads: pending[t] # "registering"
 
+\* Composite safety invariant — the conjunction the THEOREM at the
+\* end of this spec asserts. Defined as a named operator so
+\* CircuitRegistration.cfg's `INVARIANT Safety` directive resolves
+\* against a state predicate.
+Safety == TypeOK /\ NoRegisterAfterBuild
+
 \* Safety: no FeedbackOp can be connected twice. Second Connect call
 \* would require feedbackConnected[op] = FALSE but our CAS guard rejects.
 \* We encode the post-condition: if feedbackConnected[op] flips, it flips