# Formally analysed properties — AERE PQC contracts

Symbolic execution with **halmos 0.3.3** (Z3 4.12.6) over **Solidity 0.8.23** builds
of the **LIVE** contracts:

- `contracts/pqc/AerePQCAttestation.sol` (deployed mainnet 2800 at
  `0x465d9E3b476BF98Aa1393079e240Db5D2a9bEA6A`)
- `contracts/pqc/AereCryptoRegistry.sol`

This is an **additive** Foundry + halmos layer beside the existing Hardhat project.
It compiles only the two contracts under analysis (+ OpenZeppelin `Ownable` and a
tiny cheatcode shim) into its own `out-forge/` / `cache-forge/`; the Hardhat build
(`artifacts/`, `cache/`) and the Hardhat test suite are untouched.

> **Scope disclaimer.** "Proven" below means: *halmos found no counterexample to the
> stated assertion, within the stated bounds and assumptions.* It is **not** a claim
> that the contracts are "formally verified" in general. Only the specific properties
> and bounds listed here were checked. The cryptographic soundness of the PQC
> precompiles is explicitly **out of scope** (see the oracle assumption).

## How to reproduce

```bash
# from contracts/  (foundry.toml is here)
forge build                       # sanity compile (skips legacy stack-too-deep verifiers)

# Suite 1 — AerePQCAttestation
halmos --forge-build-out out-forge --contract AerePQCAttestationSymbolic \
       --default-bytes-lengths "0,32,65,897,1312,1793" --loop 4

# Suite 2 — AereCryptoRegistry
halmos --forge-build-out out-forge --contract AereCryptoRegistrySymbolic \
       --loop 12 --default-bytes-lengths "0,65"
```

Note: if you run a plain `forge build` immediately before halmos it can strip the
AST from `out-forge/`; delete `out-forge/ cache-forge/` and let halmos rebuild
(it invokes `forge build --ast` itself).

## Toolchain provenance (honest note)

halmos pulls `eth-hash[pysha3]` → `safe-pysha3`, a C extension with no wheel for the
host Python and no MSVC available. It was satisfied with a **pure-Python keccak shim
backed by pycryptodome**, verified against the known-answer empty-input digest
(`c5d2460186f7233c927e7db2dcc703c0e500b653ca82273b7bfad8045d85a470`). This only
affects keccak *inside the Python tooling*; the contracts' own keccak is modelled by
halmos itself (see keccak assumption). Foundry `forge` 1.7.1; solc 0.8.23 via svm.

---

## Latest run (both suites PASS)

```
Running 3 tests for test/formal/AerePQCAttestation.symbolic.t.sol:AerePQCAttestationSymbolic
[PASS] check_noOverwriteAcrossTwoAttests(bytes32,bytes32,bytes,bytes) (paths: 1)
[PASS] check_nonceAndStateMoveOnlyOnSuccess(bytes32,bytes,bytes32)   (paths: 10)
[PASS] check_registerKeyRejectsMalformedPubKey(uint8,bytes)          (paths: 33)
Symbolic test result: 3 passed; 0 failed

Running 4 tests for test/formal/AereCryptoRegistry.symbolic.t.sol:AereCryptoRegistrySymbolic
[PASS] check_resolveActiveTerminatesAndReturnsActive(uint256)        (paths: 50)
[PASS] check_revokedOrUnknownNeverVerifies(uint256,bytes,bytes32,bytes) (paths: 686)
[PASS] check_setStatusIsOwnerOnly(address,uint256,uint8)             (paths: 6)
[PASS] check_setSuccessorIsOwnerOnly(address,uint256,uint256)        (paths: 5)
Symbolic test result: 4 passed; 0 failed
```

A deliberately-false negative control (`nonce increments by 2`) was run separately and
halmos **did** return a counterexample, confirming the assertions above are not
vacuously passing.

---

## AerePQCAttestation

