aere-docs/AERE-ENGINEERING-SECURITY-SPEC.md

Aere Network Engineering and Security Specification

Status: Internal draft for adversarial review and for the external audit that follows. Every claim is meant to be checkable against the repository, the live chain (chain ID 2800), or the cited formal-verification artifacts. This document is internally verified and adversarially self-reviewed; it is not yet externally audited. Read every guarantee as "internally verified, not externally attested" until an independent audit completes.

A single framing statement governs the entire document and is repeated because it is the most common thing to get wrong about Aere: smart contracts and accounts on Aere can verify post-quantum signatures (Falcon, ML-DSA, SLH-DSA) through live EVM precompiles; consensus remains classical ECDSA / QBFT, and the on-chain zero-knowledge verifiers remain classical BN254 pairing checks. Aere is post-quantum at the signature and precompile layer and classical at the consensus and ZK verification layers. The chain as a whole is not post-quantum, and this document never claims it is.

---

Engineering Principles

Aere Network is built on a small set of engineering principles. This chapter is not marketing: each principle is stated with the evidence that backs it, and where a principle is an aspiration not yet fully earned, that is said plainly. A principle without evidence is a slogan, and the point of this document is to avoid slogans.

Principles we hold and can demonstrate today

• Fail closed. A component that cannot do its job safely refuses rather than guesses. The post-quantum precompiles return a not-verified result (a 32-byte zero word, or empty for the hash function) on malformed or invalid input; they never return a false accept and never revert consensus. (See Section 1.2 and Section 5.)
• No admin on the economic core. The value-bearing core (AereSink, the burn vault, sAERE) is ownerless and immutable: a repository-wide sweep of the deployed set finds no owner-withdraw, no upgrade proxy, no selfdestruct, no delegatecall. This is the honest, checkable form of the claim. It is deliberately not a blanket "no admin backdoors anywhere": operational contracts (the NAV oracle, compliance screening, the currently-inert governance) have explicit, documented Foundation roles, and hiding that would be the opposite of this principle. (See Section 1.6 and Section 1.7.)
• Least privilege. Every Foundation role that does exist is bounded and documented: the NAV oracle can only propose, dismiss, and attest, and cannot alter an attested snapshot; a program registry can disable a malicious program but cannot invalidate already-recorded proofs. (See Section 1.7.)
• Determinism over cleverness. Every precompile is a pure function of its input bytes, reading no chain state and no nondeterministic source, so all nodes compute the identical result and gas charge. Across all adversarial fault testing to date, zero forks were observed: the chain halts and recovers rather than forking. (See Assumption A-10 and Section 5.)
• Formal verification preferred. Safety-critical properties are machine-checked, not argued in prose: z3 SMT models of consensus locking and of the escrow and threshold-custody invariants (125 proved properties plus 49 counterexample negative controls at last count), Halmos and Solidity SMTChecker symbolic checking, and 22 invariant-property fuzz suites over the burn, economics, and custody contracts. (See Assumption A-11.)
• Backward compatibility first. The EVM, Solidity, bytecode, and JSON-RPC are unchanged; differentiation is added at standard extension points (precompiles at reserved addresses, client-only forks). EIP-7702 is the in-place bridge for existing accounts rather than a compatibility-breaking redesign. (See Section 4.)
• Security over performance. The choices that trade performance for safety are deliberate: deterministic QBFT finality over a higher-throughput probabilistic protocol, and keeping the burn out of the consensus-critical path so a policy change cannot halt the chain.

Principles we are still earning (stated honestly, not yet claimed as achieved)

• Open, reproducible benchmarks. We are moving toward publishing every benchmark, test, and vector so any third party can reproduce them. This is in progress, not done. Until the repositories and harness are public and the measured coverage number is published, we do not claim it as achieved.
• Reproducible builds. A verifiable source-to-SHA256 build of the client and contracts is a roadmap item, not a present guarantee.
• Independent audit. Every guarantee in this document is internally verified and adversarially self-reviewed, but not yet externally audited. This document is the bridge to that audit.

---

1. Threat Model per Subsystem

Each subsystem below lists what an attacker could realistically attempt and what actually defends against it, including the cases where the defense is a disclosed limitation rather than a cryptographic or economic guarantee.

1.1 Consensus (QBFT)

Aere runs Hyperledger Besu (Java, 26.4.0 line) with QBFT, a partially-synchronous BFT protocol. Blocks target roughly 0.5 s. Validator identity is by ECDSA public-key recovery (ecrecover) over secp256k1: each committed seal is a 65-byte recoverable signature and the signer address is recovered from it, so there is no stored validator public key at verification time. The live validator set is N = 7, and at N = 7 the QBFT quorum is ceil(2N/3) = 5 and the Byzantine fault bound is f = 2.

Attacker goals and defenses:

• Forge a block or seal without a validator key. Defended by ECDSA seal recovery plus the requirement that every recovered committer be a member of the stored validator set, with a per-block quorum of 5 distinct committers. Forgery reduces to forging secp256k1 ECDSA, which is classically hard. It is not quantum-hard: a cryptographically-relevant quantum computer running Shor breaks the seal signature, which is the central reason consensus is described honestly as classical, not post-quantum.
• Equivocate or split the chain (safety attack). QBFT tolerates up to f = 2 Byzantine validators at N = 7 with safety unconditional (no fork) under the standard BFT bound. Beyond 2 Byzantine validators (more than one third), safety is lost: a 3-of-7 collusion can violate agreement. This is a hard bound, not a soft target.
• Stall the chain (liveness attack) at the fault boundary. With exactly 2 validators down, all 5 survivors must prepare and commit with zero slack. QBFT round-robin proposer selection plus a doubling round-change timeout means an unlucky proposer sequence can exceed a fixed measurement window before an alive proposer's round succeeds. Adversarial soak testing on an isolated testnet (100 kill-2-of-7 cycles: 40 mixed-client RT=4, 40 mixed-client RT=1, 20 pure-Besu) recorded 0 forks and 100/100 self-resync, with a rare (about 5 percent), temporary, self-healing zero-progress window at the exact f = 2 boundary. That tail is inherent to partially-synchronous BFT (FLP: liveness is eventual, not bounded-time, at the boundary) and was not removable by timeout tuning. It is not a fork and not a permanent halt.
• Grind proposer selection or exploit locking. IBFT 2.0 locking (retain the prepared block and prepare-certificate, carry it in round-change, re-propose the justified block) is the property that prevents a stale or conflicting proposal from being committed across a round change. It is formally modeled (formal-consensus/qbft_locking_smt.py) and enforced by the live Besu producer.
• The centralization threat itself. All 7 validators are Foundation-operated. The Nakamoto coefficient is therefore approximately 1: a single operator (the Foundation) can in principle halt or, if it chose to run more than 2 equivocating nodes, break safety. This is the single most important limitation in this document. It is disclosed, not hidden, and is not mitigated by cryptography; the only present mitigation is operator honesty plus a public decentralization roadmap. See Assumption A-3.
• Second-client cross-check. A patched Nethermind validates live chain 2800, runs the PQC precompiles, and produces byte-identical QBFT blocks that stock Besu accepts (demonstrated offline via block import, not yet as a live devp2p producer). It currently acts as a client-diversity fail-safe cross-check. It is not a live producing validator, and until the IBFT locking findings are implemented in its engine and soak-verified against an active-Byzantine scenario, it is safe only as an observing or voting participant below the q - f threshold, not as a producer.

