e4cead319d
Aere Network public source. Everything here can be checked against the live chain (chain id 2800, https://rpc.aere.network). Scope note, stated up front rather than buried: consensus on chain 2800 is classical secp256k1 ECDSA QBFT. The post-quantum work in this repository is at the signature, precompile, account and transport layers. Nothing here makes the consensus post-quantum, and no document in it should be read as claiming so.
88 lines
4.8 KiB
Markdown
88 lines
4.8 KiB
Markdown
# Spec 27: TLA+ specification of Aere QBFT 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.
|