| # | Property | Test | Status |
|---|----------|------|--------|
| P1 | A key's nonce increases by **exactly 1** on a successful `attest`, and is **unchanged** on any non-successful `attest`. `attestationCount` moves in lock-step. | `check_nonceAndStateMoveOnlyOnSuccess` | **PASS** |
| P2 | An attestation slot `(keyId, nonce)` is written **at most once** (no overwrite): two consecutive successful attests land in **distinct** slots and the first slot's record is not mutated by the second. | `check_noOverwriteAcrossTwoAttests` | **PASS** |
| P3 | A reverting / failed `attest` leaves **all** observable state unchanged (nonce, `attestationCount`, and the target attestation slot). | `check_nonceAndStateMoveOnlyOnSuccess` (the `!ok` branch) | **PASS** |
| P4 | `registerKey` **rejects malformed pubKeys**: registration succeeds **only** for a `(scheme, length, header)` triple matching the scheme's spec; an unknown scheme can never register. | `check_registerKeyRejectsMalformedPubKey` | **PASS** |

## AereCryptoRegistry

| # | Property | Test | Status |
|---|----------|------|--------|
| R1 | **Fail-closed**: a **REVOKED** or **UNKNOWN** algorithm id can **never** pass `verify()`, for any pubkey/message/signature and regardless of what the routed verifier would return. | `check_revokedOrUnknownNeverVerifies` | **PASS** |
| R2 | Status transitions are **owner-only**: a non-owner `setStatus` (and `setSuccessor`) call cannot change registry state. | `check_setStatusIsOwnerOnly`, `check_setSuccessorIsOwnerOnly` | **PASS** |
| R3 | `resolveActive` **terminates** on any symbolic start id (returns an ACTIVE row or reverts), never diverging — including on a deliberately-seeded successor **cycle**. | `check_resolveActiveTerminatesAndReturnsActive` | **PASS** |

---

## Assumptions (these bound the strength of every "PASS" above)

1. **Precompile as an uninterpreted oracle (central).** halmos cannot execute AERE's
   native PQC precompiles (`0x0AE1..0x0AE4`) — they are Bouncy-Castle native code on
   the Besu fork, not EVM bytecode. The tests **etch a 1-slot EVM stub** at the scheme's
   precompile address and drive its 32-byte return word with a **symbolic** value, so
   halmos explores both the "precompile says valid" and "precompile says invalid"
   branches on every call. This is *strictly more adversarial* than a faithful
   precompile: the safety properties are shown to hold no matter what the precompile
   returns. It proves **nothing** about Falcon/ML-DSA/SLH-DSA cryptographic soundness —
   that is covered elsewhere (NIST KAT vectors + live `eth_call` checks), not here.

2. **keccak injectivity.** halmos models `keccak256` as an injective, collision-free
   function (its default). P2's "distinct `(keyId, nonce)` ⇒ distinct storage slot"
   rests on this. This matches standard EVM verification practice.

3. **Bounded symbolic `bytes` lengths.** Dynamic `bytes` parameters are explored only
   at the lengths passed via `--default-bytes-lengths`:
   - Suite 1 used `0,32,65,897,1312,1793` — this **covers the exact valid pubkey
     lengths of all four schemes** (897 Falcon-512, 1793 Falcon-1024, 1312 ML-DSA-44,
     32 SLH-DSA-128s) plus invalid lengths, so P4's accept/reject boundary is genuinely
     exercised, not vacuous. Falcon signatures reach the verifier at length 65.
   - Suite 2 used `0,65` (signature content is irrelevant to the fail-closed R1 gate).
   Lengths outside these sets are not explored.

4. **Bounded loop unrolling.** `resolveActive`'s loop is structurally bounded by
   `_count`. R3 was run with `--loop 12` against a registry of `_count = 7` rows
   (5 seeded live schemes + 2 extra rows forming a successor cycle), i.e. the loop is
   unrolled well past its `_count + 1` maximum, so every path terminates within the
   bound. Termination is demonstrated only for `_count ≤ 7`; the argument that it holds
   for all `_count` is the structural loop bound in the source, not an unbounded proof.

5. **Representative key/scheme instantiation.** P1–P3 fix a single registered
   Falcon-512 key (scheme 1). The nonce/slot/record logic in `attest` is
   scheme-independent, so this is a representative instantiation, not a proof quantified
   over all four schemes simultaneously.

6. **Ownership model.** In R2 the test contract is the deployer and hence the `Ownable`
   owner; the symbolic non-owner caller is constrained to differ from it.

7. **EVM revert semantics.** P3 and R2 rely on the EVM rolling back all state on a
   reverted call frame. The proofs additionally confirm the contracts contain no
   assembly path that writes state outside that revert scope.

## What is NOT claimed

- Not "formally verified" as a blanket statement — only P1–P4, R1–R3 within the bounds above.
- No claim about the PQC precompiles' cryptographic correctness (oracle assumption).
- No claim about consensus: AERE consensus remains classical ECDSA QBFT; these are
  application-layer contract properties only.
