aere-research/formal-consensus/CONSENSUS-VERIFICATION-2026-07-12.md

AERE consensus, machine-checked SAFETY + LIVENESS verification (with Falcon quorum extension)

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<f the buggy rule still clears quorum, which is exactly why the defect only surfaced under the kill-2 (f=2) adversarial soak, never in the healthy set.

Property	Result
P1, buggy rule ⇒ guaranteed stall at D=f (N=3f+1 ∈ {4,7,10,13}): with all alive validators honest and preparing, the explicit-Prepare count cannot reach quorum	PROVED (unsat)
P1-neg, fixed rule, same config, IS committable (proposer self-Prepares → quorum reachable)	CEX-FOUND (sat), the missing self-Prepare is the whole cause
P2, fixed rule ⇒ liveness restored for ALL N (unbounded Presburger): N − f(N) ≥ quorum(N) at the boundary	PROVED (unsat)
P2-neg, buggy count N−f−1 < quorum(N) for some N (a real deadlock exists)	CEX-FOUND (sat), self-Prepare is load-bearing
P3, fixed rule PRESERVES SAFETY (N ∈ {4,7,10,13}): the proposer's one extra honest Prepare (to its single proposed value) cannot make two distinct values both reach quorum under ≤ f equivocating Byzantine	PROVED (unsat)
P3-neg, lowering quorum to ceil(N/2) breaks safety (two values both commit)	CEX-FOUND (sat), the ceil(2N/3) threshold, unchanged by the fix, is what carries safety

16 checks: 8 PROVED, 8 negative controls fired. So the fix restores liveness for all N and is safety-neutral (safety rests on the quorum threshold, invariant to whether the proposer's Prepare is implicit or explicit). This is consistent with, and explains, the empirical result: 0 forks throughout and Besu-parity throughput once the self-Prepare lands. Honest boundary: P1/P3 are bounded per-N checks, P2 an unbounded identity; this models the QBFT Prepare-tally design combinatorics, not the Besu/Nethermind bytecode.

---

5. How to re-run

From aerenew/formal-consensus/:

# one command: runs all seven models, prints a single PASS/FAIL, exit 0 on success
python run_consensus_verification.py

# or individually (each prints PROVED / CEX-FOUND lines and exits 0 on success)
python qbft_safety_smt.py
python falcon_logonly_noop_smt.py
python falcon_blocking_smt.py
python qbft_liveness_smt.py
python qbft_prepare_counting_smt.py   # 2026-07-14 second-client bug + fix
python qbft_digest_keyed_smt.py       # 2026-07-14 Finding-A shipped fix (digest-keyed tally)
python qbft_locking_smt.py            # 2026-07-14 Findings D/E (engine-role IBFT locking)

# optional secondary cross-check (randomized simulation, needs quint; NOT a proof)
quint run FalconQuorum.qnt --main=n7 --invariant=safety             --max-samples=20000 --max-steps=1
quint run FalconQuorum.qnt --main=n7 --invariant=safetyNoAssumption --max-samples=20000 --max-steps=1  # expect violation
quint run FalconQuorum.qnt --main=n5 --invariant=noHaltAtFplus1     --max-samples=20000 --max-steps=1  # expect violation (halt witness)

Requirements: pip install z3-solver (proved with z3 4.16.0); optional npm i -g @informalsystems/quint (0.32.0). To reproduce the TLA+/Apalache symbolic path instead, run FalconQuorum.qnt through quint verify on a box with a JVM (e.g. the infra box), the arithmetic and the results are identical.

---

6. One-line verdict

QBFT/IBFT 2.0 agreement (no two different blocks at one height under ≤ f equivocating Byzantine validators) is machine-checked, unbounded via quorum intersection and bounded across N ∈ {4,5,7,10,13,16} including cross-round locking; liveness holds under partial synchrony; the Falcon log-only certificate is a proven strict no-op (mainnet posture, zero halt risk); Falcon blocking is safe and live at the fault bound and its N ≥ 7 requirement is machine-checked. The 2026-07-14 second-client interop bug (Besu counts only explicit Prepares → a proposer that omits its self-Prepare deadlocks at exactly the D=f boundary) and its fix (proposer broadcasts an explicit self-Prepare) are machine-checked: the fix restores liveness for all N and is safety-neutral. Every proof is backed by a firing negative control. Boundaries (bounded model-check, partial-synchrony assumption, design-not-bytecode, mainnet-is-classical-ECDSA-log-only) are stated honestly.