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, as many as the quorum of the ten validators (the seals prove those validators signed the block, not that it was decided, per the AIP-22 erratum of 2026-10-01), 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.