# AERE consensus, machine-checked SAFETY + LIVENESS verification (with Falcon quorum extension) > **Note added 2026-10-30 (consensus).** Since block 25,080,000 (AIP-22 stage 5) headers no longer carry ECDSA commit seals: each carries the Falcon-512 seal of its proposer instead, and a commit still carries the ECDSA commit seal of its validator as an additional check. Where the note of 2026-09-24 below describes the headers, it describes chain 2800 below that block. > **Note added 2026-09-24 (consensus).** Where this document says that consensus is classical secp256k1 ECDSA and not post-quantum, read it as the per-block finality statement it was until block 24,300,000 (AIP-22 stage 4, 2026-10-25). Since that block every validator attributes a consensus vote only through its verified post-quantum seal, and a block is post-quantum final once the next anchor, at most 32 blocks later, carries the certificate that covers it; headers still carry classical ECDSA commit seals until AIP-22 stage 5 (this sentence corrected on 2026-10-25). It no longer describes all of consensus on chain 2800: since 2026-08-14 every anchor block must carry a certificate of validator post-quantum seals under its hash (Falcon-512, with SLH-DSA as well since 2026-09-04), and since 2026-09-05 (block 17,250,000) the nine AERE-client validators (nine of the ten) refuse a commit message without a valid Falcon-512 seal of its author, and since 2026-09-08 (block 17,700,000) any QBFT consensus message without one, while the tenth, the second client, enforced that seal only on commit messages until block 24,300,000 and attributes every consensus message only through it since (this clause corrected on 2026-10-12, 2026-10-25 and 2026-10-28; until 2026-10-28 it dated the refusal of every message type to 2026-09-05, the date of the commit layer alone). (Note applied to this document on 2026-10-28.) > **Note added 2026-08-19.** Statements in this document that consensus on chain 2800 is (or remains) classical secp256k1 ECDSA QBFT were written before the post-quantum header anchor went live, and remain true for block-by-block finality. Since block 13,014,000 anchor blocks (every 32nd block, on every one since block 13,889,296) also carry, under the block hash, a certificate of validator Falcon-512 seals, and since 2026-08-14 a node rejects an anchor block with fewer than three valid seals (f+1 of nine; eight or nine are carried in practice). That is a post-quantum checkpoint about every 16 seconds, not a per-block quorum: the claim published on 2026-08-15 that from block 14,050,000 no block finalizes without a post-quantum quorum was wrong (the per-block rule armed at that height is retired in the shipped code in favour of the anchor rules) and was withdrawn on 2026-08-19. Details: https://aere.network/quantum.html and the aere-node repository, anchor/README.md. Date: 2026-07-12 · Scope: AERE QBFT / IBFT 2.0 (Hyperledger Besu, chain 2800) consensus and its staged Falcon-512 quorum-certificate extension (log-only + blocking). This is a **credibility artifact** for the audit. Everything below actually **runs** and is **re-runnable** in seconds. No mainnet node or key was touched to produce it. --- ## 1. Tool used Primary: **z3 (SMT), version 4.16.0**, Python 3.14.4 bindings, on Windows (MSYS2/MINGW64). The models follow the established `formal-consensus/*_smt.py` convention: each property is discharged by proving its **negation UNSAT** under the exact protocol guards, and **every proof is paired with a firing NEGATIVE CONTROL** (a deliberately broken variant whose violation is **SAT**) so the results are demonstrably **non-vacuous**. Why z3 and not TLA+/TLC: TLC/Apalache need a JVM. **Java is not installed on this workstation**, so TLC/Apalache could not be set up *cleanly* here (the task permits z3/SMT in that case). z3 4.16.0 is present and the surrounding `formal-consensus/` directory is already an SMT corpus, so z3 is the rigorous core. Secondary cross-check: **Quint 0.32.0** randomized simulator over the pre-existing `FalconQuorum.qnt` (the Apalache-targeted TLA+‑family spec of the Falcon quorum combinatorics). Quint's *symbolic* backend is Apalache (JVM, absent), so this is **randomized sampling, not a proof**, it is reported only as an independent sanity cross-check of the z3 results. --- ## 2. Files (all under `aerenew/formal-consensus/`) | File | What it verifies | |---|---| | `qbft_safety_smt.py` | **SAFETY / agreement**, no two different blocks committed at one height, `<= f` Byzantine equivocation. L1 intersection lemma (all N) + L2 one-round + L3 cross-round (IBFT 2.0 locking). | | `falcon_logonly_noop_smt.py` | **Falcon LOG-ONLY no-op**, the certificate changes neither any block hash nor the committable set. | | `falcon_blocking_smt.py` | **Falcon BLOCKING**, safety under `<= f` Falcon faults, liveness at the fault bound, and the machine-checked reason **N ≥ 7** is required. | | `qbft_liveness_smt.py` | **LIVENESS** under partial synchrony (post-GST round-change progress). | | `qbft_prepare_counting_smt.py` | **2026-07-14 second-client bug + fix**, Besu's explicit-Prepare quorum rule ⇒ a proposer omitting its self-Prepare deadlocks at D=f; the fix restores liveness (all N) and is safety-neutral. | | `qbft_digest_keyed_smt.py` | **2026-07-14 Finding-A shipped fix**: DIGEST-KEYED vote tally: prepare/commit tallies keyed by digest so prepares cast for an old proposal digest D0 can never be counted toward a conflicting D1 at the same (height,round). Removes the unjustified-quorum / cross-client fork; negative control fires on the flat-set bug. | | `qbft_locking_smt.py` | **2026-07-14 Findings D/E**: IBFT 2.0 round-change locking with the two engine roles (PROPOSER re-proposes the highest prepared value; ACCEPTOR refuses an unjustified round>0 proposal) as explicit variables mapping 1:1 onto the C# fix. Proves the second client MUST enforce acceptor-side locking before it can produce. | | `run_consensus_verification.py` | one-command runner for all seven SMT models (single PASS/FAIL). | | `FalconQuorum.qnt` | pre-existing Quint/Apalache spec (secondary randomized cross-check). | --- ## 3. What was proven, exact configs and results Besu formulas used throughout: **quorum(N) = ceil(2N/3)** (`fastDivCeiling(2N,3)`), **BFT fault bound f(N) = floor((N-1)/3)**. For N=4→q=3,f=1 · N=5→q=4,f=1 · N=7→q=5,f=2. ### 3.1 SAFETY (agreement), `qbft_safety_smt.py` → all PROVED, all neg-controls fired - **L1 quorum-intersection lemma, UNBOUNDED in N (PROVED, unsat):** for **every** N≥1, `2·quorum(N) − N ≥ f(N)+1`. Since any two quorums overlap in `≥ 2q−N` validators (inclusion–exclusion), any two commit quorums share **> f** validators, hence **≥ 1 honest** validator. This is a genuine all-N proof (linear integer arithmetic / Presburger, decidable). - **L2 one-round agreement, bounded, N ∈ {4,5,7,10,13,16} (PROVED, unsat):** explicit per-validator COMMIT with an **equivocating** Byzantine adversary (faulty may double-sign both blocks), `|faulty| ≤ f`. Two distinct blocks cannot both reach a `ceil(2N/3)` COMMIT quorum. - **L3 cross-round agreement, bounded, N ∈ {4,5,7,10,13}, R=3 rounds (PROVED, unsat):** faithful per-validator model of IBFT 2.0 **locking / round-change justification** (honest validators only PREPARE the highest previously-prepared value; the lock is sound because a round-change quorum intersects every earlier prepare-quorum in an honest node, L1). Even across round changes, no two rounds commit different values. - **NEGATIVE CONTROLS (all CEX-FOUND / sat):** lowering the quorum to `ceil(N/2)` breaks L1 (intersection can be ≤ f, witness N=2) and L2 (two blocks both "commit" at N=4); **dropping the lock** breaks L3 (a later round commits a different value). This proves the `ceil(2N/3)` quorum and the locking rule are **load-bearing**, the model genuinely catches unsafety. ### 3.2 Falcon LOG-ONLY no-op, `falcon_logonly_noop_smt.py` → all PROVED, both neg-controls fired Under **A2 (keccak injective)**, with the certificate excluded from every hashed pre-image and never gating finality before the fork: - **N1 (PROVED):** the block hash is invariant to the Falcon certificate (cert is outside the pre-image → two headers differing only in the cert hash identically). - **N2 / N3 (PROVED):** committability, and the whole **set of committable blocks**, are identical with the log-only cert enabled vs. the baseline (no Falcon layer), a **strict no-op**. - **NEGATIVE CONTROLS (CEX-FOUND):** a pre-image that *includes* the cert makes the hash cert-dependent; a log-only rule that *gates* on the cert changes the committable set. So the exclusion and the always-true gate are load-bearing. This is exactly the **mainnet (chain 2800)** posture: log-only, additive, non-gating, **zero halt risk**. ### 3.3 Falcon BLOCKING, `falcon_blocking_smt.py` → all PROVED/expected, neg-controls fired - **B-SAFETY, bounded, N ∈ {4,5,7} (PROVED, unsat):** in blocking mode `≤ f` Falcon-key-faulty validators (allowed to **equivocate**, a valid own-key seal on both conflicting blocks) can never certify two conflicting blocks. - **B-LIVENESS at the fault bound, UNBOUNDED (PROVED, unsat):** `N − f(N) ≥ quorum(N)` for all N, so the honest+correct set alone can always form a certificate. - **THRESHOLD, why N ≥ 7 (machine-checked):** - **T1 (PROVED):** no N ∈ {4,5,6} is **both** safe (`f≥2`) **and** live (`N−2 ≥ q`) against **2** simultaneous Falcon faults; **N=7 is** (f=2, N−2=5 ≥ q=5). N=7 is the smallest validator set that survives 2 Falcon faults safely and live-ly. - **T2:** the single-fault liveness margin `(N−1)−quorum(N)` is **0 exactly at N ∈ {4,5}** (proved unsat that it is nonzero) and **≥ 1 at N ≥ 6** (config). At the proved zero-margin sizes N ∈ {4,5}, one Falcon fault would force *all* remaining honest validators to sign every block, which is why the set was grown past 5. The **live mainnet size is N=7** (verified on-chain 2026-07-16 via `qbft_getValidatorsByBlockNumber`; f=2, quorum 5), the next BFT-optimal 3f+1, which has positive single-fault margin and tolerates 2 faults. - **T3 (STALL, reachable/sat):** at **N=5 with 2 Falcon-faulty** the correct set (3) is below quorum (4) → **no certificate can form → post-fork chain stalls**. At N=7 the same 2 faults still leave quorum (5 = 5) → no stall (PROVED unsat that it stalls). This is precisely why blocking is gated on N ≥ 7 + re-genesis. - **NEGATIVE CONTROLS (CEX-FOUND):** dropping the `≤ f` bound, or lowering the quorum to `ceil(N/2)`, lets two conflicting blocks both be certified, the assumption and the quorum are load-bearing. ### 3.4 LIVENESS under partial synchrony, `qbft_liveness_smt.py` → all PROVED/expected, neg-ctrl fired Premise (**assumed, not proven**, it is the protocol's own premise): **partial synchrony / post-GST** message delivery within an (adaptively growing) round timeout. Asynchronous liveness is impossible (FLP); we do not claim it. - **L-PROGRESS, bounded, N ∈ {4,5,7} (PROVED, unsat):** with round-robin `proposer(r)=r mod N`, any window of `f+1` consecutive rounds contains an **honest** proposer (`≤ f` faulty cannot cover `f+1` distinct proposers; `f+1 ≤ N` checked). - **L-COMMIT, UNBOUNDED + per-N witnesses (PROVED / sat):** an honest proposer's round commits because the honest set alone `N−f ≥ quorum` reaches PREPARE+COMMIT quorum. - **NEGATIVE CONTROL (CEX-FOUND):** with `f+1` faulty, a whole `f+1`-round window can be all-faulty proposers → no guaranteed progress, the `≤ f` bound is load-bearing for liveness too. ### 3.5 Secondary cross-check, Quint `FalconQuorum.qnt` (randomized, not a proof) - `safety`: **no violation** over 20k random samples on **n4/n5/n7**. - `safetyNoAssumption` (drop `≤ f`): **violation found**, matches z3 neg-control. - `configTheorems` (livenessAtF ∧ haltAtFplus1): **no violation** on n4/n5/n7. - `noHaltAtFplus1` (the f+1 halt witness): **violation found** on n4/n5/n7, the stall is reachable. --- ## 4. Honest boundary (what this does and does NOT establish) - **Bounded vs. unbounded.** L1, B-LIVENESS, L-COMMIT and the threshold arithmetic are **unbounded** (proved for **all N** via decidable linear integer arithmetic). L2, L3, B-SAFETY, L-PROGRESS are **bounded model checks** over the stated finite configs (N ∈ {4,5,7}; L3 uses R=3 rounds). **A bounded model check is a decision procedure over that finite configuration, not a proof for all N or all-length executions.** Stated plainly and deliberately. - **Partial synchrony is assumed**, not proven, liveness holds only post-GST (standard for QBFT/IBFT and every partially-synchronous BFT protocol; FLP forbids asynchronous liveness). - **Design combinatorics, not the Besu Java bytecode.** These models check the QBFT/IBFT 2.0 and Falcon-certificate **design math** (message quorums, locking, certificate counting). They do not execute or symbolically analyze the compiled Besu code. The complementary evidence for the Java layer is the consensus unit-test suite and the isolated-testnet runs recorded in `../consensus-pqc/QUORUM-DESIGN.md`. - **Mainnet consensus is classical ECDSA QBFT at N=7, with NO Falcon layer of any kind.** Chain 2800 QBFT is signed with **classical ECDSA** (live set N=7, f=2, quorum 5, verified on-chain); it is **not** post-quantum. **There is no Falcon certificate, not even log-only, in any mainnet header** (verified: mainnet `extraData` is byte-identical to upstream Besu, with no Falcon list). The Falcon **log-only** no-op (§3.2) and **blocking** mode (§3.3) are **isolated-testnet R&D** (chainIds 220744 / 330855, N=4), never live on chain 2800; blocking additionally requires **N ≥ 7 + a re-genesis** carrying a Falcon anchor. Nothing here claims mainnet consensus is post-quantum, and nothing here is live on mainnet. - **Cryptographic soundness of Falcon-512 is out of scope** (covered by NIST KATs + the live PQC precompile / `eth_call`, not by these combinatorial models). B-SAFETY assumes a faulty node can at most equivocate with its *own* key; it cannot forge another validator's seal. --- ## 4b. The 2026-07-14 second-client interop bug + fix, machine-checked (`qbft_prepare_counting_smt.py`) Added 2026-07-14. During the second-execution-client work (a patched Nethermind QBFT block **producer** interoperating with Besu on an isolated testnet), a real interop defect was found in the field, fixed, and confirmed by adversarial soaks (0 forks; Besu-parity throughput after the fix). This model turns that bug + fix into a re-runnable formal artifact and proves the fix is **safe**. **The defect.** Besu tallies the PREPARE quorum from **explicit Prepare messages** and does **not** count the Proposal as an implicit self-Prepare from the proposer. The Nethermind proposer emitted a Proposal but no explicit self-Prepare, leaving every block it proposed **one Prepare short** of quorum → never committed → the chain stalled. **The fix:** the proposer now also broadcasts an explicit self-Prepare (round 0 and round>0) in `AereQbftLiveEngine.cs`. **Why it bit only at the fault boundary (the arithmetic the model proves).** With `D` validators down and the proposer alive, explicit Prepares available are `N−D−1` (buggy) or `N−D` (fixed). At the boundary `D=f` and optimal size `N=3f+1`: alive `A = N−f = 2f+1 = quorum(N)`. So the **buggy** count is `A−1 = 2f = quorum−1` (one short → deadlock even with *every* alive validator honest), while the **fixed** count is `A = 2f+1 = quorum` (commits). For `D