e4cead319d
Aere Network public source. Everything here can be checked against the live chain (chain id 2800, https://rpc.aere.network). Scope note, stated up front rather than buried: consensus on chain 2800 is classical secp256k1 ECDSA QBFT. The post-quantum work in this repository is at the signature, precompile, account and transport layers. Nothing here makes the consensus post-quantum, and no document in it should be read as claiming so.
822 lines
41 KiB
Markdown
822 lines
41 KiB
Markdown
# 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=<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."
|