aere-docs/AERE-FORMAL-FINAL-COVERAGE.md

spec-formal-final: z3 SMT coverage for the new Aere Network contract suite

Prepared 2026-07-19. Environment: Python 3.14.4, z3-solver 4.16.0, Windows 11. All four new models follow the corpus discipline exactly: each safety property is proved by asserting NOT-property under the real Solidity guards (z3 returns UNSAT), paired with a firing negative control that removes one guard and returns SAT (non-vacuity). Real verdicts only. No contract was modified.

PART 1: new z3 SMT models (4 added, all PROVED, all negative controls fired)

a. ap2_mandate_smt.py (AereAP2MandateVerifier) -- 9 PROVED / 3 CEX-FOUND, exit 0

Load-bearing invariant modelled: CAP-SOLVENCY, INV(mh) := 0 <= spentUnder[mh] <= maxAmount. Proved (UNSAT under the real guards):

• base case (fresh mandate spent == 0) satisfies INV;
• authorizeSpend preserves INV inductively (cumulative spend stays within the cap);
• two sequential guarded draws can never exceed the cap (the requested windowed-cumulative property);
• authorizeSpend is monotone (consumed cap is never refunded / reduced, so a replay cannot free cap);
• an expired mandate authorizes nothing (write requires now <= periodEnd);
• a not-yet-valid mandate authorizes nothing (write requires now >= periodStart);
• an accepted authorization has a well-formed window (periodEnd >= periodStart);
• L3 executor gate (post-fix): with SETTLEMENT_EXECUTOR configured, only that executor can consume the cap (the open replay path is blocked);
• a zero-amount draw is rejected. Negative controls (SAT, all fired): drop the cap check -> authorizes over-cap; drop the expiry check -> authorizes an expired mandate; drop the L3 executor gate -> a non-executor drains a configured mandate's cap. All three requested controls present (cap, expiry, plus the L3 gate control). Caveat / [VERIFY]: the Falcon-512 validity bit is the live precompile 0x0AE1 (trusted primitive, not re-proved); mandateHash chain/contract binding and keccak256 injectivity are [VERIFY]; the contract holds NO funds (cap is accounting, the AERE402 rail moves value); unbounded-Int design abstraction, DESIGN-level not bytecode. The open path (executor == 0) is verification/test only per the contract's documented L3; the model proves the configured executor closes the vector.

b. reputation_gate_smt.py (AereReputationRegistry8004, M1 fix) -- 5 PROVED / 2 CEX-FOUND, exit 0

Invariant modelled: M1 FORWARD-SAFETY, a forwarded attestation happens => (author authorized) AND (delta in {-1,0,+1}). Proved (UNSAT): only an authorized feedback author can move a score (G0, the M1 gate); a forwarded delta is clamped to {-1,0,+1} (G2, no arbitrary value set); the composite M1 property (a score move requires an authorized author AND a clamped unit delta); feedback requires a registered agent (G1); forwarding requires the adapter to be a live attestor (G3). Negative controls (SAT, both fired): drop the author gate -> anyone drives an agent's score (this reproduces the exact M1 bug); drop the delta clamp -> an arbitrary reputation delta is forwarded. Honest caveat: this is the lightest of the four; its authorization half overlaps the Hardhat test "gates giveFeedback to owner-authorized feedback authors (M1)". The z3 value-add is the composite invariant plus the firing non-vacuity control, and the delta-clamp arithmetic bound. The live AereAIReputation computes the score FROM the delta; the model bounds only what the adapter forwards (authorized + clamped), not the live contract's score formula. Included because the task explicitly requested it AND the clamp bound + firing M1 control make it non-vacuous, not coverage-theater.

c1. vectorstore_smt.py (AereVectorStore) -- 8 PROVED / 3 CEX-FOUND, exit 0

Invariants modelled: VERSION MONOTONICITY, APPEND-ONLY history, retrieval-against-a-committed-version, one-shot receipt. Proved (UNSAT): a commit increments version by exactly one (version = s.version + 1); version strictly increases; commitCount strictly increases; the version history is append-only (a committed root can never be rewritten); every attestation names a committed version 1..current (CV); vector-inclusion is only checked against a committed version (CV2); a priced receipt is consumed at most once (R1); only the bound provider may consume a receipt (R2, the L2 fix). Negative controls (SAT, all fired): drop the version bound -> attest against an uncommitted version; drop append-only -> overwrite a committed root; drop the one-shot guard -> double-spend one paid receipt. Caveat / [VERIFY]: post-quantum commit AUTHENTICITY is the live precompile 0x0AE1 (fail-closed, trusted); the AERE402 facilitator settlement in paidQuery is an external trusted rail (this model covers the receipt STATE machine, not the token movement); Merkle inclusion rests on keccak256 / OZ MerkleProof soundness. This satisfies the task's "check AereVectorStore version monotonicity" item.

c2. bitstring_status_smt.py (AereBitstringStatusList) -- 6 PROVED / 2 CEX-FOUND, exit 0

