diff --git a/AERE-PROTOCOL-SPECIFICATION.md b/AERE-PROTOCOL-SPECIFICATION.md index a9a9a07..3de1735 100644 --- a/AERE-PROTOCOL-SPECIFICATION.md +++ b/AERE-PROTOCOL-SPECIFICATION.md @@ -694,6 +694,8 @@ This is the minimal, ordered checklist a stock Besu (or Nethermind) operator app A client built to this checklist validates the live chain, re-executes chain-2800 blocks to byte-identical state roots, and runs the five PQC precompiles byte-for-byte. The reference second client (patched Nethermind 1.39.0) is exactly such a build and has re-validated the full chain to genesis and re-executed real blocks to identical hashes and state roots, and runs the 27/27 PQC KAT vectors identically. +> **Corrected 2026-10-27.** This checklist predates the consensus rules that chain 2800 added after it was written, and the paragraph above overstates it: a client built to this checklist alone does not validate chain 2800 from block 13,014,000, where the anchor certificate rules begin, and it also misses the native post-quantum transactions of type `0x50` (AIP-20, from block 19,900,000) and the post-quantum validator identities and later stages of AIP-22 (from block 20,836,228). Item 14 describes the scope this document was written for, not what a client of chain 2800 must implement today. The rules to add are specified in the aere-node SPEC: sections 2 and 3 (consensus and the anchor certificate), section 5.3 (type `0x50`) and section 6 (what a follower must implement). The reference second client implements them as well, so it is not a build of this checklist alone. + --- ## 8. Formal state-transition delta (the delta as a set of function modifications) diff --git a/REPRODUCE.md b/REPRODUCE.md index 3fa5f04..b2bb40c 100644 --- a/REPRODUCE.md +++ b/REPRODUCE.md @@ -288,6 +288,28 @@ match a fresh count and must not be repeated until reconciled.] ### 3b. Formal verification (z3 SMT, plus Halmos and Solidity SMTChecker) +**Note added 2026-10-27.** The results below are dated (2026-07-19) and their commands use the paths of the development +tree, which a clone of the public repositories does not have. From a clone of the public research repository the whole +suite is one command: + +```bash +pip install z3-solver +cd aere-research/formal-consensus +python run_consensus_verification.py +``` + +Measured on 2026-10-27 (Python 3.14.4, z3 4.16.0), exit 0: + +``` + models run: 37 passed: 37 (16 consensus + 11 contract + 10 application) + verdict lines: 301 PROVED 159 CEX-FOUND 0 FAILED + coverage: 37 of 37 *_smt.py files in this directory are wired into this run +RESULT: ALL MODELS PASS (proofs PROVED, negative controls fired) +``` + +The runner has wired the hybrid dual-quorum and threshold models since 2026-07-20, so the sentence below that says it omits +them describes the runner of 2026-07-19. + **What it proves.** Safety-critical properties are machine-checked, not argued in prose. Each property P is proved by asserting NOT P under the exact protocol guards and showing z3 returns UNSAT (no counterexample). Every proof is paired with a **negative control**: the same model with @@ -341,9 +363,9 @@ only an owner-authorized feedback author can move a score, and the forwarded del version history is append-only, every retrieval names a committed version 1..current, and a priced receipt is consumed at most once), and `bitstring_status_smt` (AereBitstringStatusList: a Revocation list's status bit is monotone / terminal so a revoked credential can never be un-revoked, the epoch -strictly increases, and setting one bit leaves every other credential's bit unchanged). The runner -still omits the hybrid dual-quorum and threshold consensus models from its list, though those `.py` -files are present in the same directory and are run under the staging suite above. +strictly increases, and setting one bit leaves every other credential's bit unchanged). On 2026-07-19 the runner +still omitted the hybrid dual-quorum and threshold consensus models from its list, though those `.py` +files were present in the same directory and were run under the staging suite above (wired since 2026-07-20). ```bash cd aerenew/formal-consensus