- No proof for byte lengths / `_count` values outside the enumerated bounds.

---

# z3 SMT DESIGN MODELS (formal-consensus/*.py) — inductive accounting proofs

A second, complementary formal layer sits in `formal-consensus/`. These are **z3
SMT design models** in the style of `formal-consensus/spokepool_smt.py` (the model
that found the real SpokePool bond-accounting bug). Each models a contract's
money/authorization logic as an **inductive transition system** over unbounded
integers (the same abstraction solc's SMTChecker uses by default), proving the key
safety invariant is **inductive** — base case holds, and every operation preserves
it — and includes **negative controls** that reproduce the corresponding real bug
when a guard is removed (so the proofs are demonstrably non-vacuous).

**Scope:** these check the **DESIGN math** (the accounting/authorization
arithmetic and its guards), NOT the compiled EVM bytecode. They complement the
halmos bytecode-level suites above; they do not replace them.

**Toolchain:** z3 4.16.0 (pip), CPython 3.14. No forge/halmos needed.

**Reproduce (from repo root):**
```bash
python formal-consensus/settlementhub_smt.py       # exit 0 on all-proved
python formal-consensus/lending_liquidation_smt.py
python formal-consensus/agentdid_session_smt.py
python formal-consensus/spokepool_smt.py            # the original reference model
# --- the four LIVE (deployed 2026-07-12) PQC contracts ---
python formal-consensus/pqckeyregistry_smt.py       # AerePQCKeyRegistry 0x1eCa..3691
python formal-consensus/hybridauthorizer_smt.py     # AereHybridAuthorizer 0x168F..82E0
python formal-consensus/agentdid_lifecycle_smt.py   # AereAgentDID 0xce64..22C5 (root lifecycle)
python formal-consensus/cryptoregistry_smt.py       # AereCryptoRegistry 0xaE6f..baa5 (re-confirm)
```

## LIVE PQC contracts, formally analysed 2026-07-12 (z3 4.16.0, CPython 3.14)

The four PQC contracts deployed to mainnet 2800 on 2026-07-12, each modelled as an
inductive/logical transition system with FIRING negative controls (buggy variant's
violation is `sat`), so every PROVED is demonstrably non-vacuous. `forge`/`halmos`
are not installed in this environment; these z3 DESIGN models are the runnable proof
here and complement (do not replace) the halmos BYTECODE suites above.

### AerePQCKeyRegistry (`0x1eCa3c5ADcBD0b22636D8672b00faC6D89363691`) — `pqckeyregistry_smt.py`

| # | Property | Result |
|---|----------|--------|
| K1 | Cross-identity PoP replay impossible: the challenge binds `owner`, so a PoP for O cannot be one for O'≠O | **PROVED** |
| K2 | Same-identity replay impossible: nonce is in the challenge and advances `n→n+1` before store | **PROVED** |
| K3 | A **REVOKED** (or NONE) key **never** verifies via `verifyWithKey`, for any precompile output | **PROVED** |
| K4 | **Rotation preserves the owner binding** (`successor.owner == predecessor.owner`); old leaves ACTIVE | **PROVED** |
| NC1–4 | owner-less challenge (cross-identity replay), nonce-less challenge (same-identity replay), missing-REVOKED gate, arbitrary-owner rotate | **CEX** (all fire) |

Assumptions: **A1 signature-soundness** (precompile accepts only a genuine signature over the exact message — out of scope, NIST-KAT/eth_call elsewhere); **A2 keccak injectivity**; design model, not bytecode.

### AereHybridAuthorizer (`0x168F2A6a3071e7654CF1784a6f5d7BC8e1a582E0`) — `hybridauthorizer_smt.py`

| # | Property | Result |
|---|----------|--------|
| H1/H1b | Only an **ACTIVE** scheme authorizes: `resolveActive` returns ONLY an ACTIVE id; a success is verified under it (never REVOKED/DEPRECATED/UNKNOWN) | **PROVED** |
| H2a | A **REVOKED** id with no ACTIVE successor → `resolveActive` reverts → fail-closed false (authorizes nothing) | **PROVED** |
| H2b | A REVOKED id with an ACTIVE successor routes to the **successor**; the revoked id itself never verifies | **PROVED** |
| H3/H3b | `resolveActive` **terminates** within the `_count`-bounded walk (pigeonhole: no acyclic walk of length `_count+1`) | **PROVED** |
| H3c/H3d | **Fail-closed** on every revert; `algorithmFor` (preference-else-default) resolution is total | **PROVED** |
| NC1–4 | skip-resolveActive, status-blind resolver, fail-OPEN consumer | **CEX** (all fire) |

Assumptions: **A1** registry `verify` is itself fail-closed (halmos R1 / `cryptoregistry_smt.py`); **A2** loop bound is the source's structural bound; design model.

### AereAgentDID (`0xce641d7d7C10553D82b06B7C21d423550e7522C5`) — `agentdid_lifecycle_smt.py`

Complements `agentdid_session_smt.py` (spend cap C1, gating C2, anti-replay C3, expiry C4).

| # | Property | Result |
|---|----------|--------|
| D1a/b/c | A session **dies** the instant its Falcon **root is ROTATED/REVOKED** or ceases to be Falcon (liveness re-reads the registry every call; `authorize` records nothing thereafter) | **PROVED** |
| D2a | `revokeSession` is **controller-only** (current registry owner of the root) | **PROVED** |
| D2b | `createAgent` is **root-owner-only** | **PROVED** |
| D2c | Spend is recorded **only** with a valid session-key ECDSA signature (`signer==sessionAddr`) | **PROVED** |
| D3 | Containment envelope: a successful action stays within cap AND within expiry | **PROVED** |
| NC1–3 | cached root-active flag, missing controller gate, missing signature gate | **CEX** (all fire) |

Assumptions: **A1 ecrecover-soundness**; **A2** the liveness check reads the LIVE registry status (no stale cache — this is the fact D1 exploits); design model.

### AereCryptoRegistry (`0xaE6fC596bb3eCcbf5c5D02D67B0Ef065b3Afbaa5`) — `cryptoregistry_smt.py`

Design-level **re-confirmation** of the halmos R1/R3 suite (the bytecode proof in
`AereCryptoRegistry.symbolic.t.sol` remains authoritative).

| # | Property | Result |
|---|----------|--------|
| R1a/b/c | `verify()` is **fail-closed** for REVOKED / UNKNOWN / hash-only rows before any routing, any precompile output | **PROVED** |
| R3a/b/c | `resolveActive` returns **only ACTIVE** and **terminates** (pigeonhole over `_count` rows) | **PROVED** |
| NC1–2 | status-gate-skipping verify, unconditional start-row resolver | **CEX** (both fire) |

### Result (LIVE PQC set)

All stated safety invariants across the four contracts are **inductive / valid under
the modelled guards**; every negative control fires (guards are load-bearing). **No
real counterexample to a should-hold invariant was found.** One benign, non-exploitable
observation: `AereAgentDID.authorize`'s overflow guard `s.spent + amount < s.spent` is
**dead code** under Solidity-0.8 checked arithmetic (the addition reverts before the
comparison can be true) — it fails **safe** (revert = no state change), so it is a
redundancy, **not a defect**. Consensus is unaffected: AERE remains classical ECDSA
QBFT; these are application-layer contract properties only. "Proven" means only the
specific properties + bounds + assumptions listed — **not** "formally verified" as a
blanket claim.

## AereSettlementHubV2 — `settlementhub_smt.py`

Contract: `contracts/settlement/AereSettlementHubV2.sol`. Invariant
**`INV := balanceOf(hub) ≥ committedLiabilities[asset]`** (solvency / no-theft: a
permissionless `sweepResidual` can only ever move un-owed surplus, and
`settle`/`cancelIntent` can always pay out).

| # | Property | Result |
|---|----------|--------|
| S-base | fresh hub (0,0) satisfies INV | **PROVED** (unsat) |
| S1 | `deposit()` (pull amount, route fee, commit **amountAfterFee**) preserves INV | **PROVED** |
| S2 | `depositSolverBond()` preserves INV | **PROVED** |
| S3 | `slashSolverBond()` preserves INV (sink accepts OR rejects) | **PROVED** |
| S4 | `settle()` preserves INV | **PROVED** |
| S5 | `cancelIntent()` preserves INV | **PROVED** |
| S6 | `sweepResidual()` (bounded by `residualOf = bal − committed`) preserves INV | **PROVED** |
| NC1 | V1 unbounded sweep (bound = balance, ignores committed) **steals owed funds** | **CEX** (sat) |
| NC2 | buggy deposit committing the **full** amount (not amountAfterFee) **over-commits** | **CEX** (sat) |

## AereLendingMarket.liquidate — `lending_liquidation_smt.py`

Contract: `contracts/lending/AereLendingMarket.sol` (the `liquidate` seize/clamp
math, modelled at 18/18 decimals — see assumption A1 in the file).

| # | Property | Result |
|---|----------|--------|
| L1 | clamped `seize ≤ collateral` (no over-seize / no `collateralOf` underflow) | **PROVED** |
| L2 | insolvent-clamp branch: `value(pay) ≤ value(collateral seized)` (liquidator never overpays) | **PROVED** |
| L3 | non-clamp branch: `value(received) ≤ valueToSeize` (no over-seize of VALUE) | **PROVED** |
| L4 | `repaidScaled` (clamped to `debtOf`) `≤ debtOf` (debt bookkeeping no-underflow) | **PROVED** |
| — | `scaleDown` floor-division monotonicity (supports A1) | **PROVED** |
| L3-note | reverse direction `value(received) ≥ value(paid)` fails by ≤ wei-dust that rounds **toward the protocol** (the SAFE direction) — expected DeFi rounding, **NOT a bug** | demonstrated (sat, dust = 1 wei) |
| NC1 | **without** the clamp, `seize` can exceed collateral → theft of pooled collateral | **CEX** (sat) |
| NC2 | buggy clamp that **inflates** the reduced pay (`×(10000+bonus)/10000`) makes the liquidator **overpay** | **CEX** (sat) |

## AereAgentDID — `agentdid_session_smt.py`

Contract: `contracts/pqc/AereAgentDID.sol` (session `authorize` / gating /
anti-replay). Invariant **`spent ≤ spendCap`** plus the containment gates.

| # | Property | Result |
|---|----------|--------|
| C-base | freshly issued session (`spent = 0 ≤ cap`) | **PROVED** |
| C1 | `authorize()` preserves the **cumulative** spend cap `spent ≤ cap` (inductive) | **PROVED** |
| C2 | a non-live session (revoked / expired / root-inactive) can **never** record spend | **PROVED** |
| C3 | `actionNonce` strictly increases each success → no signature replay | **PROVED** |
| C4 | expiry is terminal (`now > expiry` stays true as time advances) | **PROVED** |
| NC1 | a **per-action** cap check (instead of cumulative) lets total spend exceed the cap | **CEX** (sat) |
| NC2 | omitting the liveness gate lets a **revoked** session record spend | **CEX** (sat) |

### Assumptions bounding these z3 models (honest)

- **Design math, not bytecode.** Unbounded `Int`; Solidity-0.8 checked arithmetic
  is modelled as "underflow/overflow reverts (no state change)". No claim about
  256-bit overflow beyond the explicit source guards, and no claim about the
  compiled bytecode (that is the halmos layer's job).
- **Standard ERC20** for the settlement hub (`transferFrom`/`transfer` move exactly
  `amount`). **Fee-on-transfer / rebasing tokens are OUT OF SCOPE** and would break
  the solvency invariant of any escrow — excluded by the asset-listing policy.
- **Trusted `AereSink`** (pulls at most the approved amount; `flush` either succeeds
  or reverts).
- **Lending decimals normalised to 18/18** for tractability; the `_scaleUp`/
  `_scaleDown` helpers are pure power-of-ten mul/div whose floor rounding is proven
  monotone and only shrinks the liquidator's charge (strengthening L2). Oracle
  price staleness/deviation is enforced upstream by `AereLendingOracle` and is out
  of scope here.
- **`ecrecover` is a sound signature oracle** for AereAgentDID (its cryptographic
  soundness is out of scope, same class as the halmos precompile-oracle assumption);
  the cap/nonce/gating proofs hold regardless of what it returns.

### Result

No real counterexample was found in any of the three contracts: every stated
safety invariant is **inductive under the modelled guards**, and all negative
controls fire as expected (confirming the guards are load-bearing). The only `sat`
result on a "should-hold" phrasing was the AereLendingMarket **L3-note**, which is
a **1-wei rounding-dust** discrepancy in the protocol-favouring (safe) direction —
documented above as expected DeFi rounding, **not a defect**. Consensus is
unaffected: AERE remains classical ECDSA QBFT; these are application-layer
contract properties only.