Formal-verification broadening: new contract SMT models + canonical runner consolidation

Note added 2026-09-24 (consensus). Where this document says that consensus is classical secp256k1 ECDSA and not post-quantum, read it as the per-block finality statement it was until block 24,300,000 (AIP-22 stage 4, 2026-10-25). Since that block every validator attributes a consensus vote only through its verified post-quantum seal, and a block is post-quantum final once the next anchor, at most 32 blocks later, carries the certificate that covers it; headers still carry classical ECDSA commit seals until AIP-22 stage 5 (this sentence corrected on 2026-10-25). It no longer describes all of consensus on chain 2800: since 2026-08-14 every anchor block must carry a certificate of validator post-quantum seals under its hash (Falcon-512, with SLH-DSA as well since 2026-09-04), and since 2026-09-05 the nine AERE-client validators (nine of the ten) refuse any QBFT consensus message without a valid Falcon-512 seal of its author, while the tenth, the second client, enforced that seal only on commit messages until block 24,300,000 and attributes every consensus message only through it since (this clause corrected on 2026-10-12 and 2026-10-25). (Note applied to this document on 2026-09-27.)

Note added 2026-08-19. Statements in this document that consensus on chain 2800 is (or remains) classical secp256k1 ECDSA QBFT were written before the post-quantum header anchor went live, and remain true for block-by-block finality. Since block 13,014,000 anchor blocks (every 32nd block, on every one since block 13,889,296) also carry, under the block hash, a certificate of validator Falcon-512 seals, and since 2026-08-14 a node rejects an anchor block with fewer than three valid seals (f+1 of nine; eight or nine are carried in practice). That is a post-quantum checkpoint about every 16 seconds, not a per-block quorum: the claim published on 2026-08-15 that from block 14,050,000 no block finalizes without a post-quantum quorum was wrong (the per-block rule armed at that height is retired in the shipped code in favour of the anchor rules) and was withdrawn on 2026-08-19. Details: https://aere.network/quantum.html and the aere-node repository, anchor/README.md.

Date: 2026-07-19. Tooling: Python 3.14.4, z3 4.16.0 (real z3 verdicts, no fabricated greens). All verdicts below were produced by actually running the scripts.

Part 1: four new z3 SMT models (all PROVED, negative controls fired)

Each model proves its safety property by asserting NOT-property under the real Solidity guards (z3 returns UNSAT) and pairs every proof with a firing negative control that removes one guard and returns SAT (non-vacuity). DESIGN-level caveats and [VERIFY]/[MEASURE] items are stated in each model's SUMMARY block exactly as the money-contract models do.

a. pqfinality_smt.py -> PROVED (10 PROVED, 3 CEX-FOUND, 0 FAILED, rc=0)

Contracts: contracts/contracts/pqfinality/AereFinalityCertificateVerifier.sol + AerePQAttestationKeyRegistry.sol Proved: quorum threshold is exactly ceil(2N/3) = (2N+2)/3 (Q0 for all N>=1; Q0b anchors N in {4,5,7,9} -> {3,4,5,6}); an accepted certificate meets that quorum (P1; P1b a 4-of-7 cert is rejected); it is bound to the live registry validatorSetRoot (P2) and size (P2b); it is bound to the chainId+registry attestation domain so a cross-chain/registry certificate is rejected (P3 via injective domain hash; P3b direct); a key rotation that changes the root makes an old-root certificate unaccept-able (P4 via injective root hash); an empty validator set is rejected (P5). Negative controls (all fired SAT): drop quorum -> sub-quorum accepted; drop root binding -> stale/forged root accepted; drop domain binding -> cross-chain replay accepted. Caveats stated: SP1 gateway soundness (verifyProof reverts on invalid proof) is a trusted primitive [VERIFY]; the off-chain zkVM aggregation circuit is [MEASURE], NOT implemented (contract tests use a MOCK gateway); keccak256 injectivity (root/domain) is [VERIFY]; additive PQ finality, consensus stays classical ECDSA QBFT; DESIGN math not EVM bytecode.

b. pqaggregate_smt.py -> PROVED (7 PROVED, 2 CEX-FOUND, 0 FAILED, rc=0)

Contract: contracts/contracts/mpc/AerePQAggregateVerifier.sol Proved: a registered committee is well-formed (R0: root!=0, 1<=t<=n, scheme!=0); an accepted authorization is EXACTLY the registered committee's key set (P1; P1b via committee-root injectivity, so a foreign key set is rejected); it is bound to the caller's message digest (P2); it proves at least threshold t distinct signatures (P3); it binds size and scheme as defense in depth (P4); and the on-chain accept reads only O(1) committee/public fields (keys not stored), so verification cost is independent of n (P5). Negative controls (all fired SAT): drop root binding -> a different committee's key set authorizes; drop digest binding -> a proof for message A authorizes message B. Caveats stated: SP1 gateway soundness [VERIFY]; off-chain zkVM aggregation circuit [MEASURE], not implemented (MOCK gateway); keccak256 injectivity [VERIFY]; account/authorization aggregation not consensus, no funds, no admin; DESIGN math not EVM bytecode.