1.2 Post-Quantum Precompiles

Five signature and hash precompiles are live on mainnet (activated at block 9,189,161) at the address band 0x0AE1..0x0AE5: Falcon-512 (0x0AE1), Falcon-1024 (0x0AE2), ML-DSA-44 (0x0AE3), SLH-DSA-SHA2-128s (0x0AE4), and SHAKE256 (0x0AE5). Two further precompiles, ML-KEM-768 (0x0AE6) and Falcon HashToPoint (0x0AE7), are built and KAT-verified on an isolated testnet only and are not activated on mainnet (activation is founder-gated). A STARK-verify precompile design at 0x0AE8 is a reference skeleton, not a working verifier, and is not activated anywhere. All implementations use Bouncy Castle (bcprov-jdk18on-1.83.jar) on the client classpath. Measured marginal verify cost: Falcon-512 40,000 gas, Falcon-1024 75,000 gas, ML-DSA-44 55,000 gas, SLH-DSA-SHA2-128s 350,000 gas, SHAKE256 60 gas base plus 12 gas per word.

Attacker goals and defenses:

• Crash a node or split consensus with malformed input. A precompile that panicked or behaved non-deterministically on adversarial bytes would be a consensus fault, since every node must compute the identical result and gas charge. The behavior is fail-closed and was verified against the live chain: the signature verifier precompiles (0x0AE1 through 0x0AE4) return a 32-byte zero word (read as "not verified") on any signature that does not verify or on malformed input, and SHAKE256 (0x0AE5) returns empty on malformed framing; none of them revert. The two non-signature precompiles are additionally source-verified fail-closed: MLKEM768PrecompiledContract and HashToPointPrecompiledContract catch every Throwable and return Bytes.EMPTY. (An earlier AIP design draft framed malformed input as "must revert and consume all gas"; that framing was reconciled to the actual as-shipped fail-closed behavior.)
• Forge a post-quantum signature. Defended by the NIST-standardized schemes themselves (Falcon, FIPS 204 ML-DSA, FIPS 205 SLH-DSA) as implemented by Bouncy Castle, validated bit-for-bit against official NIST KAT / ACVP vectors committed to the repository, in both accept and crafted-invalid directions. Soundness rests on the NIST PQC hardness assumptions and on the correctness of the Bouncy Castle implementation (Assumptions A-6, A-7).
• Substitute a weaker curve or downgrade. The precompile at a given address implements one fixed scheme and parameter set; there is no in-band algorithm negotiation, so there is no downgrade surface at the precompile itself. Algorithm agility is a property of the calling contract, not the precompile.
• Exhaust gas or denial of service. Verify cost is fixed per scheme and bounded well below the EIP-7825 per-transaction cap (2^24 gas), so a single verify cannot be inflated by input shape. Falcon-1024 and ML-DSA-44 in pure Solidity exceed the cap and were therefore view-only before the native precompiles; the precompiles are what bring them under the cap for on-chain recording.
• Confuse "verifies a PQ signature" with "PQ chain". The threat here is representational, not technical: a reader could over-read the precompiles as post-quantum consensus. The defense is the framing statement at the top of this document, repeated in the guarantees table below.

1.3 Zero-Knowledge Verification

Aere hosts a multi-prover on-chain verification surface behind a route-by-selector gateway: SP1 (Groth16 and Plonk), RISC Zero (Groth16), a raw KZG / EIP-4844 path, and a generated Halo2 verifier, with a permissionless attestation registry on top. The application verifiers (storage-proof coprocessor, zk-compliance, zkML, rollup validity, recursive aggregator) hold the SP1 gateway address rather than a concrete verifier, so a new prover version is a single upstream route change.

Attacker goals and defenses:

• Submit a false proof (soundness break). Defended by the underlying proof systems (SP1 / Plonky3, RISC Zero, Halo2) being sound, and by the verifiers binding the exact program: an SP1 proof is checked against a programVKey that binds a specific guest ELF, a RISC Zero receipt against an imageId, and the recursive aggregator binds the inner KoalaBear (SP1Field) verifying-key digest that the recursion verifier actually checked, rather than only the on-chain BN254 vkey. Soundness is an assumption about the proof systems (Assumption A-5), not something this chain proves from first principles.
• Break the ZK verifier with a quantum computer. The on-chain verifiers are BN254 Groth16 pairing checks. BN254 pairings are Shor-breakable, so the ZK verification layer is classical and is not post-quantum. This is disclosed. The planned mitigation is a direct hash-based STARK verifier that rests on hash collision-resistance rather than pairings. Scope caveat (2026-07-19 research finding): the skeleton built so far is a real, conformance-confirmed BabyBear + FRI STARK verifier that targets Aere's OWN Plonky3 circuits, and it does NOT verify SP1 6.1.0 proofs. The pinned SP1 6.1.0 is a Hypercube release (KoalaBear multilinear: BaseFold plus sumcheck-zerocheck plus LogUp-GKR, not BabyBear FRI), so removing the SP1 Groth16 wrap is a separate founder-gated retarget to the SP1 Hypercube stack (see AERE-STARK-SP1-RECURSION-AIR-PORT-SPEC-SUMMARY.md), not a near-term step. Either way that verifier is presently a reference skeleton that fail-closes on every input and is not activated. Until it is real, retargeted, audited, and activated, the ZK layer's post-quantum posture is a design, not a property.
• Poison a shared root or side tree. The storage-proof coprocessor walks the real Merkle-Patricia state trie from stateRoot to the claimed value, hashing each node against its parent reference, with no Foundation-seeded side tree. Anchor-poisoning and inner-vkey-enforcement findings from the 2026-07-17 review are fixed with regression tests in the repository.
• Register a malicious program. Program registration is permissionless; the Foundation can disable a malicious program but cannot disable a legitimate one and cannot retroactively invalidate already-recorded proofs. This is a bounded, disclosed Foundation role, not an arbitrary override.

