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:

# copy the directory outside any mounted Windows drive (a faster run)
AERE_REPO=/path/to/the/clone        # the root of your clone; the formal-tla/ directory sits directly under it
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).

9.9 KiB Raw Blame History