diff --git a/formal-consensus/anchor_blocking_quorum_smt.py b/formal-consensus/anchor_blocking_quorum_smt.py
index 8360fe1..d6ac033 100644
--- a/formal-consensus/anchor_blocking_quorum_smt.py
+++ b/formal-consensus/anchor_blocking_quorum_smt.py
@@ -2,11 +2,18 @@
 # -----------------------------------------------------------------------------
 # anchor_blocking_quorum_smt.py
 #
-# MACHINE-CHECKED (z3) proof of BLOCKING-QUORUM SAFETY for the AERE post-quantum
-# anchor once the blocking fork is active (height >= 14,050,000).
+# MACHINE-CHECKED (z3) proof of ANCHOR-THRESHOLD SAFETY for the AERE post-quantum
+# anchor (every 32nd block, minimum K=3 seals since height 13,034,000).
+#
+# CORRECTION 2026-08-19: this file used to call the property "blocking-quorum safety
+# once the blocking fork is active (height >= 14,050,000)". The fork property
+# aere.falcon.forkBlock=14050000 arms a per-block rule that the shipped client
+# retires at aere.pq.anchorBlock (13,014,000), so it changed no enforcement; the
+# invariant below never depended on it and is stated for what the chain enforces:
+# K=3 distinct valid seals on anchor blocks (f+1 of 9, not a quorum), none elsewhere.
 #
 #   INVARIANT (the task target):
-#     With the blocking fork active, no ANCHOR block can be finalized with fewer
+#     Since height 13,034,000, no ANCHOR block can be finalized with fewer
 #     than K=3 valid Falcon seals from DISTINCT signers of the registry ACTIVE
 #     at that height; and a NON-anchor block requires no seals at all.
 #
@@ -17,7 +24,7 @@
 #   min-seals schedule on heights: 13014000:0, 13034000:3  (so K=3 at the fork)
 #   producer write cap maxSeals = 5
 #   emergency minSealsCeiling can only LOWER the effective K, never raise it
-#   blocking fork from 14,050,000: no block finalizes without the Falcon quorum
+#   (the fork height 14,050,000 changed no enforcement; see the correction above)
 #   registry rotation on heights: 13014000 -> 7 keys, 13600000 -> 9 keys,
 #   every height covered by EXACTLY one registry
 #
diff --git a/formal-consensus/run_consensus_verification.py b/formal-consensus/run_consensus_verification.py
index 78bb783..e188e49 100644
--- a/formal-consensus/run_consensus_verification.py
+++ b/formal-consensus/run_consensus_verification.py
@@ -27,6 +27,7 @@ CONSENSUS_MODELS = [
     ("QBFT/IBFT 2.0 SAFETY (agreement)",         "qbft_safety_smt.py"),
     ("Falcon LOG-ONLY no-op",                    "falcon_logonly_noop_smt.py"),
     ("Falcon BLOCKING safety/liveness/N>=7",     "falcon_blocking_smt.py"),
+    ("Anchor THRESHOLD safety (K=3 of 9 on anchor blocks since 13,034,000, registry rotation)", "anchor_blocking_quorum_smt.py"),
     ("PQC ACTIVATION transition safety (log-only->blocking + contract-anchored registry)", "qbft_pqc_activation_smt.py"),
     ("QBFT LIVENESS (partial synchrony)",        "qbft_liveness_smt.py"),
     ("QBFT explicit-Prepare counting (2026-07-14 2nd-client bug+fix)", "qbft_prepare_counting_smt.py"),