1.4 Bridge and Cross-Chain

The cross-chain surface is optimistic intent settlement (AereSpokePool, ERC-7683 / Across-V3 style), an institutional settlement hub (AereSettlementHubV2), Hyperlane-style warp routes, and zk light clients (QBFT and Ethereum). The escrow accounting of the two core contracts is machine-checked: the SpokePool balance >= totalLocked + totalBond invariant and the SettlementHub balance >= committedLiabilities invariant are each proved inductive in z3 (formal-consensus/spokepool_smt.py, settlementhub_smt.py), with negative controls that reproduce a real under-backing counterexample when a guard is removed.

Attacker goals and defenses:

• Drain escrowed principal. Defended by the proven solvency invariants above: every settle path pays only an allowlisted solver, cancel refunds only the depositor, withdraw returns only the caller's own free bond, and any sweep of residual is strictly bounded to balance - committed so it can never touch a parked intent or a posted bond. No path sends funds to an arbitrary caller address.
• Claim without filling (optimistic-bond attack). This is the disclosed weak point. A claim does not prove the destination fill; settle releases the user's locked input to the solver after a challenge window unless challenged, and Phase-1 challenge only emits an event (the Foundation arbitrates and slashes off-chain). A rogue or key-compromised allowlisted solver could claim across many orders in one window and lose only the fixed bond, which does not scale with the value at risk. In Phase 1 this is bounded by a permissioned, Foundation-vetted solver allowlist and is documented in the contract NatSpec. It is a trust assumption, not a hidden bug. Before any permissionless phase, the bond must exceed the maximum stealable value per window.
• Break accounting with a hostile token. The SpokePool credits nominal input amounts, so a fee-on-transfer or rebasing input token can break its per-token backing invariant (a disclosed low-to-medium finding); the SettlementHubV2 closes this with an explicit asset allowlist that can exclude such tokens. Exposure is nil while inputs are restricted to vetted standard ERC-20s.
• Forge a cross-chain message or light-client header. The zk light clients verify proofs of the source chain's consensus rather than trusting a relayer. Their soundness inherits the ZK-layer assumption (Assumption A-5) and, for the QBFT light client, the same classical-BN254 caveat as Section 1.3.

1.5 Accounts and Account Abstraction

Aere supports ERC-4337 v0.7 (AereEntryPointV2), EIP-7702 upgrade-in-place, WebAuthn / P-256 passkey smart accounts, a Falcon-512-owned post-quantum smart account (AerePQCAccount), a hybrid ECDSA-plus-Falcon authorizer (AereHybridAuth), and a t-of-n post-quantum threshold account. The chain exposes the standard ecrecover (3,000 gas) and a P-256 verification precompile (RIP-7212 / RIP-7951 at 0x100, 3,450 gas), both at their standard protocol gas costs.

Attacker goals and defenses:

• Forge account authorization. Defended by the account's chosen validator: secp256k1 ECDSA, WebAuthn P-256 (device secure-element key that never leaves the device), Falcon-512 (post-quantum), or a hybrid that requires both an ECDSA and a Falcon signature over the same hash so that neither a broken curve nor a broken lattice alone suffices. Passkey security additionally depends on the device secure element and the WebAuthn ceremony (Assumption A-8).
• Reach threshold with duplicate committee keys. A 2026-07-15 finding showed the threshold custody and PQC registry accepted duplicate committee keys (distinctness was by index, not by key), so one keyholder could fill multiple slots. The fix is machine-checked (threshold_account_smt.py: with distinct keys no single keyholder reaches threshold t >= 2 for N up to 21) and is deployed on-chain as the PQC registry V2; the account-factory V2 redeploy is founder-gated, and both live buggy contracts are empty (0 committees, 0 accounts created), so exposure is nil either way.
• Exploit the nonce or paymaster surface. AereEntryPointV2 uses a strictly sequential single-dimension nonce; accounts that switch validators route on a signature prefix byte rather than a 2D nonce key, a named seam rather than a hidden one. The V2 token and stake-quota paymasters are hardened redeploys that fixed confirmed V1 drain and consent bugs, with the V1 contracts deprecated in place.
• Quantum forgery of a classical account key. An ECDSA-only or P-256-only account is not post-quantum; only accounts that use the Falcon or hybrid validators are. This is a per-account property that users opt into, not a chain-wide guarantee.

1.6 Economic Core

The economic core is immutable and ownerless. AereSink is a 3-bucket router (BURN, BUYBACK, YIELD) with, per its source, no owner, no admin, no governance role, no setBucket / setRecipient / setRouter / pause, immutable bucket recipients and immutable basis-point splits that must sum to exactly 10000. sAERE is an ERC-4626 vault. The burn is a cut of the validator block reward, capped by the immutable MAX_BURN_BPS = 5000 (50 percent) in AereCoinbaseSplitterV2; it is not a base-fee burn. AereFeeBurnVault has no withdraw function and no admin escape hatch. AERE is the native coin; its total supply is fixed at genesis (2.8B) and there is no protocol mint path.

Attacker goals and defenses:

• Rug: mint to self, admin-withdraw, upgrade-swap, selfdestruct, or delegatecall. A repository-wide primitive sweep across the deployed contract set found 0 selfdestruct, 0 delegatecall, 0 upgradeable proxies (no UUPS / transparent / _authorizeUpgrade / upgradeTo), and 0 owner escape hatch (adminWithdraw / rescueTokens / sweepTo). The concrete meaning of "no one can rug the economic core" is that these specific primitives are absent from the deployed set. This is the honest, checkable form of the claim, not a blanket "no backdoors anywhere" (see Section 1.7).
• Steal routed fees. Every AereSink routing path terminates at the no-withdraw burn vault or the sAERE vault; no path sends funds to an arbitrary or caller-supplied address, so there is no theft vector. A failed buyback swap degrades to sweepable dust rather than a lock, and flush and sweep are reentrancy-guarded.
• Inflate the burn beyond policy. The burn rate is Foundation-settable but hard-capped at 50 percent by an immutable constant; it cannot be pushed higher, and it cuts the validator reward, not the base fee.
• Manipulate the sAERE exchange rate (first-depositor / donation inflation). The vault does not mint shares on a raw transfer, so a direct donation lifts the rate rather than being stealable, and the yield bucket transfer pings the vault's sync so value drips linearly instead of as a sandwichable step. These properties are covered by invariant-property fuzz suites over the burn / economics contracts.

1.7 Oracles and Compliance

