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>
Measured in the reference client: at N = 10, seven valid Falcon-512 seals over M(p) from rounds 0 and 2 while p' is decided in
round 3, and an anchor over p carrying them passes the certificate rules. Withdrawn as written until the commit seal binds the
round: the finality definition of section 1, the Rationale's implication that a quorum of seals proves consensus, and the
Security Considerations claim for H_fin. Chain 2800 below stage 5 is not affected. The original text stays; the correction is
dated in a note at the top and in the Errata.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
AIP-22 described chain 2800 "today" as the chain before stages 1 to 3. A note dated 2026-09-30 says which
stages are active from which block; the index row and the README summary carry the same heights.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
partition_safety_smt.py (N=9 f=2 q=6): split-brain imposibil, starvatie clasificata,
vindecare fara fork. anchor_viewchange_smt.py: o schimbare de runda pe ancora nu da
doua certificate valide diferite, si unicitatea vine din legarea de bloc, nu din K=3
sigilii (< cvorum). Rulatorul cablat: 35 modele, 282 PROVED + 149 CEX, 0 FAILED.
A 6-lens hostile panel with adversarial verification confirmed 17 attacks that
would hold in a public takedown. All repaired: the MI contract now carries the
two base-fee floor-lapse windows (12,978,617-13,087,959 and
13,596,033-13,596,141) as explicit ruleset validation exceptions, so a stranger
implementing the written rules no longer halts where our own follower did; the
honesty boundary now states the full record of reject-on-disagreement including
the windows, and why the fact stays load-bearing; the independence claim is
bounded (upstream skeletons yes, AERE ruleset has one author in both forks, so
a common-author bug passes any differential gate by construction); the harness
verdict claims only what it measures, records engine identity via
web3_clientVersion on every run, refuses same-URL endpoint pairs, and prints
its NOT MEASURED block on every run; stage 4 names the live engine (upstream
parallel processing enabled by default, idling on empty blocks) and its
oracle's model limits; 'governed registry' became 'owner-controlled' with the
single-key fact stated. The panel also confirmed the import-proof doc claimed
a two-month validation history where six days is the truth; fixed.
Motivated by a real defect a from-genesis import proof found the same day: the
public patch set's loader bound key index 0 while its seal rule called it
unbound, rejecting a valid first anchor certificate that production accepts.
The model proves with z3 that under one shared index->address mapping,
'unbound never validates' is a theorem, and exhibits both divergence
directions: valid-rejected (liveness loss, the defect measured today) and
unvouched-accepted (safety loss, the silent one). Both proven impossible under
agreement. Six checks, each with the solver required to SAT the planted bad
world before the UNSAT proof counts. Engineering consequence stated: one
function, not two implementations of the same idea.
The governed on-chain registry (AereCryptoRegistry) maps every registered
post-quantum algorithm to a live verifier: measured 2026-08-15, all 5
algorithms (Falcon-512, Falcon-1024, ML-DSA-44, SLH-DSA-128s, SHAKE256)
resolve to the live NIST precompiles 0x0AE1..0x0AE5, status active, and the
registry contract itself bears code. So 'crypto agility' is not a slide: adding
a scheme or retiring one is a governed registry write, not a hard fork.
Negative control: a planted fake verifier address is caught. Read-only,
eth_call and eth_getCode only. Building this caught two of my own decode bugs
(wrong selector, wrong tuple word) before they became a false public claim,
which is what verification-before-publication is for.