c. credential_registry_smt.py -> PROVED (7 PROVED, 3 CEX-FOUND, 0 FAILED, rc=0)

Contracts: contracts/contracts/compliance/AereTrustRegistry.sol + AereVerifiableCredential.sol Proved: issuance requires accreditation (A: anchor success => Active AND in-scope; A2: a None/Suspended/Revoked or out-of-scope issuer cannot anchor) and a valid Falcon-512 issuer signature (A3); the status history is append-only so a committed record cannot be rewritten (B, via the standard append relation); revocation is terminal (C: from Revoked no transition returns to Active); and both the anchored (isValid, D) and presented (verifyPresented, D2) verification paths are fail-closed on expired / not-yet-valid / revoked / un-accredited. Negative controls (all fired SAT): drop the accreditation check -> a revoked issuer issues; allow a status overwrite -> a committed record is silently rewritten; drop the validity window -> an expired credential is accepted. Caveats stated: Falcon-512 precompile 0x0AE1 soundness modelled as the sigValid predicate [VERIFY]; the Bitstring Status List and live issuer status are trusted external oracles; application-layer, no funds, consensus stays classical ECDSA QBFT; legal weight of any accreditation is external; DESIGN logic not EVM bytecode.

d. recovery_registry_smt.py -> PROVED (5 PROVED, 2 CEX-FOUND, 0 FAILED, rc=0)

Contract: contracts/contracts/AereRecoveryRegistry.sol Proved: a record is written only if the Falcon-512 signature verifies (FC, fail-closed) and is well-formed (FC2: fault kind / heights / validator set); the per-operator nonce strictly increases on every write (NO); a nonce-k signature cannot be replayed once the nonce advances because the record hash binds the nonce (RP, via injective nonce hash + EUF-CMA verify predicate); and the records array is append-only so a committed record is never rewritten (AP). Negative controls (all fired SAT): drop the nonce binding -> one signature replays to rewrite history; drop append-only -> a committed record is silently overwritten. Caveats stated: Falcon-512 precompile 0x0AE1 soundness (EUF-CMA, input parsing, empty-return-is-invalid) modelled as the verify predicate [VERIFY]; keccak256 injectivity of the nonce-bound record hash [VERIFY]; records attestations only, does not observe consensus or activate PQ consensus (still classical ECDSA QBFT); uint64 nonce cannot realistically overflow; DESIGN logic not EVM bytecode.

Part 2: canonical runner consolidation

File changed: aerenew/formal-consensus/run_consensus_verification.py (had a hardcoded MODELS list of 8 consensus models). Added a CONTRACT_MODELS section wiring in all 7 new contract SMT scripts written in this loop, keeping the 8 consensus models intact: computemarket_smt, destinationsettler_smt, migrator_smt (the 3 money models) + pqfinality_smt, pqaggregate_smt, credential_registry_smt, recovery_registry_smt (the 4 new). The runner now also captures each child's output and tallies the per-check verdict lines.

Canonical runner fresh totals (real run, exit 0)

models run: 15 passed: 15 (8 consensus + 7 contract) verdict lines: 128 PROVED 79 CEX-FOUND 0 FAILED RESULT: ALL MODELS PASS (proofs PROVED, negative controls fired)

Breakdown of the 128/79 (per-check verdict lines, i.e. distinct property checks):

4 new models: 29 PROVED / 10 CEX-FOUND (pqfinality 10/3, pqaggregate 7/2, credential_registry 7/3, recovery_registry 5/2)
3 fund-flow models: 26 PROVED / 11 CEX-FOUND (computemarket 16/3, destinationsettler 5/4, migrator 5/4)
8 consensus models: 73 PROVED / 58 CEX-FOUND (remainder)

Note on scope: the 7 wired-in contract models live in aerenew/formal-consensus/ (the same directory as the canonical runner). The research-stage staging copy (aerenew/research-stage/formal-consensus/) is a separate curated publish target with its own committed expected-output.log and was left unchanged.

REPRODUCE.md update

Updated aerenew/REPRODUCE.md section 3b: the "canonical in-tree" subsection previously cited "8 models" / "8 of 8 models PASS". It now reads "15 models: 8 consensus + 7 contract", "15 of 15 models PASS", with the real fresh runner tally of 128 PROVED / 79 CEX-FOUND / 0 FAILED, the per-group breakdown above, the names of the 7 newly-added contract models, and a restatement of the NOT-property-UNSAT + firing-negative-control discipline and the per-model DESIGN / [VERIFY] / [MEASURE] boundaries. No fabricated numbers: every figure is from the actual run. The staging "(10 models)" section and the older bash-loop "(9 models)" contract section were left as-is (correct and separate).

Honesty posture

All verdicts are real z3 output; no green was fabricated.
Every model has at least one firing negative control (SAT under a removed guard).
No contract was modified. Only SMT scripts were added, the runner was extended, and REPRODUCE.md was updated with real fresh numbers.

10 KiB Raw Blame History