AIP-21 erratum and AIP-23 note (2026-10-01), formal models annotated: the post-quantum commit seal carries no round

AIP-21: a record that reaches `post-quantum` shows that the commit quorum of distinct validators sealed the block
post-quantum in some round; it does not by itself prove that the block was decided (follows the AIP-22 erratum of the same
day). AIP-23: dated note on what the finality level rests on; level names unchanged. Three formal models carry a dated note
where they treated certificate uniqueness as a property of the code rather than of the model.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

aips/AIP-21.md

@@ -4,6 +4,12 @@
 > chain 2800 from block 17,225,968 to block 20,746,736 (2026-09-05 to 2026-09-29). Since block 20,746,736 (AIP-22
 > stage 2) a Falcon-512 certificate is carried every 32nd block and SLH-DSA seals every 128th, with at least seven of
 > ten seals per scheme since block 20,715,632 (AIP-22 stage 1).
+>
+> **Correction added 2026-10-01.** The commit seal this record counts carries no round, and the store keeps seals by block
+> hash across rounds. A record that reaches `post-quantum` shows that at least the commit quorum of distinct validators
+> sealed the block post-quantum, in some round; it does not by itself prove that the block was decided. See the Errata entry
+> of that date, which follows the AIP-22 erratum of the same day. Chain 2800 today, below AIP-22 stage 5, is not affected:
+> a node imports a block only with the ECDSA commit quorum of a single round.
 
 ## Preamble
 
@@ -254,7 +260,24 @@ local, so the record is read on the validator, or through Aere Cloud when that r
 
 ## Errata
 
-None.
+- 2026-10-01, Abstract, Motivation, "The record" (the verdict `post-quantum`) and "The permanent record": the record counts
+  Falcon-512 seals over `M(B) = keccak256(RLP["AERE-PQ-COMMIT-1", chainId, number(B), hash(B)])`, kept by the block's on-chain
+  hash; neither the seal nor the key carries the round. In QBFT an honest validator can commit a block in one round while a
+  different block is decided in a later round, and seals over `M(B)` made in different rounds cannot be told apart (AIP-22,
+  Errata, 2026-10-01). Measured on 2026-10-01 in the reference client: seven valid Falcon-512 seals over `M(p)` from rounds 0
+  and 2 on a block `p` that no round decided (test class `AereRoundFreeCertificateTest`), and a quorum of one round assembled
+  from the post-quantum seals of rounds 0 and 2 in the decision collector, which counts the same seals, under the adversary of
+  AIP-22 who forges ECDSA (`AereRoundFreeCommitTest`, case RF2-Q1). For `aere_getPqFinality` itself this is derived from the
+  code (the same seal store, kept by hash), not run against the method. Withdrawn as written, until the commit seal binds the
+  round: (1) "the immediate post-quantum finality of a block has been true" (Abstract) and the reading of the record as the
+  answer to "is this block final under post-quantum assumptions" (Motivation); (2) the verdict `post-quantum` as finality: the
+  field and its values stay (clients read them) and mean that at least the commit quorum of distinct validators' seals over
+  `M(B)` verify now, which is evidence of participation, not of the decision; (3) "The permanent record": the anchor
+  certificate is the permanent record of the same participation, and the AIP-22 erratum says what it proves. Not affected:
+  chain 2800 below AIP-22 stage 5, where a node imports a block only with the ECDSA commit quorum of one round, so the block of
+  a record is final there against an adversary who cannot forge ECDSA; the record as evidence of which validators sealed the
+  block; and the agreement of the two clients on the same record. The remedy is the one the AIP-22 erratum proposes: a commit
+  seal that binds the round, with a quorum of one round; it is a coordinated fork and is not scheduled.
 
 ## Post-Acceptance Outcome Record
 

aips/AIP-23.md

@@ -1,5 +1,11 @@
 # AIP-23: AERE Proof Protocol (a portable, verifiable statement + on-chain finality envelope)
 
+> **Note added 2026-10-01.** "Finality" and the level `post-quantum` in this document name what the verifier checks: that the
+> notary's record is in a state under a header whose hash the seals of a verified anchor certificate signed (section 4). Since
+> the AIP-22 erratum of 2026-10-01, such a certificate is evidence that its signers sealed that block post-quantum, in some
+> round; it does not by itself prove that the block was decided. The level names, the verdicts and the verifier's output stay
+> as they are; consumers read them.
+
 ## Preamble
 
 | Field | Value |