Operational contracts, in deliberate contrast to the economic core, do have explicit and documented Foundation roles. This is disclosed and is not a hidden backdoor. The correct statement is: there is no admin on the economic core (ownerless, immutable, verifiable on-chain), and the operational contracts have explicit, documented Foundation roles.

Attacker goals and defenses:

• Falsify a reserve or NAV attestation. AereNavOracle lets the Foundation (owner) propose, dismiss challenges, and attest a Merkle-rooted reserve snapshot; it explicitly cannot retroactively alter an already-attested snapshot. A proposed snapshot starts a 24-hour challenge window, anyone may challenge, and attestation after a clean window is permissionless. The Foundation's power is bounded to propose / dismiss / attest, and the challenge window plus append-only attestation is the defense against a single bad snapshot; it is a trusted-attestor model, not a decentralized oracle.
• Abuse compliance or sanctions screening. Compliance uses SP1 zk-compliance proofs (a user proves off-chain sanctions / residency / jurisdiction screening inside the zkVM, anchoring only a boolean-style clearance, with no PII on chain) and a Privacy-Pools-style compliant-withdrawal pool. The Foundation role here is screening policy, disclosed, not fund custody.
• Capture governance. Governor plus Timelock exist but are currently inert (they own nothing and control nothing until an audit-gated transfer). The threat of a captured governance is therefore not live today; it becomes relevant only if and when control is transferred, at which point the Timelock delay is the defense.
• Oracle staleness or decimals trap. A known activation-time hazard: AereSink's oracle-floor math assumes 18-decimal tokens, so enabling the oracle against a 6-decimal pair would give false sandwich protection. The oracle is off today (ORACLE = 0x0 on-chain), and activation is documented as requiring the decimals fix first. No exposure at present.

---

2. Guaranteed vs Not-Guaranteed

This table is the centerpiece of the specification. The left column is what Aere will stand behind; the right column is what Aere explicitly does not promise. A guarantee holds only under the assumptions in Section 3.

Component	What we GUARANTEE	What we DO NOT guarantee
Consensus (QBFT)	Safety (no fork / no equivocation) with up to 2 of 7 validators Byzantine; self-recovery and resync after transient faults (0 forks and 100/100 resync across 100 adversarial kill-2 cycles on testnet); IBFT 2.0 locking modeled and enforced by the live producer.	Safety beyond 2 Byzantine validators (a 3-of-7 collusion can fork); bounded-time liveness at the exact f = 2 boundary (FLP: liveness is eventual, not instantaneous); decentralization (all 7 validators are Foundation-operated, Nakamoto coefficient about 1); post-quantum consensus (seals are classical ECDSA).
PQC precompiles	Live on mainnet at 0x0AE1..0x0AE5; deterministic, gas-metered verification of Falcon-512/1024, ML-DSA-44, SLH-DSA-SHA2-128s, SHAKE256, validated bit-for-bit against NIST KAT/ACVP vectors; fail-closed (return a not-verified zero word or empty, never a fault).	That any signature scheme is unbreakable (soundness rests on NIST PQC hardness and on Bouncy Castle correctness); that 0x0AE6/0x0AE7 (ML-KEM, HashToPoint) or 0x0AE8 (STARK) are live on mainnet (they are not); that verifying PQ signatures makes the chain post-quantum.
ZK verification	A multi-prover on-chain verification surface (SP1 Groth16/Plonk, RISC Zero, KZG, Halo2) that binds the exact program (vkey / imageId), with a permissionless attestation registry and a real Merkle-Patricia storage-proof coprocessor.	Soundness of the underlying proof systems from first principles (assumed, not proven here); post-quantum security of the on-chain verifiers (BN254 pairings are Shor-breakable); that the planned STARK verifier is live (it is a non-activated reference skeleton).
Bridge / cross-chain	Machine-checked escrow solvency for the two core contracts (balance >= totalLocked + totalBond; balance >= committedLiabilities), proved inductive in z3; funds route only to allowlisted solver / depositor / own-bond / sink, never to an arbitrary address.	That an allowlisted solver cannot claim-without-filling within a challenge window (the fixed optimistic bond does not scale with value at risk; Phase-1 safety rests on the permissioned, Foundation-vetted solver allowlist); correct accounting under fee-on-transfer / rebasing input tokens on the SpokePool.
Accounts / AA	ERC-4337 v0.7, EIP-7702, passkey (P-256), Falcon-512, hybrid ECDSA+Falcon, and t-of-n threshold accounts; threshold duplicate-key fix machine-checked and deployed (PQC registry V2); hardened V2 paymasters.	That a classical ECDSA-only or P-256-only account is post-quantum (only Falcon / hybrid accounts are); device / WebAuthn security (out of chain scope); that the founder-gated account-factory V2 redeploy has occurred (buggy factory is live but empty).
Economic core	Ownerless and immutable AereSink and sAERE: no admin, no governance, no upgrade proxy, no selfdestruct, no delegatecall, no owner withdraw across the deployed set (repo-wide primitive sweep = 0 each); burn hard-capped at 50 percent of validator reward; fixed 2.8B native supply with no mint path.	A blanket "no admin anywhere on the network" (operational contracts have explicit Foundation roles, see next row); protection against a Foundation-set burn rate anywhere between 0 and the 50 percent cap; economic / price outcomes of the burn-buyback-yield mechanism.
Oracles / compliance	Explicit, documented, bounded Foundation roles: NavOracle can only propose / dismiss / attest and cannot alter an attested snapshot (24-hour challengeable window, permissionless attest); compliance anchors only zk clearance booleans (no PII on chain); Governor / Timelock are inert.	A decentralized or trustless oracle (NAV is a trusted-attestor model); that the Foundation cannot publish a wrong-but-unchallenged snapshot within a window; correctness of any off-chain screening input; anything about governance once control is transferred beyond the Timelock delay.

---

3. Security Assumptions

The guarantees in Section 2 hold only under the following assumptions. If an assumption is false, the corresponding guarantee does not hold. They are stated plainly so that a reviewer can accept or reject each one on its own terms.