Invariants modelled: REVOCATION-BIT MONOTONICITY (terminal), no silent no-op, epoch monotonicity, bit-frame isolation. Proved (UNSAT): on a Revocation list a status bit is monotone, the only enabled transition is 0 -> 1 (RM), so a revoked credential can never be un-revoked; an enabled revocation transition always starts from an unset bit (RM2); every recorded mutation is a real change (NS); only the controller can write (CTRL); the epoch strictly increases on every mutation (EP, the freshness anchor); setting one bit leaves every other credential's bit unchanged (FR, frame isolation). Negative controls (SAT, both fired): drop the terminal guard -> a Revocation list clears a bit (un-revoke); drop the bit mask -> flip a neighbouring credential's bit while setting one. Caveat: Suspension lists are intentionally reversible, so the monotonicity property is asserted only for Revocation lists. The zk non-revocation path (verifyNonRevocation + SP1 circuit) is [MEASURE] (circuit pending, fail-closed off until configured); its codeless-verifier L1 guard and fail-closed binding are covered by the aere-pq-screen Hardhat tests, not modelled here. This satisfies the task's "AereBitstringStatusList status-bit monotonicity of revocation" item.

Contracts deliberately NOT modelled (honesty over coverage-theater)

Per the task's own guidance, these have key properties that are access-control / fail-closed / precompile-return-handling, already covered by their Hardhat tests (and, where applicable, Halmos symbolic). A z3 arithmetic model would be vacuous:

• AereIdentityRegistry8004: register is gated to the agent's current controller; resolve/getAgent are pass-through reads. Pure access-control. Covered by test/erc8004-adapters.test.js.
• AereValidationRegistry8004: respondValidation is fail-closed PQC-return handling (reverts on an invalid Falcon-512 / ML-DSA-44 proof) plus a one-shot Pending -> Completed status and a request nonce used only for id derivation. Its structural invariants (fail-closed verify, record-once, monotone nonce) are already the exact shapes proved by recovery_registry_smt and credential_ registry_smt, and it is covered by erc8004-adapters.test.js. Not forced.
• AereRandomnessBeaconV2: precompile-return-handling / fail-closed (task explicitly lists it).
• AerePQAggregateModule and the L1 fix on AerePQAggregateVerifier: the t-of-n authorization is already covered by pqaggregate_smt.py; the L1 fix itself is a codeless-gateway constructor guard (fail- closed), covered by the AerePQAggregate.test.js "rejects a code-less SP1 gateway at construction" test. Not arithmetic.
• The other L1 codeless-verifier constructor guards (AereComputeMarketV3, AereBitstringStatusList): fail-closed constructor guards covered by the AereComputeMarketV3 and aere-pq-screen Hardhat tests; not arithmetic. (ComputeMarketV3's escrow arithmetic is already modelled by computemarket_smt.py; BitstringStatusList's real arithmetic is the revocation monotonicity modelled above, not the L1 guard.) Also, within the modelled contracts, the precompile-return / access-control halves (AP2 Falcon verification, VectorStore L2 provider-binding) are noted as test/precompile-trust covered; the z3 models only the genuine arithmetic/state halves.

PART 2: canonical runner new totals and REPRODUCE.md

All four new models wired into aerenew/formal-consensus/run_consensus_verification.py CONTRACT_MODELS (existing 15 entries kept intact). Fresh canonical run on 2026-07-19:

models run: 19   passed: 19   (8 consensus + 11 contract)
verdict lines: 156 PROVED   89 CEX-FOUND   0 FAILED
RESULT: ALL MODELS PASS (proofs PROVED, negative controls fired)     exit 0

Delta from the previous 15-model run (128 PROVED / 79 CEX-FOUND): +28 PROVED, +10 CEX-FOUND, exactly the four new models' contribution (ap2_mandate 9/3, reputation_gate 5/2, vectorstore 8/3, bitstring_status 6/2).

REPRODUCE.md section 3b updated to the real fresh count: "19 models: 8 consensus + 11 contract", the tally "156 PROVED, 89 CEX-FOUND, 0 FAILED", the four newly-added models named with their one-line invariants and per-model verdict-line contributions, and the [VERIFY] boundary note extended to the ERC-8004 mandate / reputation adapters (the model bounds the adapter's guard logic and accounting, not the AERE402 rail's token movement or the live reputation's score formula). No stale "15 models" or "128 PROVED" counts remain; no em-dashes or "--" in the prose.

Files added / changed

• NEW aerenew/formal-consensus/ap2_mandate_smt.py
• NEW aerenew/formal-consensus/reputation_gate_smt.py
• NEW aerenew/formal-consensus/vectorstore_smt.py
• NEW aerenew/formal-consensus/bitstring_status_smt.py
• EDIT aerenew/formal-consensus/run_consensus_verification.py (4 entries appended to CONTRACT_MODELS)
• EDIT aerenew/REPRODUCE.md (section 3b: 15 -> 19 models, 128/79 -> 156/89, named the new models)