155 lines
10 KiB
Markdown
155 lines
10 KiB
Markdown
# RULEAZA-TOT: the formal verification of AERE consensus, end to end
|
|
|
|
*Translated into English and dated on 2026-10-27. Until that date this document was in Romanian and stated, without a date,
|
|
facts that were true only of the chain of August 2026 (a set of nine validators, an anchor minimum of three); the
|
|
corrections are marked below, and the results it records keep the date they were measured on.*
|
|
|
|
A complete run of everything that can be checked automatically about AERE consensus (QBFT / IBFT 2.0, chain 2800), with two
|
|
independent methods:
|
|
|
|
- **SMT (z3)**, parametric, in this directory (`formal-consensus/*_smt.py`): each property is proved by showing that its
|
|
negation is UNSAT, plus a negative control that plants the violation and must come back SAT. The models scale to N=9,
|
|
the validator set of 2026-08-24, when the table below was written; the set has had ten validators since 2026-09-11, and
|
|
the models state the N each one is run at.
|
|
- **TLA+ / TLC**, exhaustive, in `formal-tla/` of the development tree (not in this repository): it explores the state
|
|
space at a small scale (N=4), where the combinatorics is enough.
|
|
|
|
The rule everywhere: **no model is reported green unless it can come out RED.** Every property has a negative control
|
|
that is run.
|
|
|
|
---
|
|
|
|
## 1. The SMT suite (z3): one command
|
|
|
|
```
|
|
cd formal-consensus
|
|
python run_consensus_verification.py
|
|
```
|
|
|
|
It runs ALL the `*_smt.py` models in this directory (the completeness guard refuses a green result if a model that is
|
|
present is not wired). It prints PASS / FAIL per model, the time of each, and the tally of verdict lines.
|
|
|
|
**Measured 2026-10-07** (Windows, Python 3.14.4 / z3 4.16.0; the times vary with the machine):
|
|
|
|
```
|
|
models run: 37 passed: 37 (16 consensus + 11 contract + 10 application)
|
|
verdict lines: 301 PROVED 159 CEX-FOUND 0 FAILED
|
|
wall time: ~37s total (slowest: qbft_safety_smt.py ~20s)
|
|
coverage: 37 of 37 *_smt.py files wired
|
|
RESULT: ALL MODELS PASS (proofs PROVED, negative controls fired)
|
|
```
|
|
|
|
The history of the figures, dated: 2026-08-24, 35 models (14 consensus), 282 PROVED / 149 CEX-FOUND, ~39 s;
|
|
2026-09-02, + `pq_message_enforcement_smt.py` (36 of 36); 2026-10-07, + `anchor_rewrite_bound_roundfree_smt.py`
|
|
(37 of 37; 13 proofs, 2 lemmas, 4 witnesses, 1 definition, 8 negative controls; the rewrite bound is 32 / 33 under the
|
|
round-free model, as a function of K_eff and of the post-quantum keys held; see
|
|
`research/rewrite-bound-round-free-seal-2026-10-07.md` and `anchor_rewrite_bound_roundfree_smt.RESULT.txt`).
|
|
|
|
The 16 consensus models (14 on 24 August, + 1 on 2 September, + 1 on 7 October):
|
|
|
|
| model | what it proves | N |
|
|
|---|---|---|
|
|
| `qbft_safety_smt.py` | agreement (quorum intersection unbounded; one-round + cross-round locking) | 4,5,7,10,13,16 |
|
|
| `qbft_liveness_smt.py` | progress after GST (f+1 rounds reach an honest proposer) | 4,5,7 |
|
|
| `qbft_locking_smt.py` | IBFT 2.0 locking on the engine roles (view change / round change) | 4,5,7 |
|
|
| `qbft_prepare_counting_smt.py`, `qbft_digest_keyed_smt.py` | the counting of votes (bug and fix of 2026-07-14) | small |
|
|
| `falcon_blocking_smt.py`, `anchor_blocking_quorum_smt.py` | the anchor seal threshold of 2026-08-15 (K=3 of 9; the minimum is 7 of 10 since block 20,715,632) | 9 |
|
|
| `qbft_pqc_activation_smt.py` | the log-only -> blocking transition | - |
|
|
| **`partition_safety_smt.py`** (new on 2026-08-24) | **network partitions: split brain, starvation, healing** | **9, parametric** |
|
|
| **`anchor_viewchange_smt.py`** (new on 2026-08-24) | **a round change at an anchor does not give two valid certificates, in the model, under its finalized-block guard (the code has no such guard: note added 2026-10-01)** | **9** |
|
|
| `pqanchor_ceiling_monotonicity_smt.py` | the emergency ceiling only lowers K | - |
|
|
| `registry_index_binding_smt.py`, `registry_rotation_coverage_smt.py` | the key registry by height (the registries of 2026-08-15) | - |
|
|
| **`anchor_rewrite_bound_roundfree_smt.py`** (2026-10-07) | **the rewrite bound under the adversary holding every classical key: 32 blocks (the anchor + 31), 33 under the exception of the AIP-22 erratum (the undecided sibling, the common grandparent); bounded exactly when the post-quantum keys held j < K_eff (K_eff = 7 on a validator, 1 on the published follower with its ceiling); 128 / 129 in the dated window with interval 128; the reference point pins the prefix (the hash chain unrolled over 1280 heights); `--plant-bounds` is the control of the control** | 10, any K_eff >= 1 |
|
|
|
|
> Note: the three registry / ceiling models were in the directory from 15 to 19 August but were NOT wired into the runner
|
|
> (the completeness guard made it exit with code 2). They were wired on 24 August together with the two new models.
|
|
|
|
---
|
|
|
|
## 2. TLA+ / TLC, exhaustive: network partitions (new on 24 August)
|
|
|
|
The model `formal-tla/QBFTPartition.tla` (development tree) makes the partition an explicitly modelled FAULT (a predicate
|
|
on the delivery of messages between groups) and checks it exhaustively at N=4. Six configurations, each with its positive
|
|
/ negative pair.
|
|
|
|
### The run (much faster under Linux, or WSL on Windows, than natively on Windows)
|
|
|
|
Write a script, copy it, run it without inline quotes. Every run uses `-deadlock`, because the protocol TERMINATES
|
|
normally (everyone has decided) and termination is not a defect. The models are in the development tree only: the TLA+
|
|
results below cannot be rerun from the public repositories today (corrected 2026-10-27: the script asked for the root of
|
|
your clone, where `formal-tla/` does not exist):
|
|
|
|
```bash
|
|
# copy the directory outside any mounted Windows drive (a faster run)
|
|
AERE_REPO=/path/to/the/development/tree # formal-tla/ is not in the public aere-research repository, so this run
|
|
# cannot be reproduced from a public clone today
|
|
mkdir -p /root/ftla
|
|
cp -f "$AERE_REPO"/formal-tla/*.tla /root/ftla/
|
|
cp -f "$AERE_REPO"/formal-tla/*.cfg /root/ftla/
|
|
cp -f "$AERE_REPO"/formal-tla/tla2tools.jar /root/ftla/
|
|
cd /root/ftla
|
|
for CFG in MCpart_safety MCpart_safety_witness MCpart_safety_negctrl \
|
|
MCpart_noprogress MCpart_liveness MCpart_liveness_negctrl; do
|
|
java -XX:+UseParallelGC -cp tla2tools.jar tlc2.TLC QBFTPartition -config ${CFG}.cfg -deadlock
|
|
done
|
|
```
|
|
|
|
### Results measured 2026-08-24 (WSL, OpenJDK 21, exhaustive, 0 states left in the queue)
|
|
|
|
| config | what it checks | expected | result | time |
|
|
|---|---|---|---|---|
|
|
| `MCpart_safety` | 3-1, quorum 3, heal: SAFETY holds | no error | **No error** (1866 states) | ~3s |
|
|
| `MCpart_safety_witness` | the same, invariant `NoCommit` | VIOLATION (a commit is reached) | **NoCommit violated** -> `committed={a}` | ~2s |
|
|
| `MCpart_safety_negctrl` | 2-2, quorum LOWERED to 2 | VIOLATION (fork) | **NoFork violated** -> `committed={a,b}` (v1->a, v3->b) | ~4s |
|
|
| `MCpart_noprogress` | 2-2, quorum 3, NO healing, invariant `NoCommit` | no error | **No error** (81 states; nothing finalizes) | ~2s |
|
|
| `MCpart_liveness` | 2-2, quorum 3, healing, `EventualCommit` | no error | **No error** (liveness returns after the heal) | ~3s |
|
|
| `MCpart_liveness_negctrl` | 2-2, quorum 3, NO healing, `EventualCommit` | VIOLATION | **EventualCommit violated** (stuttering, `committed={}`) | ~2s |
|
|
|
|
The three pairs answer exactly the questions asked:
|
|
- **SAFETY holds on both sides**: `MCpart_safety` is green, and non-vacuous through `witness` (the majority side does
|
|
finalize). The negative control `safety_negctrl` shows that what stops the fork is the ceil(2N/3) quorum: lowered to 2,
|
|
the two sides finalize `a` and `b`.
|
|
- **LIVENESS is lost in the group without a quorum**: `MCpart_noprogress` (nothing finalizes in an unhealed 2-2
|
|
partition).
|
|
- **LIVENESS returns on healing**: `MCpart_liveness` is green; the negative control `liveness_negctrl` shows that without
|
|
the healing step `EventualCommit` FAILS (the heal is the cause).
|
|
|
|
---
|
|
|
|
## 3. TLA+ / TLC: the complete QBFT model (agreement + view change + equivocation)
|
|
|
|
`formal-tla/QBFT.tla` (development tree) with `MCsafety.cfg` (N=4) / `MCsafety7.cfg` (N=7) and `MCliveness.cfg`.
|
|
**Measured 2026-07-19 and 2026-08-24: these configurations do NOT terminate** within the local budget (the state space is
|
|
in the tens of millions; `MCliveness` generated 543k distinct states in 197 s with 527k still queued). What is established
|
|
there is a partial explicit-state witness (9.35 million states without a violation at N=4 round 0), NOT a complete
|
|
check (`TLC-RUN-REPORT.md`, development tree). The all-N core (quorum intersection, agreement under locking) is already
|
|
proved for ANY N by the SMT suite; TLA+ is the independent method, and its value for partitions is that
|
|
`QBFTPartition.tla` does TERMINATE exhaustively (single height), unlike the complete model.
|
|
|
|
---
|
|
|
|
## 4. Optional cross-check: quint / Apalache
|
|
|
|
`FalconQuorum.qnt` is a secondary cross-check (see `CONSENSUS-VERIFICATION-2026-07-12.md` for the `quint run`
|
|
commands).
|
|
|
|
---
|
|
|
|
## The honest boundary (read it, do not skip it)
|
|
|
|
- Model checking **is not a complete proof.** SMT proves the combinatorics of the design (vote counting, quorum
|
|
intersection, the binding of the certificate), not the Besu / EVM bytecode. TLC checks exhaustively only the finite
|
|
configuration stated (N=4 for partitions).
|
|
- Parametric SMT at N=9 proves the property for **that** N; the arithmetic core (quorum intersection, 2q > N) is
|
|
unbounded in N.
|
|
- When these models were written (July to October 2026), chain 2800 committed its blocks with **classical** secp256k1
|
|
ECDSA seals and the post-quantum anchor was ADDITIVE; nothing here implies "post-quantum consensus". The chain of today
|
|
is described in the aere-node SPEC.md. (Corrected 2026-10-27: this point was stated in the present tense.)
|
|
- The cryptographic primitives (keccak injectivity, the soundness of the SP1 gateway, the validation of the Falcon seal)
|
|
are treated as `[VERIFY]`: modelled, not re-proved.
|
|
- In the models of August 2026 the anchor used K=3 = **f+1**, NOT a quorum; since block 20,715,632 the minimum is 7 of
|
|
10 per scheme, as many as the QBFT quorum of the ten validators (corrected 2026-10-27: this point was stated in the
|
|
present tense). In the model, the uniqueness of the certificate comes from its binding to the finalized block, the
|
|
guard of `anchor_viewchange_smt.py`, not from an intersection of seals; the client code has no such guard (note added
|
|
2026-10-01 in the runner).
|