• A-1 Partial synchrony. Validator clocks are loosely synchronized and, after some unknown global stabilization time (GST), message delay is bounded. QBFT safety does not depend on this, but liveness does: under asynchrony, progress is only eventual (FLP), and the rare f = 2 boundary stall is a consequence of this assumption, not a defect.
• A-2 Byzantine bound. At most 2 of the 7 validators are Byzantine (f = 2 at N = 7, quorum = 5). Beyond one third Byzantine, BFT safety fails and a fork becomes reachable. This bound is exact.
• A-3 Honest-operator trust model (the load-bearing assumption). All 7 validators are Foundation-operated, so the trust model is honest-operator, not economic or decentralized, and the Nakamoto coefficient is approximately 1. Aere's safety today rests on the Foundation not running more than 2 equivocating nodes and not censoring at will. This is disclosed, is the reason the chain is not yet credibly decentralized, and is the assumption an external reviewer should weigh most heavily.
• A-4 Keccak collision resistance. Block hashing, Merkle-Patricia state proofs, and commit-seal pre-images assume keccak-256 is collision-resistant.
• A-5 Proof-system soundness. The SP1 / Plonky3, RISC Zero, and Halo2 proof systems are sound: a verifying proof implies the asserted statement, except with negligible probability. The on-chain verifiers are assumed to correctly implement these systems (backed by KAT / fixture tests, not by a from-scratch soundness proof).
• A-6 NIST PQC hardness. The hardness assumptions behind Falcon (NTRU lattice), ML-DSA / ML-KEM (module lattice), and SLH-DSA (hash-based) are unbroken. Signature-layer post-quantum guarantees are void if these are broken.
• A-7 Audited primitive library. The precompiles rely on the correctness of Bouncy Castle (bcprov-jdk18on-1.83.jar) for Falcon / ML-DSA / SLH-DSA / SHAKE. A bug in that library is a bug in the precompiles.
• A-8 Device and WebAuthn security. Passkey / P-256 account security assumes the device secure element protects the private key and that the WebAuthn ceremony is not subverted on the client. This is outside the chain's control.
• A-9 BN254 is honest until replaced. The on-chain ZK verifiers use BN254 pairings, which are Shor-breakable. They are assumed secure against classical adversaries only, and this assumption is explicitly temporary: it stands until the planned direct hash-based STARK verifier (Section 1.3) is made real, audited, and activated. Under a cryptographically-relevant quantum adversary, the ZK verification layer and the QBFT light client offer no guarantee.
• A-10 Precompile determinism. Every precompile is a pure function of its input bytes, reads no chain state or nondeterministic source, and every node runs an identical client build, so all nodes compute the identical result and gas charge. A divergence here would be a consensus fault.
• A-11 No external audit yet. The guarantees are backed by internal formal verification (z3 SMT: 125 proved properties plus 49 counterexample negative controls across the consensus and contract models at last count; Halmos; Solidity SMTChecker; and 22 invariant-property fuzz suites over burn / economics / custody; exact per-suite counts are reproducible by running the published verification harness, run_consensus_verification.py plus the contract SMT suite) and by adversarial self-review, but not by an independent external audit. This document is the bridge to that audit; until it completes, every guarantee should be read as "internally verified, not externally attested."

---

4. Design Rationale ("Why not?")

This section records, for each load-bearing architecture decision, what was chosen, what the credible alternatives were, and why the alternative was rejected. The intent is to make the trade-offs auditable: every choice below has a cost, and the cost is stated. Where a decision reflects a deliberate deviation from Ethereum's current roadmap, the deviation is documented rather than hidden.

4.1 Consensus: QBFT, not HotStuff

Chosen. QBFT (a Byzantine-fault-tolerant IBFT-family protocol) as implemented in Hyperledger Besu, producing deterministic single-slot finality at a sub-second cadence (~0.5s target block time). At the live validator count N=7, QBFT tolerates f=2 Byzantine or crashed validators, with a commit quorum of 2f+1 = 5 of 7.

Alternative considered. HotStuff (and its pipelined variants), which achieves linear per-round communication complexity and is engineered to scale BFT consensus to hundreds of validators.

Why not HotStuff. HotStuff's headline advantage is communication complexity that stays linear as the validator set grows large. Aere runs a small, permissioned validator set (7 today, with a roadmap target in the 9 to 21 range). At that scale QBFT's O(N^2) message complexity is a non-issue in absolute terms (the crypto and gossip cost of a 5-of-7 quorum verify is on the order of a few milliseconds per block, a small fraction of the 500ms slot). The scaling regime where HotStuff wins is one Aere does not operate in and does not plan to enter under this design. Against that non-benefit, QBFT offers three concrete advantages at our size: (1) it provides deterministic, instant, single-block finality (no probabilistic or multi-round confirmation), which is the settlement guarantee the whole network is built to sell; (2) it is mature and already integrated in Besu, so it carries no new-protocol implementation risk; and (3) it is the protocol our post-quantum consensus research, our second-client work, and our zk finality proofs are all built against. Adopting HotStuff would have meant taking on the risk and integration cost of a less-battle-tested (for our client) protocol to buy scalability we have no use for. The honest limitation of the QBFT choice is disclosed in the threat model: at N=7 the fault tolerance is real against node outages but the validators are all Foundation-operated, so decentralization, not consensus mechanism, is the binding trust assumption.

4.2 Execution client: forked Besu, not Reth, with Nethermind as the second client

Chosen. A fork of Hyperledger Besu v26.4.0 (Java, base commit d2032017, built on a JDK 21 toolchain) as the sole live mainnet producer. The fork adds native post-quantum precompiles and an extended EIP-2935 block-hash lookback (live on mainnet since block 9,189,161) and carries the base-fee-floor change (live since block 10,141,734). A patched Nethermind 1.39.0 (.NET) is the second, independent client.

Alternatives considered. Reth (Rust, high-performance) as the base client; or running a single client indefinitely.

Why not Reth. Two reasons, one structural and one empirical. Structurally, Besu already ships QBFT, and QBFT block production is Besu-specific: no off-the-shelf Geth, Reth, Erigon, or stock Nethermind produces QBFT-compatible blocks. Choosing Reth would have meant building QBFT production into a client that has no notion of it, before we could produce a single block. Besu also already carried the codebase into which our PQC precompile fork and base-fee changes were integrated. Empirically, a single producing client is a demonstrated systemic risk: the September 2025 Reth halt is the reference case for why a chain that depends on one producing implementation can stop when that implementation hits a bug. That event is precisely the risk the second-client program exists to retire.