formal-consensus/anchor_viewchange_smt.py

@@ -41,6 +41,15 @@
 # keccak256 is modelled as an INJECTIVE uninterpreted function where the argument
 # rests on "a different block gives a different digest" [VERIFY: keccak256]. This
 # checks the DESIGN-level composition, NOT the compiled EVM/Besu bytecode.
+#
+# Note added 2026-10-01 (AIP-22 erratum of that date). The guard this model's uniqueness rests on, "the
+# certificate's digest is bound to the block QBFT FINALIZED", is NOT a rule of the shipped code: the anchor rules
+# (PqAnchorDigestRule, PqAnchorSealsRule) check that the certificate sits under the anchor's hash and that K
+# distinct valid seals sign M(parent), and M carries no round. The code therefore behaves as NEGATIVE CONTROL A
+# below, and the erratum measures it in the reference client: seven valid seals over a block that no round
+# decided, and an anchor over it that passes both rules (AereRoundFreeCertificateTest). AV1 and AV2 are
+# properties of this model, not of chain 2800. Below AIP-22 stage 5 such an anchor's own header still needs the
+# ECDSA commit quorum of one round, which an adversary without the classical keys cannot produce.
 # -----------------------------------------------------------------------------
 from z3 import (Int, Bool, Function, IntSort, Solver, And, Or, Not, Implies, If,
                 Sum, sat, unsat)

formal-consensus/pqanchor_ceiling_monotonicity_smt.py

@@ -23,6 +23,9 @@
 #   write cap maxSeals = 5
 #   emergency ceiling minSealsCeiling: only LOWERS K (that is the theorem)
 #   blocking fork at 14,050,000: no block finalizes without the Falcon quorum
+#   Note added 2026-10-01: the "blocking fork at 14,050,000" premise was withdrawn on 2026-08-19 (that height
+#   armed a per-block rule the anchor rules had already retired, and it changed no enforcement). The FORK-*
+#   checks below model that retired rule; they say nothing about the chain after that height.
 #   registry rotation: 13,014,000 -> 7 keys ; 13,600,000 -> 9 keys ;
 #   every height is covered by EXACTLY one registry
 #

formal-consensus/registry_rotation_coverage_smt.py

@@ -24,6 +24,9 @@
 #   K schedule 13,014,000:0 then 13,034,000:3 (K=3 minimum Falcon seals)
 #   write cap maxSeals = 5; emergency minSealsCeiling can only LOWER K
 #   blocking fork at 14,050,000: no block finalizes without the Falcon quorum
+#   Note added 2026-10-01: the "blocking fork at 14,050,000" premise was withdrawn on 2026-08-19 (that height
+#   armed a per-block rule the anchor rules had already retired, and it changed no enforcement). The FORK-*
+#   checks below model that retired rule; they say nothing about the chain after that height.
 #   registry rotation 13,014,000 -> 7 keys, 13,600,000 -> 9 keys
 #
 # Schedule semantics (the design being proved): a registry is active from its

formal-consensus/run_consensus_verification.py

@@ -34,7 +34,7 @@ CONSENSUS_MODELS = [
     ("QBFT digest-keyed vote tally (2026-07-14 Finding-A shipped fix)", "qbft_digest_keyed_smt.py"),
     ("QBFT IBFT 2.0 locking, engine-role model (2026-07-14 Findings D/E)", "qbft_locking_smt.py"),
     ("QBFT NETWORK-PARTITION safety/liveness (N=9 parametric: split-brain, starvation, heal)", "partition_safety_smt.py"),
-    ("Anchor x VIEW-CHANGE (no round change yields two valid PQ certificates, N=9)", "anchor_viewchange_smt.py"),
+    ("Anchor x VIEW-CHANGE (MODEL only, under its finalized-block guard: no round change yields two valid PQ certificates, N=9; the code has no such guard, Note added 2026-10-01)", "anchor_viewchange_smt.py"),
     ("PQ MESSAGE-LAYER ENFORCEMENT (SPEC 2.6: armed-requires-valid, no cross-domain/position/author replay, below-fork unchanged, commit form under armed anchor = D-311)", "pq_message_enforcement_smt.py"),
     ("PqAnchor CEILING monotonicity (minSealsCeiling only lowers K; K_eff <= maxSeals)", "pqanchor_ceiling_monotonicity_smt.py"),
     ("PQ anchor REGISTRY index binding (loader and seal rule read ONE mapping)", "registry_index_binding_smt.py"),