aere-docs/AERE-TLA-FORMAL-SPEC.md

# Spec 27: TLA+ specification of Aere QBFT consensus

> **Note added 2026-09-24.** Validator-set figures in this document (N=7 with f=2 and a commit quorum of 5 of 7, or N=9 with a quorum of 6) describe the set on the date they were written. Since 2026-09-11 chain 2800 has ten validators (f=3, commit quorum 7 of 10), all still operated by the Foundation, one of them running the second, Nethermind-derived client. Since 2026-09-04 the anchor certificate is scheme-tagged and carries Falcon-512 seals, with SLH-DSA-SHA2-128s seals as well at every anchor until block 20,746,736 and at every 128th block since; from block 17,225,968 (2026-09-05) to block 20,746,736 there was one anchor every 128 blocks with at least six valid seals for each scheme, and since then (AIP-22 stages 1 and 2, updated 2026-09-30) a Falcon-512 certificate is required every 32 blocks and SLH-DSA seals every 128, with at least seven valid seals for each scheme, the full quorum of the ten validators, from block 20,715,632; since block 20,836,228 the validators are named in consensus by post-quantum ids. The live set and its quorum are at https://aere.network/docs/network/consensus.

Date: 2026-07-19
Deliverable location: `aerenew/formal-tla/` (new directory)

## What was built

A real, well-formed TLA+ model of Aere Network's QBFT / IBFT 2.0 consensus, with
model-checkable safety and liveness properties and TLC configs. It complements
(does not replace) the existing z3 / SMT proofs in `aerenew/formal-consensus/`,
establishing the same properties by a second, independent method.

Files:

| File | Role |
|---|---|
| `aerenew/formal-tla/QBFT.tla` | The specification (constants, vars, actions, properties). 66 definitions; single-height, bounded-round IBFT 2.0. |
| `aerenew/formal-tla/MCsafety.tla` | Concrete N=4 and N=7 instances + message-pool bound. |
| `aerenew/formal-tla/MCsafety.cfg` | Safety, N=4, F=1, Quorum=3, rounds {0,1,2}. |
| `aerenew/formal-tla/MCsafety7.cfg` | Safety, live N=7, F=2, Quorum=5, rounds {0,1}. |
| `aerenew/formal-tla/MCliveness.tla` | Liveness instance (N=4, round-0 proposer Byzantine). |
| `aerenew/formal-tla/MCliveness.cfg` | `EventualCommit` under `FairSpec` fairness. |
| `aerenew/formal-tla/README.md` | What it proves, how to run TLC, relation to z3, honest status. |

## Faithfulness to QBFT / IBFT 2.0

- Constants pin the Besu formulas via `ASSUME`: `Quorum = ceil(2N/3)`,
  `F = floor((N-1)/3)`. N=7 gives quorum 5, f 2 (the live set).
- Four message types (PRE-PREPARE / PREPARE / COMMIT / ROUND-CHANGE) in a uniform
  record pool; quorum accounting counts DISTINCT senders.
- IBFT 2.0 locking: `Justified(r,v)` requires a quorum of valid round-change
  messages and the highest-prepared value among them, backed by a REAL prepare
  quorum (`ValidRoundChange` rejects a fabricated high-prepared certificate,
  because a genuine prepare quorum needs Q distinct senders and only F are
  Byzantine). Honest `Prepare` is guarded by `Justified` (acceptor-side lock);
  `RoundChange` carries the sender's prepare certificate.
- Up to F Byzantine validators unconstrained via `FaultyBroadcast` (inject any
  message from their own identities; cannot forge honest signatures).
- Proposer takes an explicit self-`Prepare` (mirrors the 2026-07-14 fixed Besu
  rule from `qbft_prepare_counting_smt.py`).

## Properties

- Safety invariants: `Agreement` (no two honest validators decide different
  blocks) and `NoFork` (committed set never holds two distinct blocks for one
  height). Mirror `qbft_safety_smt.py` L2/L3 and `qbft_locking_smt.py`.
- Liveness: `EventualCommit` under `FairSpec` (WF on each honest action, none on
  Byzantine). `MCliveness` makes proposer(0) Byzantine so a commit requires a
  round change to an honest proposer, exercising `qbft_liveness_smt.py`'s path.

## Relationship to z3 models

Same properties, different method. z3 proves each property's negation UNSAT
(including the UNBOUNDED all-N quorum-intersection lemma `2q-N >= f+1` and
`N-f >= quorum`, which finite TLC cannot do). TLC gives an independent
explicit-state check of the message-passing protocol at concrete sizes N in
{4,7}. Cross-method agreement is the credibility gain. The all-N arithmetic stays
the z3 models' job; TLC contributes the finite-state protocol exploration.

## Honesty flags

- **[VERIFY] SANY parse not run.** Structure self-checked by a heuristic script
  (module headers + `====` terminators present; parens/brackets/braces/block
  comments balanced; all referenced operators resolve to a definition / constant /
  variable / `Integers`,`FiniteSets`,`Sequences` builtin / bound var). This is NOT
  a real parser. A `tla2sany.SANY QBFT.tla` run on a box with the TLA+ tools jar
  should confirm no residual syntax issue.
- **[MEASURE] No TLC run executed.** The TLA+ tools jar / Apalache are not
  installed in this environment (Java 21 IS present, but that alone is not a TLA+
  tool, and downloading a jar was out of scope). No property is claimed
  model-checked. Run `tlc MCsafety -config MCsafety.cfg`, `tlc MCsafety -config
  MCsafety7.cfg`, `tlc MCliveness -config MCliveness.cfg` and record
  states-explored + no-violation / property-holds.
- **Bounded model check, not all-N.** Fixed finite instances; message-pool cap is
  a knob. A decision procedure over the finite config, not a proof for all N.
- **Liveness is temporal, post-GST.** Progress only after GST; asynchronous
  liveness impossible by FLP and not claimed. Bounded witness only; unbounded
  liveness not decidable by finite TLC.
- **Scope.** Models agreement / progress design, not Besu Java bytecode. Chain
  2800 consensus uses classical ECDSA seals (N=7, f=2, quorum 5). The agreement
  model is orthogonal to the seal scheme; nothing implies post-quantum consensus.

## Status

Artifact written and structurally self-checked. Safety and liveness are
specified and structurally validated, NOT yet model-checked (needs the TLC run
above). Complements, does not replace, the z3 corpus.