Why Nethermind as the second client (not a second Besu). A second Besu instance is not client diversity; it shares every bug with the first. Nethermind was chosen specifically for implementation diversity: it is a different codebase in a different language (.NET versus Besu's Java), so a consensus-relevant bug in one is unlikely to exist in the other. The patched Nethermind validates the live chain, runs the five PQC precompiles byte-for-byte identically (27 of 27 NIST KAT vectors), and, on an isolated test network, produces byte-identical QBFT blocks that stock Besu accepts through full BFT validation (with a one-byte-tampered seal rejected). The honest boundary: this cross-client production is proven on an isolated testnet (offline import and, in later work, live devp2p between test nodes), and a listen-only Nethermind follower has been run against the live network; it is not yet a live gossiping producer on chain 2800. Making it one is a founder-supervised change, because a producer bug on a live chain can halt or fork it. Besu remains the sole live producer today; the second client is a client-diversity cross-check and fail-safe, not a second live validator yet.

4.3 Interoperability: Hyperlane-compatible, not IBC, plus a zk-interop path

Chosen. An EVM-native, Hyperlane-compatible messaging layer (a Mailbox-compatible AereMessenger, an Interchain Gas Paymaster AereIGP), an ERC-7683 intent layer, and an Across-v3-compatible spoke pool. Alongside this sits a zero-knowledge interop path: on-chain zk light clients that verify a counterparty's consensus finality (inbound Ethereum sync-committee finality, outbound Aere QBFT finality) from inside a contract, via SP1 Groth16 proofs.

Alternative considered. IBC (the Inter-Blockchain Communication protocol), the trust-minimized, light-client-based standard from the Cosmos ecosystem.

Why not IBC. IBC's design philosophy, verifying the counterparty's consensus rather than trusting a bridge committee, is the right one, and Aere adopts that philosophy directly. But IBC as a protocol is built around Tendermint-style light clients and a non-EVM connection, channel, and packet model. Adopting it natively would have meant importing a substantial non-EVM stack and its tooling into an EVM chain whose entire value proposition is that it is an ordinary EVM. Instead Aere splits the problem: for permissionless, developer-familiar EVM interop it uses the Hyperlane-compatible interfaces (which the EVM tooling ecosystem already speaks), and for the trust-minimization that is IBC's real contribution it built the zk-interop light clients, which capture the "verify the counterparty's consensus, do not trust a relayer" property without leaving the EVM world. The honest boundary: the Hyperlane-compatible endpoints are interface-faithful and deployed, but a live decentralized relayer and interchain-security-module network is not yet stood up (the current bridge path runs through a single Foundation signer with a relayer pending), and the zk light clients are trust-minimized, not trustless, and not quantum-safe (their committed seals are classical secp256k1 and the proof wrap is Groth16 over BN254).

4.4 Post-quantum signatures: Falcon and ML-DSA together, not one lattice scheme

Chosen. Native on-chain verification of multiple post-quantum signature schemes, including two distinct lattice families: Falcon (Falcon-512 and Falcon-1024) and ML-DSA (Dilithium2 / ML-DSA-44), alongside hash-based schemes (SLH-DSA, XMSS). The precompiles for SHAKE256, Falcon-512, Falcon-1024, ML-DSA-44, and SLH-DSA-SHA2-128s are live on mainnet in the 0x0AE1 to 0x0AE5 band.

Alternative considered. Standardizing on a single lattice signature scheme (for example ML-DSA alone, the NIST primary lattice standard, or Falcon alone for its compact signatures).

Why not a single scheme. Cryptographic-risk diversification. Falcon and ML-DSA rest on different structured-lattice problems (Falcon on NTRU lattices, ML-DSA on module lattices with Fiat-Shamir-with-aborts). Supporting both means that a cryptanalytic break or a standardization flaw in one lattice family does not, by itself, remove Aere's ability to verify post-quantum signatures: accounts and settlement authorization can migrate to the surviving family. This is the same conservative posture as the hybrid AereHybridAuth account, which requires both a classical ECDSA and a Falcon-512 signature so that neither a broken curve nor a broken lattice alone suffices to forge. The cost of supporting multiple schemes is more verifier surface to implement, validate, and eventually audit; that cost is accepted deliberately in exchange for not betting the network's post-quantum future on a single mathematical assumption. The critical honest scope, stated wherever post-quantum is discussed: this is post-quantum at the signature, account, and application layer only. Consensus remains classical (validators sign secp256k1 QBFT messages) and the zk verification is classical (BN254 Groth16, Shor-breakable). Aere never claims post-quantum consensus.

4.5 Account abstraction: ERC-4337, not native AA, with EIP-7702 as the bridge

Chosen. ERC-4337 (v0.7) smart accounts as the account-abstraction path, with EIP-7702 (live under the Pectra ruleset) as the migration bridge that lets existing externally-owned accounts (EOAs) delegate to smart-account code.

Alternative considered. Native, protocol-level account abstraction, up to and including the "all accounts are smart accounts by default" end-state.

Why not native AA. ERC-4337 needs no consensus change and is an established standard with an existing tooling and bundler ecosystem; it delivers programmable accounts (including the Falcon-owned post-quantum smart account, AerePQCAccountFactory) without touching the protocol, which preserves exact EVM and Ethereum compatibility. Making all accounts smart by default would break EOA and EVM compatibility: it changes what an account fundamentally is, which breaks the assumptions of existing tooling, existing contracts, and existing user keys. Preserving that compatibility was a deliberate design goal, not an oversight. EIP-7702 is the chosen bridge precisely because it upgrades existing EOAs in place (an EOA can delegate to smart-account code) without forcing the disruptive "everything is a contract" change. Note on the Ethereum roadmap lineage: EIP-3074, an earlier EOA-empowerment proposal, was superseded by EIP-7702, which is the mechanism Aere carries; Aere does not implement 3074.

4.6 The virtual machine: extend the EVM, do not build a new VM

Chosen. Keep the EVM. Solidity, EVM bytecode, JSON-RPC, and the developer tooling are all unchanged. Differentiation (post-quantum verification, parallel execution, the block-hash lookback) is added as precompiles and client fork rules at otherwise-empty addresses, not as a new instruction set or a new language.

Alternative considered. Designing a new, purpose-built virtual machine (a new bytecode, a new language, or a non-EVM execution environment) optimized around Aere's differentiators.

Why not a new VM. A new VM maximizes both technical risk and adoption risk. Technically, a mature VM has years of implementation hardening, a known cost model, and a formal-ish operational history; a new VM starts that clock at zero. For adoption, the EVM is the single largest smart-contract developer surface in existence, and every deviation from it (a nonstandard opcode, a nonstandard account model, a nonstandard RPC) is a tax on every developer and every tool. Aere's thesis is settlement, not a novel programming model, so the design keeps the mature, tested execution environment intact and adds its differentiation at the edges where the EVM has explicit, standard extension points (precompiles at reserved addresses, activated by client-only forks in the same manner Ethereum activates its own hard forks). The result: nothing about Aere's account, passkey, or post-quantum surface depends on a nonstandard EVM. The cost of this choice is that some ambitions (base-layer parallel execution, an EVM-in-a-zkVM) must be reached inside the existing model rather than by designing them in from scratch; those remain roadmap and are labeled as such.

4.7 The burn: a cut of the validator reward, not a base-fee burn

Chosen. Aere burns a share (37.5% under the current configuration) of the validator coinbase block reward, applied by a splitter contract (AereCoinbaseSplitterV2) that validators or their forwarder daemons call each block. The rate is a Foundation-adjustable parameter, hard-capped at 50% (5000 basis points). It is explicitly not EIP-1559 protocol-level base-fee burning.

Alternative considered. An EIP-1559-style base-fee burn enforced by consensus (the mechanism Ethereum mainnet uses, where the base fee of every transaction is burned as a protocol rule).

Why not a base-fee burn. Being precise here is a credibility matter, and the design is deliberately honest about it. A consensus-level base-fee burn is a protocol rule; the Aere burn is a coinbase-reward split applied above consensus by a contract. The design routes the burn through the coinbase layer rather than enshrining it in consensus for two reasons: it keeps the burn out of the consensus-critical path (a change to the burn rate cannot halt or fork the chain, whereas a change to a consensus base-fee rule is a hard fork), and it lets the destinations be made immutable at the contract layer while the rate stays a bounded, governable dial. What is sealed is not the rate but the endpoints: AereSink (no owner, no setters, immutable splits) and AereFeeBurnVault (no owner, no admin, no withdraw function), so burned value cannot be rugged or drained regardless of who sets the rate. This document must not describe the Aere burn as a base-fee burn; it is a validator-reward-cut burn, rate-adjustable within a 50% ceiling, into immutable destinations. Separately, and not to be conflated with the burn: Aere does run a base-fee change at the protocol layer, a 1-Gwei EIP-1559 base-fee floor (live since block 10,141,734). That floor sets a minimum base fee; it is not a burn mechanism.

4.8 Deliberate compatibility deviations from the Ethereum roadmap

Aere tracks Ethereum's hard forks (Pectra activated at block 2,075,363; Fusaka / Osaka at block 2,106,606) so that its EVM surface matches mainnet at the same addresses. Several roadmap features are, however, deliberately neutralized or absent because Aere is a QBFT chain with no separate consensus (beacon) layer and no blob data-availability market. These are design decisions, disclosed here so an integrator is not surprised:

• Base fee has a floor plus a validator-reward burn, not a consensus base-fee burn (see 4.7). The floor is 1 Gwei, live from block 10,141,734.
• EIP-4844 blob transactions are present in the EVM, but BLOBBASEFEE (EIP-7516) returns 0 because there are no blobs: Aere runs no blob data-availability market.
• EIP-4788 (parent beacon block root) returns 0x0, because a QBFT chain has no separate beacon / consensus layer to expose a root from.
• EIP-3074 is not implemented; it is superseded by EIP-7702, which is the EOA-delegation primitive Aere carries (see 4.5).
• PeerDAS (EIP-7594), FOCIL, and EOF have no active role under Aere's QBFT model. PeerDAS has no data-availability role (there is no blob market), FOCIL (proposer inclusion lists) has no fork-choice or proposer-inclusion layer to enforce under QBFT, and EOF is not activated under the current ruleset.

---

5. Failure Analysis

This section describes Aere's behavior under each significant failure mode. For each, it states whether the behavior is PROVEN (demonstrated by a repeatable test or a live event) or EXPECTED (the deterministic consequence of the protocol's rules, not separately soak-tested at that exact configuration), and whether the chain halts safely, forks, or continues. The governing consensus parameters are fixed: N=7 validators, f=2, commit quorum 2f+1 = 5 of 7.

