aere-docs/AERE-CERTORA-FORMAL-VERIFICATION.md

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 hooks.

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):

// 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).

// 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.

// 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):

// 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):

// 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:

// 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.

// 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[]):

// 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):

// 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"
}

// 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"
}

// 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"
}

// 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):

# one-time setup (NOT run in this environment)
pip install certora-cli
export CERTORAKEY=<key from prover.certora.com>

# 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 <contract>.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."