# Spec 21: Certora formal-verification specifications for Aere Network's safety-critical contracts Status date: 2026-07-19. Author: Aere Network engineering (self-authored CVL). ## HONEST STATUS BANNER (read first) This document contains **written-and-ready** Certora Verification Language (CVL) specifications. It does **not** contain proof results. Every CVL rule and invariant here is authored against the real contract source in this repository, but **none has been executed by the Certora Prover**, so **nothing in this document is claimed "proved."** Running these specs requires the Certora Prover, which is an external tool: - Free tier available at `prover.certora.com` (needs an account). - Local driver is the `certora-cli` Python package (`pip install certora-cli`), which uploads the job to Certora's cloud solver back end. - The prover is **not installed or run in this environment.** Wherever a proof result would go, this document writes a `[MEASURE]` marker naming the exact command to run and the artifact to publish. A rule graduates from "written" to "proved" only after `certoraRun` returns `Verified` for it and the HTML rule report is published. Until then the correct description is **"CVL authored, not yet run."** Scope boundary preserved throughout: these are **application / account / tokenomics-layer** contracts. Aere Network consensus remains classical ECDSA QBFT (Besu). No rule here asserts post-quantum consensus; the PQC content is signature verification and key custody at the contract layer only. --- ## 1. Why Certora, and how it complements the existing formal work Aere already runs two layers of machine-checked reasoning: | Layer | Tool | What it checks | Where it lives | |---|---|---|---| | Design-level SMT | z3 (Python) | Property holds over an abstract model of the contract logic (guards, arithmetic, status machine) | `aerenew/formal-consensus/*_smt.py` | | Symbolic bytecode | Halmos / forge | Property holds over the compiled EVM bytecode for symbolic inputs, bounded | `aerenew/formal-contracts/specs/*.symbolic.t.sol`, `aerenew/contracts/test/formal/*.symbolic.t.sol` | | Property fuzzing | Foundry / Medusa | Property survives large random input campaigns (sampling) | `aerenew/contracts/test/**` | Fuzzing **samples** the input and state space. It runs a property against many concrete inputs and reports the ones it happened to try. A clean fuzz run is strong evidence, but it is evidence about the paths that were sampled, not a statement about the paths that were not. The Certora Prover is different in kind. It compiles the contract to a logical transition system and asks an SMT solver whether the negation of a rule is satisfiable **over all inputs and all reachable states** (subject to declared loop bounds and summaries). A rule that verifies is a statement that no input, in no ordering, from no reachable state, can violate the property. A rule that fails returns a concrete counterexample transaction. Certora sits above the existing work rather than replacing it: - It shares the z3 models' **property statements** (the "what to prove"), which is why this document reuses the invariants already written in `threshold_account_smt.py`, `cryptoregistry_smt.py`, and `pqckeyregistry_smt.py` verbatim as the source of truth, now expressed in CVL. - Unlike the z3 models, which reason over a hand-built abstraction, CVL rules are checked against the **actual compiled contract**, closing the gap the z3 files honestly flag as their own boundary ("a design model, not the Solidity bytecode"). - Unlike Halmos, which is symbolic-execution based and bounded per call, the Certora Prover reasons inductively across an arbitrary method sequence via `invariant` and parametric `rule` constructs, and gives first-class support for `ghost` state and storage `hook`s. The three tools are complementary: z3 fixes the property at design time, Halmos and Certora both check it against bytecode (Halmos by bounded symbolic execution, Certora by inductive SMT over all methods), and fuzzing provides cheap continuous regression coverage. --- ## 2. Target contracts and the properties to prove Each subsection: (1) the real interface as read from source, with file path and the exact state variables / function signatures the CVL binds to, then (2) the CVL rules and invariants. Convention in the CVL: `env e` is the calling environment, `mathint` is the unbounded integer sort (used to make arithmetic assertions overflow-free), `currentContract` is the contract under verification, and `nativeBalances[a]` is the native-AERE balance of address `a`. A `using X as y` line links a second contract (for example the ERC-20 asset) so its storage is observable inside a rule. --- ### 2.a Burn stack #### 2.a.1 `AereSink` (immutable 3-bucket router) Source: `aerenew/contracts/contracts/sink/AereSink.sol`. Read confirms: - `is ReentrancyGuard` only. **No `Ownable`, no admin role, no setters** (`grep` for `onlyOwner`, `setBucket`, `setRecipient` returns nothing; the NatSpec asserts this and the source matches). - Immutable state (each exposed by an auto getter): `address AERE`, `address BURN_VAULT`, `address SAERE_VAULT`, `address DEX_ROUTER`, `uint16 BURN_BPS`, `uint16 BUYBACK_BPS`, `uint16 STAKER_YIELD_BPS`, `uint16 MAX_SLIPPAGE_BPS`, `address ORACLE`. - Constructor reverts with `BpsMustSumTo10000` unless `BURN_BPS + BUYBACK_BPS + STAKER_YIELD_BPS == 10000`. - Mutating entrypoints: `flush(address token, uint256 amount)`, `sweepDust(address token)`. In the `token == AERE` branch both dispatch only to `BURN_VAULT` and `SAERE_VAULT` via `_safeTransfer`; the `token != AERE` branch routes the same two addresses through `_swapAndForward`, where `recipient` is only ever `BURN_VAULT` or `SAERE_VAULT` (proven set by inspection). Properties (matching the z3 / Halmos SK-series and the SECURITY-POSTURE "no path sends to an arbitrary address" statement): ```cvl // certora/specs/AereSink.spec using DummyERC20A as aere; // the AERE / WAERE asset, linked so its balances are observable methods { function BURN_BPS() external returns (uint16) envfree; function BUYBACK_BPS() external returns (uint16) envfree; function STAKER_YIELD_BPS() external returns (uint16) envfree; function BURN_VAULT() external returns (address) envfree; function SAERE_VAULT() external returns (address) envfree; function DEX_ROUTER() external returns (address) envfree; function AERE() external returns (address) envfree; function aere.balanceOf(address) external returns (uint256) envfree; } // SK-INV-1 the three bucket splits always sum to exactly 10000 basis points. // Immutable, so the constructor's BpsMustSumTo10000 guard is the whole proof; the // invariant asserts no reachable state breaks it. invariant bpsSumTo10000() to_mathint(BURN_BPS()) + to_mathint(BUYBACK_BPS()) + to_mathint(STAKER_YIELD_BPS()) == 10000; // SK-INV-2 the bucket recipients can never be redirected: no method changes the // immutable BURN_VAULT / SAERE_VAULT addresses. This is the "no owner/admin can // redirect funds" property expressed as an all-methods parametric rule. rule recipientsImmutable(method f, env e, calldataarg args) { address burnBefore = BURN_VAULT(); address saereBefore = SAERE_VAULT(); f(e, args); assert BURN_VAULT() == burnBefore, "BURN_VAULT is immutable"; assert SAERE_VAULT() == saereBefore, "SAERE_VAULT is immutable"; } // SK-RULE-3 NO ARBITRARY RECIPIENT: a flush of AERE never increases the AERE // balance of any address that is not one of the fixed buckets, the router, or the // sink itself. There is no code path that pays a caller-chosen address. rule noFundsToArbitraryAddress(env e, uint256 amount, address stranger) { require stranger != BURN_VAULT(); require stranger != SAERE_VAULT(); require stranger != DEX_ROUTER(); require stranger != currentContract; mathint before = aere.balanceOf(stranger); flush(e, AERE(), amount); mathint after = aere.balanceOf(stranger); assert after <= before, "flush must never credit an address outside the immutable bucket set"; } // SK-RULE-4 same guarantee for the permissionless sweepDust path. rule sweepDustNoArbitraryAddress(env e, address stranger) { require stranger != BURN_VAULT(); require stranger != SAERE_VAULT(); require stranger != DEX_ROUTER(); require stranger != currentContract; mathint before = aere.balanceOf(stranger); sweepDust(e, AERE()); assert aere.balanceOf(stranger) <= before; } ``` Note on the token != AERE branch: `_swapAndForward` calls out to `DEX_ROUTER`, an external address. Certora leaves the router call to its default havoc, which conservatively allows the router to move funds however it likes; the CVL above therefore restricts SK-RULE-3/4 to the `token == AERE` direct-settle branch (no external callback), exactly the branch the Halmos SK-series covers. The router branch is argued by inspection (identical `recipient` set) and is a `[MEASURE]` extension: add a `DISPATCHER` summary for `IAereV2Router.swapExactTokensForTokens` that forwards only to `recipient`. #### 2.a.2 `AereCoinbaseSplitterV2` Source: `aerenew/contracts/contracts/AereCoinbaseSplitterV2.sol`. Read confirms: - `is Ownable, ReentrancyGuard`. Mutable `uint256 burnBps` (default 3750), `uint256 sinkBps` (default 1500). - Constants: `BPS = 10000`, `MAX_BURN_BPS = 5000`, `MAX_SINK_BPS = 3000`, `SINK_CHANGE_TIMELOCK = 7 days`. - `setBps(uint256 _burnBps, uint256 _sinkBps)` is `onlyOwner` and reverts `BpsOutOfRange` unless `_burnBps <= MAX_BURN_BPS`, `_sinkBps <= MAX_SINK_BPS`, and `_burnBps + _sinkBps <= BPS`. - `rebateBps()` view returns `BPS - burnBps - sinkBps` (derived, so it must stay non-negative). ```cvl // certora/specs/AereCoinbaseSplitterV2.spec methods { function burnBps() external returns (uint256) envfree; function sinkBps() external returns (uint256) envfree; function BPS() external returns (uint256) envfree; function MAX_BURN_BPS() external returns (uint256) envfree; function MAX_SINK_BPS() external returns (uint256) envfree; function owner() external returns (address) envfree; } // CS-INV-1 burnBps is capped at MAX_BURN_BPS (5000) in every reachable state. // This is the on-chain form of "validator-reward burn cut, hard-capped at 50%". invariant burnBpsWithinCap() burnBps() <= MAX_BURN_BPS(); // CS-INV-2 sinkBps is capped at MAX_SINK_BPS (3000). invariant sinkBpsWithinCap() sinkBps() <= MAX_SINK_BPS(); // CS-INV-3 burn + sink never exceed the total, so the derived rebateBps // (BPS - burnBps - sinkBps) can never underflow / go negative. invariant burnPlusSinkWithinTotal() to_mathint(burnBps()) + to_mathint(sinkBps()) <= to_mathint(BPS()); // CS-RULE-4 only the owner can move the bps, and only within the caps. Any method // that changes burnBps or sinkBps must be called by the owner and must land inside // the caps (so no path, owner or not, exceeds MAX_BURN_BPS). rule onlyOwnerChangesBpsWithinCaps(method f, env e, calldataarg args) { uint256 b0 = burnBps(); uint256 s0 = sinkBps(); f(e, args); bool changed = (burnBps() != b0) || (sinkBps() != s0); assert changed => e.msg.sender == owner(), "only owner may change bps"; assert burnBps() <= MAX_BURN_BPS(), "post-state respects the burn cap"; assert to_mathint(burnBps()) + to_mathint(sinkBps()) <= to_mathint(BPS()); } ``` #### 2.a.3 `AereFeeBurnVault` Source: `aerenew/contracts/contracts/AereFeeBurnVault.sol`. Read confirms: - No `Ownable`, no admin. Functions: `receive()`, `burn()` (payable), `burnToken(address,uint256)`, `sweepToZero()`, `currentAEREBalance()` view. **There is no `withdraw`, no `rescue`, no admin escape.** - `uint256 totalBurnedAERE` increments on every native inflow; `uint256 totalSentToZero` increments in `sweepToZero`; `mapping(address => uint256) totalBurnedToken`. - `sweepToZero()` sends the whole native balance to `address(0)` (the burn sink) and to nowhere else. ```cvl // certora/specs/AereFeeBurnVault.spec methods { function totalBurnedAERE() external returns (uint256) envfree; function totalSentToZero() external returns (uint256) envfree; } // FB-INV-1 the lifetime burn counter is monotonic non-decreasing (it is a running // total of arrivals; no path decrements it). rule totalBurnedMonotonic(method f, env e, calldataarg args) { mathint before = totalBurnedAERE(); f(e, args); assert to_mathint(totalBurnedAERE()) >= before; } // FB-RULE-2 NO WITHDRAW PATH: the vault's own native balance is monotonic // non-decreasing for EVERY method except sweepToZero. sweepToZero is the only // method that can reduce the balance, and (FB-RULE-3) it can only send to the burn // sink (address(0)), never to a caller-chosen address. rule balanceMonotonicExceptBurnSink(method f, env e, calldataarg args) filtered { f -> f.selector != sig:sweepToZero().selector } { mathint before = nativeBalances[currentContract]; f(e, args); assert nativeBalances[currentContract] >= before, "no non-sweep method may reduce the vault balance (there is no withdraw)"; } // FB-RULE-3 the only sink is address(0): sweepToZero credits no non-zero address. // (address(0) is the burn destination; every other account's balance is untouched // or reduced, never increased by the vault's operation.) rule sweepGoesOnlyToBurnSink(env e, address r) { require r != 0; // any real, non-burn address require r != currentContract; mathint before = nativeBalances[r]; sweepToZero(e); assert nativeBalances[r] <= before, "sweepToZero must not credit any address other than the address(0) burn sink"; } ``` `[MEASURE: run certoraRun certora/conf/burnstack.conf and publish the AereSink / AereCoinbaseSplitterV2 / AereFeeBurnVault rule report]` --- ### 2.b Tokenomics: `sAERE` (ERC-4626 staking receipt) Target the corrected `sAEREv2`. Source: `aerenew/contracts/contracts/staking/sAEREv2.sol` (the R7-fixed redeploy; the live `sAERE` at `0xA212...50b0` shares the same interface but not the R7 fix, see the note on SR-RULE-3). Read confirms: - `is ERC4626`. **No admin / owner / pause / upgrade proxy / parameter setters.** Constants `DRIP_DURATION = 7 days`, `DRIP_RESTART_THRESHOLD_BPS = 100`, `DEAD_SHARES_SEED_WAERE = 1000 wei`, `_decimalsOffset() == 6`. - State: `uint256 rewardRate`, `uint256 periodFinish`, `uint256 lastObservedBalance`. - `totalAssets()` returns `syncedBalance - undistributed`, where `syncedBalance = min(assetBalance, lastObservedBalance)` (the R7 fix) and `undistributed = _undistributedNow()`. - `sync()` is permissionless and only observes arrivals; it never moves funds out. Public `deposit`, `mint`, `withdraw`, `redeem` each call `sync()` first, then the OZ super. Properties (donation-inflation resistance, totalAssets consistency, exchange-rate monotonicity under the drip): ```cvl // certora/specs/sAEREv2.spec using DummyERC20A as waere; // the underlying WAERE asset methods { function totalSupply() external returns (uint256) envfree; function totalAssets() external returns (uint256) envfree; function undistributedRewards() external returns (uint256) envfree; function convertToAssets(uint256) external returns (uint256) envfree; function asset() external returns (address) envfree; function waere.balanceOf(address) external returns (uint256) envfree; } // SR-RULE-1 DONATION / INFLATION RESISTANCE: no bare transfer into the vault, and // no sync(), mints shares. Share supply can increase ONLY through deposit or mint. // A raw WAERE.transfer to the vault (the classic ERC-4626 first-depositor inflation // donation) leaves totalSupply untouched. rule noShareMintOnDonationOrSync(method f, env e, calldataarg args) filtered { f -> f.selector != sig:deposit(uint256,address).selector && f.selector != sig:mint(uint256,address).selector } { mathint tsBefore = totalSupply(); f(e, args); assert to_mathint(totalSupply()) <= tsBefore, "only deposit / mint may increase sAERE share supply"; } // SR-INV-2 totalAssets CONSISTENCY: reported assets never exceed the vault's real // WAERE balance (the R7 fix subtracts the undistributed reserve from the SYNCED // balance, so an un-synced donation is never counted early and totalAssets is a // true lower bound on redeemable backing). invariant totalAssetsNeverExceedsBalance() to_mathint(totalAssets()) <= to_mathint(waere.balanceOf(currentContract)); // SR-INV-3 the unvested drip reserve is fully backed: undistributedRewards never // exceeds the real balance (so the reserve can never be double-counted into a // payout, the exact R7 defect that drove totalAssets to 0 in v1). invariant reserveFullyBacked() to_mathint(undistributedRewards()) <= to_mathint(waere.balanceOf(currentContract)); // SR-RULE-4 EXCHANGE-RATE MONOTONICITY UNDER THE DRIP: calling sync() never lowers // the value of a share. With share supply unchanged across the call, the assets a // fixed share amount converts to does not fall. In v2 an arrival folded into the // reserve is rate-neutral at the sync instant (R7) and then vests upward over time; // it never steps down. Running this same rule against the pre-R7 sAERE.sol produces // a counterexample (v1 counts the arrival in totalAssets first, so sync() drops the // rate): that CEX is the R7 bug, which is why sAEREv2 is the verification target. rule syncNeverLowersShareValue(env e, uint256 shareAmt) { require shareAmt > 0; mathint supplyBefore = totalSupply(); mathint assetsPerShareBefore = convertToAssets(shareAmt); sync(e); assert to_mathint(totalSupply()) == supplyBefore, "sync mints/burns no shares"; assert to_mathint(convertToAssets(shareAmt)) >= assetsPerShareBefore, "a share is never worth less after sync (drip is up-only)"; } ``` `[MEASURE: run certoraRun certora/conf/sAEREv2.conf and publish the rule report]`. Note the deliberate demonstration value of SR-RULE-4: it is written to PASS on `sAEREv2.sol` and to FAIL (with a printed counterexample) on the un-fixed `sAERE.sol`, matching the R7 finding in `SECURITY-POSTURE-VERIFICATION-2026-07-15.md`. Do not claim either result until the prover has run both. --- ### 2.c Registries #### 2.c.1 `AereCryptoRegistry` Source: `aerenew/contracts/contracts/pqc/AereCryptoRegistry.sol`. Read confirms: - `is Ownable`. Storage: `mapping(uint256 => Algorithm) _algorithms`, `uint256 _count`, `bool _seeded`. Ids are 1-based and monotonic (`_count += 1` in `_addAlgorithm`, never decremented). - `Algorithm` fields set once at `addAlgorithm` and never rewritten afterward: `name`, `scheme`, `verifier`, `pubKeyLen`, `sigLen`, `esigHeader`, `addedBlock`, `isSignature`. Only `status` (`setStatus`) and `successorId` (`setSuccessor`) are ever mutated post-registration. - `enum Status { UNKNOWN, ACTIVE, DEPRECATED, REVOKED }`. `verify(...)` is fail-closed: returns false (never reverts) for a non-existent id, a hash-only row (`isSignature == false`), or a row whose status is `UNKNOWN` or `REVOKED`, BEFORE the `a.verifier.staticcall`. Properties mirror `cryptoregistry_smt.py` (R1 fail-closed, plus the append-only / no-re-point statements required by the task): ```cvl // certora/specs/AereCryptoRegistry.spec methods { function algorithmCount() external returns (uint256) envfree; function statusOf(uint256) external returns (AereCryptoRegistry.Status) envfree; function owner() external returns (address) envfree; // verify staticcalls an external verifier; leave it to the prover's default // havoc so the fail-closed rules must hold for ANY verifier answer. } // CR-INV-1 algorithm ids are append-only: the count never decreases, so an id that // exists can never be un-registered (rows are added, never removed). rule algorithmCountMonotonic(method f, env e, calldataarg args) { mathint before = algorithmCount(); f(e, args); assert to_mathint(algorithmCount()) >= before; } // CR-RULE-2 NO UNAUTHORIZED RE-POINT: an existing row's verifier address is // immutable. Once a scheme id maps to a verifier, no method (setStatus, // setSuccessor, addAlgorithm of a later id, seedLiveSchemes) can silently rewrite // it. To change a verifier you must add a NEW id; the old id -> verifier binding is // write-once. This is the "recorded entries are append-only, cannot be silently // rewritten" property. rule verifierNeverRepointed(method f, env e, calldataarg args, uint256 id) { require id != 0 && id <= algorithmCount(); AereCryptoRegistry.Algorithm a0 = getAlgorithm(e, id); f(e, args); require id <= algorithmCount(); AereCryptoRegistry.Algorithm a1 = getAlgorithm(e, id); assert a1.verifier == a0.verifier, "verifier address is write-once"; assert a1.scheme == a0.scheme, "scheme tag is write-once"; assert a1.pubKeyLen == a0.pubKeyLen, "pubKeyLen is write-once"; assert a1.sigLen == a0.sigLen, "sigLen is write-once"; assert a1.esigHeader == a0.esigHeader, "wire-format header is write-once"; assert a1.isSignature == a0.isSignature, "signature/hash flag is write-once"; assert a1.addedBlock == a0.addedBlock, "addedBlock is write-once"; } // CR-RULE-3 only the owner can mutate the registry (add / setStatus / setSuccessor // / seed). The onlyOwner modifier reverts otherwise, so a completed mutating call // implies the caller was the owner. rule onlyOwnerMutates(method f, env e, calldataarg args) filtered { f -> f.selector == sig:addAlgorithm(string,uint8,address,uint16,uint32,uint8,uint256,bool).selector || f.selector == sig:setStatus(uint256,AereCryptoRegistry.Status).selector || f.selector == sig:setSuccessor(uint256,uint256).selector || f.selector == sig:seedLiveSchemes().selector } { f(e, args); assert e.msg.sender == owner(), "registry mutation requires owner"; } // CR-RULE-4 FAIL-CLOSED verify (mirrors cryptoregistry_smt.py R1a): a REVOKED id // never verifies, whatever the routed verifier would answer (the status gate short- // circuits before the staticcall, so the prover's havoc of the verifier is // irrelevant). rule verifyFailClosedOnRevoked(env e, uint256 id, bytes pubKey, bytes32 messageHash, bytes signature) { require statusOf(id) == AereCryptoRegistry.Status.REVOKED; bool result = verify(e, id, pubKey, messageHash, signature); assert result == false, "a REVOKED row must never verify"; } // CR-RULE-5 FAIL-CLOSED verify for an UNKNOWN id (R1b): a never-registered id // (id == 0 or id > count) never verifies. rule verifyFailClosedOnUnknown(env e, uint256 id, bytes pubKey, bytes32 messageHash, bytes signature) { require id == 0 || id > algorithmCount(); assert verify(e, id, pubKey, messageHash, signature) == false; } // CR-RULE-6 resolveActive returns ONLY an ACTIVE id (mirrors R3a): if it returns // (does not revert), the returned id's status is ACTIVE. rule resolveActiveReturnsActive(env e, uint256 startId) { uint256 resolved = resolveActive(e, startId); assert statusOf(resolved) == AereCryptoRegistry.Status.ACTIVE, "resolveActive never returns a non-ACTIVE id"; } ``` #### 2.c.2 `AerePQCKeyRegistry` (the PQC key registry) Source: `aerenew/contracts/contracts/pqc/AerePQCKeyRegistry.sol`. Read confirms: - Permissionless (no `Ownable`). Storage: `KeyRecord[] _keys` (append-only; keyId is the array index, pushed in `_registerWithPoP`, never removed), `mapping(address => uint64) identityNonce` (monotonic), `mapping(address => uint256[]) _identityKeys`. - Status constants: `STATUS_NONE=0, STATUS_ACTIVE=1, STATUS_ROTATED=2, STATUS_REVOKED=3`. `revokeKey` is terminal. - `KeyRecord.owner` is set once (`owner: owner` in the push) and never rewritten. `rotateKey` stores the successor with `owner == msg.sender == old.owner`. - `verifyWithKey` is fail-closed: returns false for an unknown key, `STATUS_REVOKED`, or `STATUS_NONE`. Properties mirror `pqckeyregistry_smt.py` K3 (revoked never verifies), K4 (rotation preserves owner), plus the append-only statements: ```cvl // certora/specs/AerePQCKeyRegistry.spec methods { function keyCount() external returns (uint256) envfree; function statusOf(uint256) external returns (uint8) envfree; function ownerOf(uint256) external returns (address) envfree; function schemeOf(uint256) external returns (uint8) envfree; function identityNonce(address) external returns (uint64) envfree; } // KR-INV-1 keys are append-only: keyCount is monotonic non-decreasing, so a // registered keyId is never removed or its slot reused. rule keyCountMonotonic(method f, env e, calldataarg args) { mathint before = keyCount(); f(e, args); assert to_mathint(keyCount()) >= before; } // KR-RULE-2 the owner binding of an existing key is immutable: no method rewrites // an already-registered key's owner (the record's owner field is write-once). This // is the "recorded entries cannot be silently rewritten" property for identities. rule keyOwnerImmutable(method f, env e, calldataarg args, uint256 keyId) { require keyId < keyCount(); address ownerBefore = ownerOf(keyId); uint8 schemeBefore = schemeOf(keyId); f(e, args); assert ownerOf(keyId) == ownerBefore, "a key's owner is write-once"; assert schemeOf(keyId) == schemeBefore, "a key's scheme is write-once"; } // KR-RULE-3 REVOKED is terminal (K3 precondition): once a key is REVOKED it stays // REVOKED across every subsequent method. rule revokeIsTerminal(method f, env e, calldataarg args, uint256 keyId) { require statusOf(keyId) == 3; // STATUS_REVOKED f(e, args); assert statusOf(keyId) == 3, "a REVOKED key can never leave REVOKED"; } // KR-RULE-4 FAIL-CLOSED verifyWithKey on a REVOKED key (mirrors pqckeyregistry_smt // K3): a revoked key never verifies, whatever the precompile would answer. rule verifyWithKeyFailClosedRevoked(env e, uint256 keyId, bytes32 message, bytes signature) { require statusOf(keyId) == 3; // STATUS_REVOKED assert verifyWithKey(e, keyId, message, signature) == false; } // KR-RULE-5 the per-identity PoP nonce is monotonic (K2 backbone): every // registration advances identityNonce, and no method decreases it, so a consumed // proof-of-possession challenge can never recur for the same identity. rule identityNonceMonotonic(method f, env e, calldataarg args, address who) { mathint before = to_mathint(identityNonce(who)); f(e, args); assert to_mathint(identityNonce(who)) >= before; } ``` The K1 / K2 domain-separation results (the PoP challenge binds owner and nonce so a proof cannot be replayed across identities or re-used by the same identity) rest on keccak injectivity. In Certora that is provable by hashing the challenge tuple through the linked `keccak` model and asserting the two challenge preimages differ; it is written as a `[MEASURE]` extension (`AerePQCKeyRegistry_pop.spec`) because it needs the hashing summary set up, and it restates `pqckeyregistry_smt.py` K1/K2 at the bytecode layer. `[MEASURE: run certoraRun certora/conf/registries.conf and publish the AereCryptoRegistry / AerePQCKeyRegistry rule report]` --- ### 2.d Threshold / precompile callers: the duplicate-committee-key fix Source: `aerenew/contracts/contracts/mpc/AereThresholdAccount.sol` (ERC-4337 t-of-n PQC account) and the shared library `aerenew/contracts/contracts/mpc/AerePQCThreshold.sol`. The sibling `AereThresholdPQCRegistry.registerCommittee(uint8,uint8,bytes[])` carries the identical fix. Read confirms: - `initialize(address _entryPoint, uint8 _scheme, uint8 _threshold, bytes[] pubKeys)` is factory-only and one-shot (`AlreadyInitialized` if re-called). It validates `1 <= _threshold <= n <= 255` and, at the one place a committee is ever set, **rejects duplicate public keys**: it hashes each key and reverts `DuplicatePubKey(i)` if `keccak256(pubKeys[i]) == keccak256(pubKeys[j])` for any `j < i`. - Authorization (`validateUserOp`, `executeThreshold`) counts distinct signers by member INDEX via the `seen` bitmask in `_countMem`, and returns success only when `valid >= threshold`. - `scheme`, `threshold`, `size`, `membersHash`, `_pubKeys` are immutable after `initialize`. This is the exact target of `aerenew/formal-consensus/threshold_account_smt.py` (P1: with distinct keys, no single keyholder can reach threshold `t >= 2`). The CVL splits it into the part provable at bytecode level and the combinatorial part that stays in z3, keeping the same boundary the z3 file itself declares. ```cvl // certora/specs/AereThresholdAccount.spec methods { function threshold() external returns (uint8) envfree; function size() external returns (uint8) envfree; function scheme() external returns (uint8) envfree; function membersHash() external returns (bytes32) envfree; function entryPoint() external returns (address) envfree; function pubKeyAt(uint8) external returns (bytes) envfree; } // TH-RULE-1 committee bounds hold after a successful initialize: a real committee // always has 1 <= threshold <= size <= 255. In particular threshold >= 1, so an // empty signer set never authorizes, and threshold <= size, so the committee is // satisfiable only by genuine members. rule committeeBoundsAfterInit(env e, address ep, uint8 sch, uint8 t, bytes[] pubKeys) { initialize(e, ep, sch, t, pubKeys); assert threshold() >= 1, "threshold is at least 1"; assert threshold() <= size(), "threshold never exceeds committee size"; assert to_mathint(size()) == pubKeys.length; } // TH-RULE-2 the committee is set ONCE and is immutable thereafter: a second // initialize always reverts, and no method changes scheme / threshold / size / // membersHash after the first init. So the distinct-key set fixed at init can never // be swapped for a duplicate-laden one later. rule committeeImmutableAfterInit(method f, env e, calldataarg args) { require entryPoint() != 0; // already initialized uint8 t0 = threshold(); uint8 n0 = size(); uint8 s0 = scheme(); bytes32 mh0 = membersHash(); f(e, args); assert threshold() == t0, "threshold immutable post-init"; assert size() == n0, "size immutable post-init"; assert scheme() == s0, "scheme immutable post-init"; assert membersHash() == mh0, "membersHash immutable post-init"; } // TH-RULE-3 DISTINCT KEYS ENFORCED AT INIT (the 2026-07-15 dup-key fix): if // initialize succeeds, then no two stored committee members share a public key. // Expressed over the two-member witness that the pairwise loop rejects: for any // distinct in-range indices i, j, the stored keys differ. This is the bytecode-level // statement of "the same keyholder cannot occupy two committee slots". rule initRejectsDuplicateKeys(env e, address ep, uint8 sch, uint8 t, bytes[] pubKeys, uint8 i, uint8 j) { initialize(e, ep, sch, t, pubKeys); // reverts on any duplicate; reaching here => no dup require i < size() && j < size() && i != j; assert keccak256(pubKeyAt(i)) != keccak256(pubKeyAt(j)), "no two committee members share a public key after a successful init"; } ``` Design-level restatement of `threshold_account_smt.py` P1, expressed in CVL over an abstract committee (the same combinatorial layer, and the same boundary, that the z3 file declares: it models the counting logic, not the full Solidity `_countMem` loop over an unbounded `Leg[]`): ```cvl // certora/specs/ThresholdCounting.spec (abstract-committee model) // // key(i) = the id of the keyholder controlling slot i. count(h) = number of slots h // controls. The seen-bitmask counts distinct INDICES, so "valid signers" <= number of // distinct indices supplied. TH-RULE-3 gives distinct KEYS per index, hence distinct // keyholders per counted index. This ghost model proves the P1 consequence: with // pairwise-distinct keys, no single keyholder h controls >= threshold slots for t >= 2. ghost mapping(uint256 => uint256) key; // slot -> keyholder id ghost uint256 committeeSize; // P1: distinct committee keys => every keyholder fills at most one slot, so reaching // a threshold t >= 2 requires at least t distinct keyholders. rule distinctKeysImplyThresholdNeedsDistinctHolders(uint256 h, uint256 t) { require t >= 2; // committee keys are pairwise distinct (established on-chain by TH-RULE-3): require forall uint256 a. forall uint256 b. (a < committeeSize && b < committeeSize && a != b) => key[a] != key[b]; // NEGATION: some single keyholder h controls >= t slots. mathint slotsForH = 0; // (in the runnable spec this is a bounded fold over committeeSize; shown here as // the property the fold asserts) assert !(exists uint256 s1. exists uint256 s2. s1 < committeeSize && s2 < committeeSize && s1 != s2 && key[s1] == h && key[s2] == h), "with distinct keys no keyholder occupies two slots, so t>=2 needs t distinct holders"; } ``` Honesty note on TH: TH-RULE-1/2/3 are bytecode-level rules against the real `AereThresholdAccount`. The abstract-committee P1 rule is the CVL transcription of the z3 combinatorial proof and carries the same "not the compiled counting loop" boundary that `threshold_account_smt.py` states in its own summary. The z3 negative controls (P2/P3: without the distinct-key check one keyholder reaches threshold alone) remain in z3; the CVL equivalent is simply TH-RULE-3 failing if the `DuplicatePubKey` guard is removed. `[MEASURE: run certoraRun certora/conf/threshold.conf and publish the AereThresholdAccount rule report]` --- ## 3. `certora/` layout, run config, and commands Proposed tree under the contracts package (`aerenew/contracts/`, so `certoraRun` resolves imports through the existing Hardhat / Foundry remappings): ``` aerenew/contracts/ certora/ specs/ AereSink.spec AereCoinbaseSplitterV2.spec AereFeeBurnVault.spec sAEREv2.spec AereCryptoRegistry.spec AerePQCKeyRegistry.spec AerePQCKeyRegistry_pop.spec # K1/K2 keccak domain-separation (MEASURE extension) AereThresholdAccount.spec ThresholdCounting.spec # abstract-committee P1 model harness/ DummyERC20A.sol # faithful minimal ERC20 for the linked asset AereSinkHarness.sol # exposes internal getters if needed conf/ burnstack.conf sAEREv2.conf registries.conf threshold.conf README.md # this status doc's run section, copied for the repo ``` `harness/DummyERC20A.sol` is the same faithful minimal ERC-20 the Halmos suite already uses (`aerenew/formal-contracts/specs/AereSink.symbolic.t.sol` MockERC20): exact-amount `transfer`, `transferFrom`, `approve`, `balanceOf`. Fee-on-transfer and rebasing tokens are out of scope (excluded by the asset-listing policy), the same bound the Halmos SK-series declares. Example run config (Certora conf files are JSON): ```json // certora/conf/burnstack.conf { "files": [ "contracts/sink/AereSink.sol", "contracts/AereCoinbaseSplitterV2.sol", "contracts/AereFeeBurnVault.sol", "certora/harness/DummyERC20A.sol" ], "verify": "AereSink:certora/specs/AereSink.spec", "link": [ "AereSink:AERE=DummyERC20A" ], "solc": "solc0.8.23", "optimistic_loop": true, "loop_iter": "3", "rule_sanity": "basic", "msg": "Aere burn stack: sink 3-bucket immutability + splitter caps + burn-vault no-withdraw" } ``` ```json // certora/conf/sAEREv2.conf { "files": [ "contracts/staking/sAEREv2.sol", "certora/harness/DummyERC20A.sol" ], "verify": "sAEREv2:certora/specs/sAEREv2.spec", "link": [ "sAEREv2:_asset=DummyERC20A" ], "solc": "solc0.8.23", "optimistic_loop": true, "rule_sanity": "basic", "msg": "sAERE v2: donation resistance + totalAssets consistency + drip monotonicity" } ``` ```json // certora/conf/registries.conf { "files": [ "contracts/pqc/AereCryptoRegistry.sol", "contracts/pqc/AerePQCKeyRegistry.sol" ], "verify": "AereCryptoRegistry:certora/specs/AereCryptoRegistry.spec", "solc": "solc0.8.23", "optimistic_loop": true, "rule_sanity": "basic", "msg": "Aere PQC registries: fail-closed verify + append-only rows + no re-point" } ``` ```json // certora/conf/threshold.conf { "files": [ "contracts/mpc/AereThresholdAccount.sol", "contracts/mpc/AerePQCThreshold.sol" ], "verify": "AereThresholdAccount:certora/specs/AereThresholdAccount.spec", "solc": "solc0.8.23", "optimistic_loop": true, "loop_iter": "4", "rule_sanity": "basic", "msg": "Aere threshold account: distinct-key committee + set-once immutability" } ``` Exact commands (each requires the `certora-cli` package and a `CERTORAKEY` from `prover.certora.com`): ```bash # one-time setup (NOT run in this environment) pip install certora-cli export CERTORAKEY= # from aerenew/contracts/ certoraRun certora/conf/burnstack.conf certoraRun certora/conf/sAEREv2.conf certoraRun certora/conf/registries.conf certoraRun certora/conf/threshold.conf # run a single rule while iterating: certoraRun certora/conf/burnstack.conf --rule noFundsToArbitraryAddress # separate registry spec run (AerePQCKeyRegistry has its own verify target): certoraRun certora/conf/registries.conf --verify AerePQCKeyRegistry:certora/specs/AerePQCKeyRegistry.spec ``` Each `certoraRun` uploads the job to Certora's cloud back end and returns a job URL whose HTML report lists every rule as `Verified`, `Violated` (with a counterexample), or `Timeout`. That report is the artifact to publish. --- ## 4. Honest status ### 4.1 What is written here versus what is proved Everything in Section 2 is **CVL that is authored and matched to the real contract interfaces read from source in this repository.** The method signatures, state-variable getters, enum members, status constants, and function selectors are taken from the actual `.sol` files, not from documentation. **No rule in this document is proved.** The Certora Prover has not been run. The distinction matters: "authored and interface-matched" is a claim about the CVL text; "proved" is a claim about a solver result, and we do not have one. ### 4.2 Which targets have real CVL versus flags | Target | Source file read | CVL status | |---|---|---| | `AereSink` | `contracts/sink/AereSink.sol` | Real CVL against real getters (`BURN_BPS`, `BURN_VAULT`, `flush`, `sweepDust`). AERE-branch rules exact; router branch is a marked `[MEASURE]` extension. | | `AereCoinbaseSplitterV2` | `contracts/AereCoinbaseSplitterV2.sol` | Real CVL (`burnBps`, `sinkBps`, `MAX_BURN_BPS`, `setBps`, `owner`). | | `AereFeeBurnVault` | `contracts/AereFeeBurnVault.sol` | Real CVL (`totalBurnedAERE`, `sweepToZero`, `nativeBalances`). | | `sAEREv2` | `contracts/staking/sAEREv2.sol` | Real CVL (`totalAssets`, `undistributedRewards`, `sync`, `convertToAssets`). SR-RULE-4 designed to distinguish v2 from the un-fixed v1. | | `AereCryptoRegistry` | `contracts/pqc/AereCryptoRegistry.sol` | Real CVL (`getAlgorithm`, `statusOf`, `verify`, `resolveActive`, `Status` enum). | | `AerePQCKeyRegistry` | `contracts/pqc/AerePQCKeyRegistry.sol` | Real CVL (`keyCount`, `ownerOf`, `statusOf`, `verifyWithKey`, `identityNonce`). K1/K2 keccak domain-separation flagged `[MEASURE]` extension. | | `AereThresholdAccount` + `AerePQCThreshold` | `contracts/mpc/AereThresholdAccount.sol`, `AerePQCThreshold.sol` | Real CVL for init bounds / set-once / distinct-key (TH-1/2/3). The P1 keyholder-counting theorem is an abstract-ghost model, same boundary as `threshold_account_smt.py`. | | `AereThresholdPQCRegistry` | `contracts/mpc/AereThresholdPQCRegistry.sol` | Not separately specced here; its `registerCommittee` dup-key guard is byte-identical to `AereThresholdAccount.initialize`, so TH-RULE-3 transfers. Adding a dedicated spec is a `[MEASURE]` follow-up. | No target required a `[VERIFY: locate .sol]` flag: every contract named in the task was located and read. The only interface caveat is the sAERE target selection, which points at `sAEREv2.sol` (the R7-fixed redeploy) rather than the live `sAERE.sol`; this is stated inline at Section 2.b. ### 4.3 The measurement gate (nothing is proved until these run) | # | Command | Publishes | |---|---|---| | M1 | `certoraRun certora/conf/burnstack.conf` | `[MEASURE]` PASS/FAIL for SK-INV-1/2, SK-RULE-3/4, CS-INV-1/2/3, CS-RULE-4, FB-INV-1, FB-RULE-2/3 | | M2 | `certoraRun certora/conf/sAEREv2.conf` | `[MEASURE]` PASS/FAIL for SR-RULE-1, SR-INV-2/3, SR-RULE-4 | | M3 | `certoraRun certora/conf/registries.conf` | `[MEASURE]` PASS/FAIL for CR-INV-1, CR-RULE-2..6, KR-INV-1, KR-RULE-2..5 | | M4 | `certoraRun certora/conf/threshold.conf` | `[MEASURE]` PASS/FAIL for TH-RULE-1/2/3 and the P1 ghost model | `[MEASURE: run each conf above with certoraRun and publish the resulting Certora rule report (the job-URL HTML listing every rule as Verified / Violated / Timeout). Only after a rule shows Verified may it be described as proved. Until then it is CVL authored, not run.]` ### 4.4 Publication statement When this document is published, the accurate framing is: "Aere Network has authored Certora CVL specifications for its most safety-critical contracts (burn stack, sAERE, the crypto and PQC-key registries, and the post-quantum threshold account), matched to the deployed contract interfaces and reusing the property statements already checked at the design level in z3. Executing them to a machine report requires the Certora Prover (free tier at prover.certora.com; `certora-cli`), which produces the per-rule Verified / Violated result. That run is pending; no rule is claimed proved before it."