A safety-first summary that holds across every mode tested: in all adversarial fault testing to date, zero forks were observed. The chain's failure posture is to halt (and later recover) rather than to fork. That is the property a settlement layer must have, and it is the property the evidence supports.

Failure mode	Outcome	Fork?	Status
1 validator dies	Chain continues	No	PROVEN
2 validators offline	Continues at the quorum limit (rare, self-recovering stalls)	No	PROVEN
3+ validators offline	Chain halts (safe)	No	EXPECTED (quorum math) + sub-quorum halt demonstrated
Network partition	Minority side halts, recovers on reconnect	No	PROVEN (halt-then-recover demonstrated)
Nethermind and Besu disagree on state	Divergence detected by client cross-check	No (fail-safe)	PROVEN as a validation cross-check; not yet a live automated gate
PQC precompile errors on input	Fail-closed (defined empty / zero output, no revert)	No	PROVEN (live behavior verified)
Bridge goes down	Cross-chain messaging halts; L1 keeps running	No	EXPECTED (app-layer isolation)
ZK prover unavailable	New proofs pause; chain and verified state keep running	No	EXPECTED (advance is manual / permissionless)

5.1 One validator dies

Behavior. The chain continues. With one of seven validators down, six remain, which exceeds the commit quorum of five, so blocks continue to be proposed (round-robin skips the dead proposer's slots via round change) and committed.

Halt / fork / continue. Continues. No fork.

Status. PROVEN. Single-fault survival is demonstrated in the fault-tolerance work: in an N=4 (f=1) mixed-client run, killing one validator left the surviving three committing; the pure-Besu N=7 baseline sustains block production well inside the f=2 boundary. This is also the direct consequence of quorum math (six alive > five needed).

5.2 Two validators offline

Behavior. The chain continues, but it is at the exact fault-tolerance limit: with two of seven down, exactly five validators remain, which equals the quorum of five with zero slack. All five survivors must prepare and commit every block. In a 40-cycle adversarial soak (kill two random validators, measure a 45-second fault window, restart, measure recovery), the chain committed blocks in 37 of 40 cycles and, in 3 of 40 cycles, produced a temporary zero-progress ("stall") window. Those three stalls were temporary and self-recovering, not permanent halts and not forks: every stalled cycle resumed the moment the killed nodes restarted, with fork_during = False and resynced_after = True in all cases.

Halt / fork / continue. Continues at the limit. No fork in any of the 40 cycles. Under specific worst-case two-down proposer arrangements at the exact f=2 boundary, progress can pause briefly, but the chain is neither forked nor permanently stuck.

Status. PROVEN, with the boundary nuance reported honestly rather than rounded to "zero halts." Evidence: FAULT-TOLERANCE-CHARACTERIZATION-2026-07-14.md (0 forks / 40, 40/40 killed nodes resynced, 3/40 temporary self-recovering stall windows; pure-Besu N=7 kill-two reference showed 0 forks and 0 stalls over 20 cycles). The rare stall at the boundary is inherent to QBFT running with zero quorum slack, not a fork and not a safety failure.

5.3 Three or more validators offline

Behavior. The chain halts. With three of seven down, only four validators remain, which is below the commit quorum of five, so no block can reach quorum and progress stops. It halts cleanly: it does not fork, because no side can form a quorum, and it resumes exactly where it stopped once enough validators return.

Halt / fork / continue. Halts, safely. No fork.

Status. EXPECTED as the deterministic consequence of quorum math (four alive < five needed), and the sub-quorum halt-then-recover behavior itself is demonstrated (see network partition, below, and the hybrid-consensus negative controls where dropping the set below quorum halted block production in place and recovered on restoration with no re-genesis and no split). This specific "third of seven goes down" configuration follows directly from the quorum rule; it is not separately soak-characterized as its own experiment, and the claim as written rests on quorum math plus the demonstrated sub-quorum halt-and-recover.

5.4 Network partition

Behavior. On a network partition, the side of the partition that does not hold a quorum (at least five of seven validators) cannot commit blocks and halts. It does not fork: a minority partition can never form the 5-of-7 committed-seal quorum required to finalize a block, so it produces no competing finalized chain. When the partition heals and the validators reconnect, the halted side resumes and resyncs to the canonical head. This halt-then-recover behavior was demonstrated directly.

Halt / fork / continue. The minority side halts; the majority side (if one partition holds >= 5 validators) continues; on reconnection the halted side recovers. No fork.

Status. PROVEN (halt-then-recover demonstrated). Evidence: sub-quorum halt and in-place recovery were shown in the in-place PQC activation work (dropping below the required quorum halted block production at a specific height, and restoring the missing signers resumed from that exact height with no re-genesis) and in the hybrid-consensus negative controls (killing enough validators to break quorum halted the chain with no split and recovered in place). The single-operator caveat applies and is disclosed: all seven validators are Foundation-operated on Hetzner infrastructure, so a partition that is really an infrastructure or operator outage is a correlated failure, not an independent one. QBFT's partition safety (no fork) holds regardless; the availability of a quorum-holding side is an operational, not a protocol, guarantee at N=7 under one operator.

5.5 The two clients disagree on state (Nethermind vs Besu)

Behavior. The second client exists precisely to catch this. The patched Nethermind independently re-derives state: it has re-validated the full chain to genesis with zero invalid seals and re-executed real chain-2800 blocks to byte-for-byte identical block hashes and state roots (spot-checked across many heights, and, as a live listen-only follower, matched the live RPC's hash and state root at every checked height in range). Because there is exactly one definition of correct state and two independent implementations computing it, a consensus-relevant divergence between Besu and Nethermind (a differing state root, a differing block hash, a differing seal decision) is detectable by comparing the two: it does not silently pass.

Halt / fork / continue. This is a fail-safe (a cross-check), not an automatic consensus action. A detected divergence is a signal to halt and investigate before the divergent block is trusted, not something that itself forks or halts the live chain. Besu is the sole live producer today, so a Nethermind disagreement flags a discrepancy against the producer; it does not currently arbitrate consensus.

Status. PROVEN as a validation cross-check (full-chain re-validation, byte-identical state-root re-execution, and identical PQC precompile outputs). It is not yet a live, automated, alerting divergence gate wired into production monitoring, and Nethermind is not yet a live producing validator. Framed honestly: the second client demonstrably would detect a state divergence, and this is real client-diversity assurance; turning that into an automated live fail-safe gate is the remaining operational work.

5.6 A PQC precompile errors on its input

Behavior. The precompiles fail closed. On malformed or unexpected input they return a defined non-accepting output rather than reverting: the Falcon, ML-DSA, and SLH-DSA verifier precompiles (0x0AE1 through 0x0AE4) return a 32-byte zero word (which reads as "not verified"), and the SHAKE256 precompile (0x0AE5) returns empty on malformed framing. None of them revert, and none of them can affect consensus: they are pure verification functions at reserved addresses, so a bad input produces a not-verified result and nothing more. The integrator rule that travels with this is explicit: treat a zero-word or empty return as not-verified, and validate input lengths yourself.

Halt / fork / continue. The chain is unaffected. No revert of consensus, no halt, no fork. The calling contract simply sees a not-verified result.

Status. PROVEN. This as-shipped behavior was verified against the live chain and reconciled into the precompile documentation (the earlier draft's "MUST revert" framing was corrected to the actual fail-closed zero-word / empty-output behavior). Evidence: the AIP reconcile in aerenew/research/aip-draft-pqc-precompiles.md "As shipped" corrections.

5.7 The bridge goes down

Behavior. Cross-chain messaging stops; the L1 keeps running. The interop layer (the Hyperlane-compatible messenger, the intent and spoke contracts, and any relayer) sits entirely at the application layer and is not in the consensus or execution-critical path. If the bridge relayer or a counterparty deployment goes offline, outbound and inbound cross-chain messages stop being delivered, but Aere chain 2800 continues producing and finalizing blocks exactly as before.

Halt / fork / continue. The L1 continues. Only cross-chain message delivery halts. No fork.

Status. EXPECTED, by architectural isolation: the bridge is app-layer and the current bridge path is not even a live decentralized network yet (it runs through a single Foundation signer with a relayer pending), so its being down affects only cross-chain product surface, never L1 liveness.

5.8 The ZK prover is unavailable

Behavior. New proofs pause; the chain and all existing verified state keep running. The zk components (the rollup-validity anchor, the inbound Ethereum light client, the outbound QBFT light client) advance only when someone submits a proof: advancing is permissionless but not automatic. If the off-chain prover (the SP1 prover, run on dedicated non-infra hardware) is unavailable, no new finality advances or new validity proofs are recorded, but nothing already verified is rolled back, and the L1 itself does not depend on the prover to produce or finalize blocks.

Halt / fork / continue. The L1 continues. Only the production of new zk proofs pauses; previously verified state stands. No fork.

Status. EXPECTED, by design: the light clients' heads move only when a proof is submitted ("permissionless but not automatic"), and proving runs off-chain, off the infra box, so prover downtime cannot halt consensus. The honest boundary already stated for the zk path applies: it is trust-minimized, not trustless, and not quantum-safe (Groth16 over BN254).

---

6. Document Status and Reproducibility

This specification is the bridge between Aere's internal verification and an independent external audit. Its guarantees are backed by machine-checked formal verification and adversarial self-review, and every figure in it is intended to be reproducible from the published repositories and harness (that reproducibility is itself a roadmap item, tracked as the open-benchmark and reproducible-build work). Two standing honesty rules govern any use of this document:

1. Until an independent external audit completes, every guarantee reads as "internally verified, not externally attested."
2. The post-quantum scope boundary is absolute: signatures and accounts can be post-quantum; consensus (ECDSA / QBFT) and the on-chain ZK verifiers (BN254 Groth16) are classical. The chain as a whole is not post-quantum, and no derived material may claim otherwise.