aere-docs/REPRODUCE.md

REPRODUCE.md (spec-23): Verify Aere Network yourself

Prepared 2026-07-19. This is the single reproducibility manifest for Aere Network. It lets any third party re-run our tests, our formal verification, our cryptographic known-answer tests (KATs), and our benchmarks, and get the same results we get. Trust in a chain comes from reproducibility, not from slogans, so this document is deliberately literal: real paths, real commands, real expected outputs, and where a number cannot be freshly measured on a laptop, the exact command to measure it rather than an invented figure.

How to read the numbers in this file

Every quantitative claim below carries one of three honesty tags:

• [FRESH] means the number was produced by actually running the command on 2026-07-19 in the environment described under Provenance. It is a real, re-observed result.
• [CITED: file] means the number is taken from a committed artifact in this repository, and the file is named so you can open it and check. It was not re-derived from scratch for this document, though where a suite was cheap to re-run its green status was reconfirmed [FRESH].
• [MEASURE: command] means the figure has not been measured here (the toolchain is not installed on this machine, or the run is heavy or requires the isolated fork build). Run the stated command to produce and publish the real number. Do not quote a figure until you have.

Nothing in this file is a rounded-up guess. If you find a bare number without a tag, treat it as a bug in this document.

Provenance of the fresh runs

• OS: Windows 11 (the SMT and Node suites are OS-independent; the fork KAT and gas harnesses are Linux-only, see their sections).
• Python 3.14.4, z3 4.16.0 (python -c "import z3; print(z3.get_version_string())").
• Node v24.14.1, Hardhat present in aerenew/contracts/node_modules/.bin/hardhat.
• forge (Foundry) and halmos are NOT installed on this machine, so every Foundry or Halmos step below is tagged [MEASURE], never [FRESH].

1. What "verify yourself" means for Aere, and the honest scope

Aere's posture is radical about reproducibility and surgical about secrets. We publish the things that let you check our claims: contract source, the full test suites, the formal verification models, the NIST cryptographic vectors, and the benchmark harnesses. We never publish the things that would let someone impersonate the network or move funds: validator or Foundation private keys, infrastructure host addresses and access, internal business material, and the frontier research and development we hold private. Those two lists do not overlap, and this document only ever points at the first list.

Two things are true at once and we state both:

1. Aere mainnet (chain 2800) consensus is classical secp256k1 ECDSA QBFT (Hyperledger Besu fork), N=7 Foundation validators (fault bound f=2, quorum 5 of 7), 0.5 second blocks. It is NOT post-quantum. There is no Falcon certificate of any kind in any mainnet header.
2. The post-quantum work (Falcon log-only, blocking, and hybrid consensus modes) is isolated testnet research and development, and five NIST PQC precompiles are live on mainnet at 0x0AE1..0x0AE5 (from block 9,189,161) as an application-layer verification surface that does not change how consensus itself is signed. See [CITED: aerenew/conformance/README.md] and [CITED: aerenew/research-stage/formal-consensus/REPRODUCE.md] for the same boundary stated in the source.

The publish gate is mandatory (secret scan plus green CI)

No part of this bundle is published to a public remote until two gates pass, in this order:

• Secret scan. No private keys, no .env files with real values, no API tokens, no internal host addresses anywhere in the diff. The DevRel publishing flow gates publication on a secret scan pass and it must not be bypassed. See [CITED: aerenew/GITHUB_DEPLOYMENT_CHECKLIST.md].
• Green CI. Build, tests, and the secret scan run in CI, on a pull request, before merge.

Both gates are a hard prerequisite for step zero below. Preparing this manifest does not publish anything.

2. PASUL 0 (state the honesty gap plainly): make "open source" true before claiming it

Today the site, SDK docs, and press material reference Aere source repositories that do not yet resolve. This is a real over-promise and we name it rather than paper over it.

Confirmed references in the current tree:

• aerenew/sdk-js/README.md links to https://git.aere.network/aere-network/sdk-js, .../aere-network/aerenew, and .../aere-network/blocky-chain-forge.
• aerenew/tools/create-aere-pqc/README.md links to .../aere-network/sdk-js.
• aerenew/docs/aerecore/AERECORE_PLAN.md links to .../aere-network/aerecore.
• The press kit and press draft link to https://github.com/aerenetwork/aere-research, and the DevRel material references aerenetwork/aere-docs and aerenetwork/aere-contracts.

Reachability check on 2026-07-19: curl -s -o /dev/null -w "%{http_code}" https://git.aere.network/aere-network/aerenew returned 404 [FRESH]. Until the referenced repositories are actually published, the "open source" and "verify yourself" claims over-promise.

[VERIFY: individually curl each referenced repo path (git.aere.network/aere-network/{sdk-js, aerenew,blocky-chain-forge,aerecore} and github.com/aerenetwork/{aere-research,aere-docs, aere-contracts}); the aerenew path is confirmed 404, the rest are asserted from the same host and should be checked one by one before the site copy is trusted.]

Step zero of this bundle is to make the claim true: publish the real repositories, behind the secret scan plus green CI gate of section 1. Publishing itself is gated on clean accounts and is a manual step. This document does not perform it, and nothing here should be read as having pushed anything.

3. Reproduction sections (one per verifiable artifact)

3a. Contract test suites

What it proves. That the deployed Solidity behaves as claimed: PQC verifiers accept genuine signatures and reject tampered ones, escrow and custody accounting conserves funds, and the economics contracts have no admin escape hatch.

Primary functional surface: Hardhat (JavaScript). The functional test suite is Hardhat, not Foundry. It lives at aerenew/contracts/test/*.test.js.

cd aerenew/contracts
npm ci                          # installs the pinned toolchain (hardhat, OZ 4.9.x)
node scripts/run-tests-sharded.js --jobs 3    # the documented command, see below

THE SUITE NOW RUNS TO COMPLETION, AND IT IS NOT GREEN. Measured 2026-07-20.

The previous version of this file warned that npx hardhat test died with a segmentation fault at a point that moved between runs, and that we had not isolated it. We have now isolated it, and the honest result is below. It is not the result we would have chosen.

Diagnosis [FRESH]. The crash is native memory exhaustion, not a failing test and not the Node heap. Hardhat runs all 175 files under test/ inside one process hosting one long-lived in-process EVM (EDR, a native Rust addon), and that EVM materialises a per-opcode execution trace for every transaction. The pure-Solidity post-quantum verifiers are enormously expensive to execute: about 9.14 million gas per Falcon-512 verify [CITED: aerenew/pqc-fork/results/bench-results.json, the same figure quoted in section 3d], and about 10.7 million gas per recovery leg [CITED: the comment at aerenew/contracts/test/AerePQCSocialRecoveryModule.test.js line 513]. That is tens of millions of opcodes, so a single such transaction commits multiple GB of trace. Within one process those peaks are not returned to the OS, so the high-water mark only ratchets upward across the run until the OS kills the process. Three independent confirmations:

• A single npx hardhat test process was observed reaching 43,248 MB of private bytes before dying; a second, concurrent one died at 31,560 MB. The machine has 15.78 GB of RAM and a 55.5 GB commit limit, which is why the death point depends on what else is running, and therefore moves.
• aere-contracts/test/mldsa44Verifier.test.js prints memory allocation of 3623878656 bytes failed and aborts. That is a single failed 3.6 GB native allocation, which is a Rust allocator abort, not a V8 heap error.
• Run entirely alone on an otherwise idle machine, that same file still dies: npx hardhat test aere-contracts/test/mldsa44Verifier.test.js exits 139, "Segmentation fault" [FRESH]. The segfault therefore reproduces on one file and is not an artefact of suite length.

There is no supported switch that turns the tracing off. Hardhat 2.28.6 defines _setVerboseTracing but never calls it, and the EDR provider returns responseObject.traces on every request whether or not anything consumes it (see node_modules/hardhat/internal/hardhat-network/provider/provider.js lines 234 to 238).

The fix is a workaround and we label it as one. scripts/run-tests-sharded.js gives every test file its own process, so peak memory becomes the worst single file instead of the accumulated high-water mark of all of them. It reproduces hardhat's own file selection exactly (every .js under config.paths.tests, recursively). It does not eliminate the per-transaction cost, which is inherent to running post-quantum verifiers in-EVM under a tracing provider. Put these files back into one process and the crash returns.

Measured result [FRESH], node scripts/run-tests-sharded.js --jobs 3, 2026-07-20:

FILES:      175   OK=171  FAILING=3  CRASH=1
AGGREGATE:  2055 passing, 8 failing, 23 pending
WALL:       25.4 min at jobs=3

Per-file peak private bytes were sampled at 3 second intervals during that run. The median file peaks at 857 MB, 162 of the 175 files stay under 1 GB, and only 8 exceed 4 GB. The cost is concentrated in a handful of suites: mldsa44Verifier 28,384 MB, AerePQCSocialRecoveryModule 12,138 MB, interop/AereEthLightClient 11,208 MB, AereFalcon1024Verifier 10,243 MB, pqc-intents 6,642 MB, AereFalcon512Verifier 5,982 MB. Caveat on that attribution: peaks are matched to files by process id, and Windows reuses process ids, so a per-file figure is reliable only for the long-running heavy files listed here, which is why no full per-file memory table is published.

The four files that are not clean, with their actual messages [FRESH]:

1. aere-contracts/test/mldsa44Verifier.test.js, exit 139 (0xC0000409 when spawned directly on Windows). Native OOM as described above. It cannot complete on a 16 GB machine. Its first assertion, the official ACVP valid vector tc108, does pass before the process dies.
2. aere-contracts/test/interop/AereEthLightClient.test.js, 6 passing, 6 failing under the default config. The default hardhat network pins hardfork: "cancun", but this suite needs the EIP-2537 BLS12-381 precompiles, which arrive in Prague. Under cancun those precompiles are absent, hashToG2 returns all zeros, and every signature check fails with LC:bad signature. Re-run under the config that exists for exactly this reason, npx hardhat test aere-contracts/test/interop/AereEthLightClient.test.js --config hardhat.config.prague.js, and it becomes 7 passing, 5 failing [FRESH]: the BLS cross-check against noble now passes, and the 5 remaining failures are a single different defect, SSZ:branch len, a finality branch depth mismatch between the fixture and the contract. That is a real open bug, not a memory problem.
3. aere-contracts/test/compliance-pool.fuzz.test.js, 0 passing, 1 failing. Timeout of 600000ms exceeded on "survives 1500 randomized actions with all invariants intact". The fuzz does not finish inside its own 10 minute budget on this hardware. No invariant was reported violated; it ran out of time.
4. aere-contracts/test/invariant-lending-market-property.test.js, 0 passing, 1 failing. Transaction reverted without a reason string raised inside AereLendingMarket.liquidate via _healthyAtLiqThreshold (contracts/lending/AereLendingMarket.sol:464). A reasonless revert at that line is consistent with an arithmetic overflow panic in _scaleUp(col, ...) * _priceLiq(...) under the collateral and price magnitudes the property test drives. This is the one finding here that touches fund logic, because a liquidation that reverts contradicts the "liquidations never pause" invariant the contract's own comments claim. It is reported, not fixed, and it is not deployed-state advice: it is an open item.

npx hardhat test with no arguments is still the upstream command and it still dies. Use the sharded runner. If you want to confirm the defect yourself rather than take our word for it, run the single file in item 1 and watch the process size.

• Test file count: 170 files named *.test.js, and 175 .js files in total under test/ [FRESH] (find test -name '*.test.js' | wc -l = 170; find test -name '*.js' | wc -l = 175). The earlier figure of 137 in this file counted only the top level of test/ and was wrong for the purpose it was used for: hardhat globs config.paths.tests recursively and loads every .js file it finds, including the 5 non-test helpers, so 175 is the set actually executed. Those files hold 496 describe blocks and 2,046 it blocks [FRESH].
• Of those, 22 are invariant-property fuzz suites over burn, economics, and custody contracts [FRESH] (19 named *-invariant-property.test.js plus 3 named invariant-*-property.test.js; this matches the "22 invariant-property fuzz suites" figure in [CITED: aerenew/docs/AERE-ENGINEERING-SECURITY-SPEC.md]).
• Spot-check actually run here: npx hardhat test test/AereCryptoRegistry.test.js returned 42 passing (3s), exit 0 [FRESH] (artifacts were already compiled in contracts/artifacts, so no solc download was needed). This confirms the harness runs and a representative file is green on this machine.
• Full-suite result: 2,055 passing, 8 failing, 23 pending across all 175 files, 25.4 minutes at --jobs 3 [FRESH, node scripts/run-tests-sharded.js --jobs 3, 2026-07-20]. This is the first time the whole suite has been observed finishing. It is an aggregate over 175 separate processes, not one invocation, because one invocation cannot complete; that distinction is stated in the defect block above and must not be dropped when this number is quoted. The 8 failures and the 1 crashed file are enumerated there. The suite is not green, and no summary of this repository should say that it is. The older "161/161" figure from a historical milestone is superseded and must not be used.
• Machine-readable per-file results, including exit code and duration for every file, are written to aerenew/contracts/reports/sharded-test-run/results.json, with full stdout per file under reports/sharded-test-run/logs/.

Symbolic layer: Foundry plus Halmos. A foundry.toml sits beside the Hardhat project, deliberately scoped (its own out-forge/cache-forge, src = contracts/pqc, test = test/formal) so it does not disturb Hardhat. It exists for symbolic execution over three PQC contracts: aere-contracts/test/formal/AereCryptoRegistry.symbolic.t.sol, AerePQCAttestation.symbolic.t.sol, and AereSpokePool.symbolic.t.sol.

cd aerenew/contracts
# DO NOT use a bare `forge test` as a verdict. Measured on forge 1.7.1 in an isolated
# project: no tests at all exits 0, one passing test exits 0, one failing test exits 1.
# The exit code does not distinguish "everything passed" from "nothing ran", so a typo,
# a renamed function or a non-matching --match-path hands you a green tick for zero work.
# This wrapper runs the same command and then REFUSES unless at least PODEA_TESTE tests
# actually ran, reading the count out of forge's own summary.
PODEA_TESTE=9 bash ../scripts/forge-test-cu-podea.sh
halmos                     # symbolic execution of the *.symbolic.t.sol properties

forge test MEASURED, forge 1.7.1 on Windows, 2026-07-20:

Ran 3 test suites in 120.12ms: 9 tests passed, 0 failed, 0 skipped (9 total tests)

Two things had to be fixed before that command produced anything, and both are worth stating plainly because the honest previous status was "never run here":

• forge test did not COMPILE. contracts/intents/AereSpokePool.sol:586 hits "Stack too deep" in the legacy pipeline. via_ir = true is now set in foundry.toml, which is also the pipeline halmos is invoked with, so the two agree.
• forge test then found NO TESTS. The three *.symbolic.t.sol suites name their properties check_*, the halmos convention, and Foundry only collects functions beginning with test. The nine properties had therefore never been exercised by anything except halmos, and halmos is not installed here. test/formal/ForgePropertyFuzz.t.sol now wraps each one as a Foundry fuzz test, 256 runs each.

That is FUZZING, not proof. Foundry samples inputs; halmos explores them symbolically. Nine green fuzz properties mean no counterexample was found in 2,304 sampled executions. They do not establish the properties for all inputs and must never be described as formal verification. The symbolic obligation still belongs to halmos.

[MEASURE: halmos is still NOT installed on this machine (checked: halmos is absent from PATH, and there is no halmos in ~/.cargo/bin or any project venv). Install it and publish the per-property symbolic result. The security spec references "15 symbolic-execution proofs over the core contracts" [CITED: aerenew/docs/drafts/PRESS-RELEASE-DRAFT-2026-07-18.md]; the repository currently contains 9 check_* properties across 3 files, so 15 is a documented claim that does not match a fresh count and must not be repeated until reconciled.]

3b. Formal verification (z3 SMT, plus Halmos and Solidity SMTChecker)

What it proves. Safety-critical properties are machine-checked, not argued in prose. Each property P is proved by asserting NOT P under the exact protocol guards and showing z3 returns UNSAT (no counterexample). Every proof is paired with a negative control: the same model with one guard removed, which must return SAT (a real counterexample). If a control ever failed to fire, the model would be suspect. A green run is therefore both correct and demonstrably non-vacuous.

Consensus suite, publish target (10 models). Location: aerenew/research-stage/formal-consensus/ (curated copy prepared for the public research repo, with REPRODUCE.md and a committed expected-output.log).

pip install z3-solver
cd aerenew/research-stage/formal-consensus
python run_consensus_verification.py

Fresh result on 2026-07-19 [FRESH]:

  models run: 10   passed: 10
RESULT: ALL MODELS PASS (proofs PROVED, negative controls fired)

Counts from the fresh run: 173 PROVED verdict lines, 121 CEX-FOUND (negative-control) verdict lines, 0 FAILED, exit 0 [FRESH]. These verdict-line counts include both the per-check line and its echo in each model's SUMMARY block, so they are stable verdict counts rather than a count of distinct unique properties; they match the committed reference in [CITED: aerenew/research-stage/formal-consensus/REPRODUCE.md] exactly (that file records the same 173 PROVED / 121 CEX-FOUND / 0 FAILED under z3 4.16.0, Python 3.14.4). The ten models are qbft_safety, qbft_liveness, qbft_locking, qbft_prepare_counting, qbft_digest_keyed, falcon_logonly_noop, falcon_blocking, qbft_pqc_activation, falcon_hybrid_dualquorum, and threshold_account.

Consensus + contract suite, canonical in-tree (19 models: 8 consensus + 11 contract). The non-staging copy at aere-research/formal-consensus/run_consensus_verification.py now wires the 8 QBFT / Falcon consensus models AND 11 contract SMT models (fund-flow, registry, and PQC-verifier invariants), so a single canonical run covers them and prints a verdict-line tally. The 11 contract models are computemarket_smt, destinationsettler_smt, migrator_smt (escrow / filler / no-custody fund-flow), pqfinality_smt (Post-Quantum Finality Certificate accept guards: quorum ceil(2N/3), validator-set-root / size / attestation-domain binding, and rotation-invalidates-old-root), pqaggregate_smt (constant-cost t-of-n post-quantum aggregate authorization: committee-root and message-digest binding), credential_registry_smt (federated compliance trust: accreditation-to-issue, append-only status history, fail-closed verification), recovery_registry_smt (Falcon-512 append-only, strictly-increasing-nonce, fail-closed recovery evidence), plus the four added in this loop: ap2_mandate_smt (AereAP2MandateVerifier spend-authorization: cumulative spend stays within the mandate cap inductively, an expired or not-yet-valid mandate authorizes nothing, and the post-fix L3 executor gate blocks the open replay path), reputation_gate_smt (AereReputationRegistry8004 M1 fix: only an owner-authorized feedback author can move a score, and the forwarded delta is clamped to {-1,0,+1}), vectorstore_smt (AereVectorStore: version strictly increases by one per commit, the version history is append-only, every retrieval names a committed version 1..current, and a priced receipt is consumed at most once), and bitstring_status_smt (AereBitstringStatusList: a Revocation list's status bit is monotone / terminal so a revoked credential can never be un-revoked, the epoch strictly increases, and setting one bit leaves every other credential's bit unchanged). The runner still omits the hybrid dual-quorum and threshold consensus models from its list, though those .py files are present in the same directory and are run under the staging suite above.

cd aerenew/formal-consensus
python run_consensus_verification.py

Fresh result on 2026-07-19 [FRESH]: exit 0, all 19 of 19 models PASS (8 consensus + 11 contract), RESULT: ALL MODELS PASS (proofs PROVED, negative controls fired). The runner's own verdict-line tally on that run was 156 PROVED, 89 CEX-FOUND, 0 FAILED [FRESH]. That tally counts each model's per-check line once (the [PROVED ...] / [CEX-FOUND ...] lines), so it is a count of distinct property checks (proofs plus their firing negative controls), not of SUMMARY echoes. Of that total the four models added in this loop contributed 28 PROVED / 10 CEX-FOUND (ap2_mandate 9/3, reputation_gate 5/2, vectorstore 8/3, bitstring_status 6/2); the earlier four registry / PQC-verifier models contributed 29 PROVED / 10 CEX-FOUND (pqfinality 10/3, pqaggregate 7/2, credential_registry 7/3, recovery_registry 5/2); the three fund-flow models 26 PROVED / 11 CEX-FOUND (computemarket 16/3, destinationsettler 5/4, migrator 5/4); and the 8 consensus models account for the remaining 73 PROVED / 58 CEX-FOUND. Every contract model follows the same discipline as the rest of the corpus: each property is proved by asserting NOT-property under the real Solidity guards (z3 returns UNSAT), paired with a firing negative control that removes one guard and returns SAT (proving non-vacuity). Each contract model states its DESIGN-level boundary and its [VERIFY] trusted primitives honestly (for the PQC verifiers, SP1 gateway soundness and the un-implemented [MEASURE] off-chain zkVM aggregation circuit; for the Falcon-512 paths, the live precompile at 0x0AE1 and keccak256 injectivity; for the ERC-8004 mandate / reputation adapters, that the model bounds the adapter's guard logic and accounting, not the AERE402 rail's token movement or the live reputation's score formula).

Contract SMT models (9 models, escrow / custody / registry invariants). Same directory, aerenew/formal-consensus/. Each is a standalone z3 script.

cd aerenew/formal-consensus
for m in agentdid_lifecycle_smt agentdid_session_smt cryptoregistry_smt hybridauthorizer_smt \
         lending_liquidation_smt pqckeyregistry_smt settlementhub_smt spokepool_smt \
         threshold_account_smt; do python "$m.py" || echo "FAILED $m"; done

Fresh result on 2026-07-19 [FRESH]: all 9 of 9 models exit rc=0 (green). Per-model exit codes were 0 for agentdid_lifecycle, agentdid_session, cryptoregistry, hybridauthorizer, lending_liquidation, pqckeyregistry, settlementhub, spokepool, threshold_account.

The aggregate property count for these 9 contract models is 125 proved properties plus 49 counterexample negative controls [CITED: aerenew/docs/SECURITY-POSTURE-VERIFICATION-2026-07-15.md (line 171), also aerenew/docs/AERE-ENGINEERING-SECURITY-SPEC.md]. The per-model breakdown recorded in that doc is agentdid_lifecycle 15, agentdid_session 11, cryptoregistry 12, hybridauthorizer 17, lending_liquidation 11, pqckeyregistry 13, settlementhub 15, spokepool 26, threshold_account 5, which sums to 125. The two highest-risk fund-flow models are the load-bearing ones: settlementhub_smt.py proves balanceOf(hub) >= committedLiabilities inductively, and spokepool_smt.py proves bal >= totalLocked + totalBond inductively. [MEASURE: to publish the exact fresh per-model property counts rather than the cited 125/49, run each model and read the SUMMARY block; the counting convention varies per model (some checks are parameterized over several validator-set sizes), so re-derive the aggregate with a single agreed counting rule before restating 125/49 as a freshly measured figure. The green (rc=0) status of all nine is freshly confirmed above.]

Optional secondary cross-check (not a proof). A Quint spec FalconQuorum.qnt is a randomized simulation used only as an independent sanity check:

npm i -g @informalsystems/quint      # reference version 0.32.0
quint run FalconQuorum.qnt --main=n7 --invariant=safety --max-samples=20000 --max-steps=1

Halmos and Solidity SMTChecker over the contracts are the symbolic complement to the z3 design-level models; see section 3a for the Halmos command and its [MEASURE] tag.

Honest boundary for all SMT models. The quorum-intersection lemma, the blocking-liveness identity, and the threshold arithmetic are proved for all N via decidable linear integer arithmetic. The one-round, cross-round, safety, and progress checks are bounded model checks over finite configurations (mainly N in {4,5,7}). A bounded model check is a decision procedure over that finite configuration, not a proof for all N or all execution lengths. Liveness assumes partial synchrony (post-GST), which is standard for QBFT and forced by FLP. These models check the protocol design mathematics, not the compiled client bytecode. Stated plainly, per [CITED: aerenew/research-stage/formal-consensus/REPRODUCE.md].

3c. PQC KAT / ACVP harness

What it proves. That the PQC verifier implementations accept the official NIST vectors and reject crafted-invalid inputs, so "NIST-conformant" is a checkable statement rather than a label.

Contract-level KATs (run under Hardhat, no fork build needed). The committed vectors live in aerenew/contracts/test/ and aerenew/contracts/test/fixtures/:

Scheme	Vector file	Committed conformance
Falcon-512	aere-contracts/test/falcon512_kat0.json	official NIST round-3 KAT, vector 0 [CITED: test/AereFalcon512Verifier.test.js]
Falcon-1024	aere-contracts/test/falcon1024_kat0.json	official round-3 KAT
ML-DSA-44 (Dilithium2, FIPS 204)	aere-contracts/test/fixtures/mldsa44-acvp-tg8.json	15/15 NIST ACVP sigVer cases [CITED: aerenew/aips/AIP-4.md]
SLH-DSA / SPHINCS+-SHA2-128s (FIPS 205)	aere-contracts/test/fixtures/sphincs-sha2-128s-acvp-tg31.json	14/14 NIST ACVP sigVer cases [CITED: aerenew/aips/AIP-4.md]
XMSS-SHA2_10_256 (RFC 8391)	aere-contracts/test/fixtures/xmss-sha2_10_256-kat.json	RFC 8391 KAT

cd aerenew/contracts
npx hardhat test test/AereFalcon512Verifier.test.js   # SHAKE256, HashToPoint, accept + tamper-reject
npx hardhat test test/AereFalcon1024Verifier.test.js
npx hardhat test test/AereSphincsVerifier.test.js

The Falcon-512 test asserts, among others, that the FIPS 202 SHAKE256 empty-string vector reproduces 0x46b9dd2b0ba88d13233b3feb743eeb243fcd52ea62b81b82b50c27646ed5762f, that HashToPoint reproduces the reference challenge polynomial, and that a genuine signature accepts while a tampered one rejects. [MEASURE: run the three commands above and publish each "N passing" line. Only the CryptoRegistry file was executed for this document (42 passing, 3a).]

Fork-level precompile KATs (require the isolated Besu PQC fork build, Linux). These feed the committed NIST ACVP vectors to the native precompiles and assert accept plus crafted-invalid reject. Location aerenew/pqc-fork/.

cd aerenew/pqc-fork
bash setup-fork.sh     # clone besu@d203201, overlay fork EVM layer, add precompiles, compile
bash build-dist.sh     # ./gradlew installDist (one full build)
bash run-kats.sh       # ML-KEM-768 (NIST ACVP) + Falcon HashToPoint (Python SHAKE256 cross-check)

Committed results, to be reconfirmed by a fresh run:

• ML-KEM-768 (FIPS 203) at 0x0AE6: 25/25 NIST ACVP encapsulation cases PASS [CITED: aerenew/pqc-fork/results/kat-results-mlkem.json].
• Falcon HashToPoint (SHAKE256 rejection sampler) at 0x0AE7: 12/12 PASS, cross-checked against an independent Python hashlib.shake_256 oracle [CITED: aerenew/pqc-fork/results/kat-results-hashtopoint.json].

[MEASURE: run-kats.sh targets the Besu build tree and staging directory on the isolated fork host and cannot run on this machine or on any production host (heavy build; the infra box runs live services and must never take heavy compute). Reproduce on a scratch Linux box and publish the two result JSONs. The Rust acceleration crate has its own KATs: cd aerenew/pqc-accel && cargo test (integration tests slhdsa_kat, scalar_hash_kat); [MEASURE: run cargo test and publish the result, cargo is not exercised here].]

3d. Benchmark harness (gas)

What it proves. What each signature scheme actually costs on-chain, and how much the native precompile saves versus a pure-Solidity verifier.

Precompile gas schedule (marginal verify-op gas). These are the per-operation gas charges for the native precompiles, defined in the fork source and specified in [CITED: aerenew/aips/AIP-7.md] and [CITED: aerenew/conformance/README.md]:

Scheme	Marginal verify-op gas	Full verify-and-record tx gasUsed (measured on fork)	Share of 2^24 cap
ecrecover (secp256k1)	3,000 (protocol standard)	n/a	n/a
P-256 / secp256r1 (RIP-7212/7951 at 0x100)	3,450	n/a	n/a
Falcon-512	40,000	86,336	0.51%
Falcon-1024	75,000	145,496	0.87%
ML-DSA-44	55,000	351,050	2.09%
SLH-DSA-SHA2-128s	350,000	558,276	3.33%
ML-KEM-768 encapsulate (0x0AE6)	60,000	n/a	n/a
SHAKE256 / HashToPoint (0x0AE7)	60 base + 12/word	n/a	n/a

Sources: the marginal and full-tx columns are [CITED: aerenew/aips/AIP-7.md] (table at lines 92-98); ecrecover 3,000 is [CITED: aerenew/docs/AERE-ENGINEERING-SECURITY-SPEC.md]; P-256 3,450 is [CITED: aerenew/aips/AIP-6.md and aerenew/docs/AERE-EIP-COMPATIBILITY-MATRIX.md]; the ML-KEM 60,000 and HashToPoint 60-base constants are read directly from the precompile source [CITED: aerenew/pqc-fork/precompiles/MLKEM768PrecompiledContract.java (GAS = 60_000L) and HashToPointPrecompiledContract.java (BASE_GAS = 60)]. Honest caveat from [CITED: aerenew/conformance/README.md]: precompile gas is documented in the fork source but the conformance vectors pin outputs, not gas schedules, so gas conformance is a stated next addition.

[MEASURE: the full verify-and-record gasUsed figures (86,336 / 145,496 / 351,050 / 558,276) were measured once on the isolated fork and committed to the AIP. To reproduce them freshly, build the fork (section 3c) and run a verify-and-record transaction per scheme through the live precompiles, then publish the receipt gasUsed. Do not restate these as current unless re-measured.]

Precompile-versus-Solidity Falcon-512 gas benchmark. aere-research/bench/bench.py deploys the pure-Solidity verifier and the precompile-backed variant on a single-node QBFT fork, runs the same Falcon-512 KAT vectors through both, and reports receipt gasUsed and accept/tamper-reject.

cd aerenew/pqc-fork
bash bench/start-node.sh
python3 bench/bench.py

Committed result [CITED: aerenew/pqc-fork/results/bench-results.json], 8 vectors, integration_all_pass: true, chainId 28777:

• Average in-EVM Falcon-512 verify: 9,140,858 gas, precompile-backed: 7,186,367 gas, a 21.4% drop.
• HashToPoint step alone: 2,281,180 to 311,480 gas, roughly an 86% drop.

[MEASURE: bench.py assumes the fork node at 127.0.0.1:8545 and solc on PATH; it is Linux/fork tooling and was not run here. Rebuild the fork, run it, and publish the fresh bench-results.json.]

Chain and zkVM benchmarks. The 273,000 TPS figure is a design ceiling from synthetic benchmarks, not a measured mainnet steady-state number, and must be stated that way if it appears at all [CITED: aerenew/GITHUB_DEPLOYMENT_CHECKLIST.md]. [MEASURE: any chain-throughput or zkVM proving-time number belongs here only with the harness command and a fresh run; none is asserted in this document.]

4. Coverage and mutation

Neither of these is a claimed number. Both are commands to run and publish.

Coverage. The one command.

cd aerenew/contracts
npm install
bash scripts/coverage/run-coverage.sh

That is the whole procedure from a clean checkout. It takes HOURS, not minutes, and it needs the contract tree to sit still for the duration. Read the next three paragraphs before you run it or before you quote anything it produces.

Why it is not just npx hardhat coverage. A single-process whole-repo coverage run does not fit in memory on a 16 GB machine. MEASURED: the coverage process was observed reaching 33.23 GB private bytes against a 33.78 GB commit limit and being killed by the OS with no report. So the driver shards the suite across many hardhat coverage processes and merges the istanbul JSONs. Summing shard counters is valid only if every shard instrumented byte-identical sources, so the driver fingerprints the contract tree with scripts/coverage/tree-fingerprint.js before the first shard and re-checks it after every single shard. If a contract is added or edited mid-run it ABORTS with exit 3 and writes no aggregate, because a merge across two different instrumentations is not a lower-quality number, it is a wrong one. That failure is why an earlier run of this suite could not be merged at all.

Expected output. On success the last lines are:

=== DONE ===
the number      : <OUTDIR>/aere-coverage-summary.json
what to distrust: <OUTDIR>/AERE-COVERAGE-README.md
unmeasurable    : <OUTDIR>/shards/unmeasurable.txt (N test files)

aere-coverage-summary.json is the ONLY file in the run that is the coverage figure. Read its totals object. It also carries treeFingerprint, the sha256 of the exact contract tree measured; a coverage number published without that fingerprint is not reproducible and should not be quoted.

Three artifacts that will mislead you, and they mislead DOWNWARD. MEASURED on the July 2026 run:

Artifact	What a reader would conclude	What it actually is
shards/shard-NNN.partial-istanbul.json	1.27% statements	one shard's hits against the whole tree's denominator
<report dir>/coverage-final.json	1.27% statements	solidity-coverage overwrites its report folder per invocation, so this is whichever shard finished last. The driver now renames it to LAST-SHARD-ONLY-NOT-THE-COVERAGE-NUMBER.json.
the merged istanbul file's l counters	0.25% lines	istanbul's line counters are derived data and were being carried over unmerged from the first shard. merge-shards.js now recomputes l from statementMap plus the summed s, so this trap is closed rather than labelled.

We fixed these by renaming (the first two) and by recomputing the stale counter (the third), and AERE-COVERAGE-README.md is written into every run directory naming each one.

The number is a LOWER BOUND, and the gap is in the technology we talk about most. Some suites cannot be instrumented on this machine at all. MEASURED for aere-contracts/test/mldsa44Verifier.test.js, a 2.7 KB file with 4 test cases:

# uninstrumented: passes in a 256 MB heap
node --stack-size=8000 --max-old-space-size=256 \
  ./node_modules/hardhat/internal/cli/bootstrap.js test aere-contracts/test/mldsa44Verifier.test.js
#   -> 4 passing (1m)

# instrumented: dies in a 8192 MB heap
NODE_OPTIONS=--max-old-space-size=8192 \
  npx hardhat coverage --config hardhat.config.coverage.js \
  --testfiles aere-contracts/test/mldsa44Verifier.test.js
#   -> FATAL ERROR: Reached heap limit Allocation failed

A thirty-fold heap multiplier on a file whose fixtures are measured in kilobytes rules out fixture size as the cause. The cost is solidity-coverage's per-statement bookkeeping executing inside a single ML-DSA-44 verification that costs roughly 52.9 million gas, where the same statements run millions of times in one process. Fourteen test files behave this way, disproportionately the post-quantum verifier suites, so THOSE CONTRACTS READ AS ZERO PERCENT COVERED even though their tests pass outside the coverage harness. The driver's answer is to split below the file and run one it per process (scripts/coverage/list-test-cases.js plus the micro_shard stage); where a suite's test titles are built from template literals in a loop, splitting would silently skip cases, so the driver refuses to split and leaves the file listed in unmeasurable.txt instead. Read that file before quoting the aggregate.

Coverage, Foundry path.

cd aerenew/contracts
forge coverage --ir-minimum

MEASURED, and it does NOT work today: forge 1.7.1 fails to compile the coverage build with Yul exception: Cannot swap Variable var_sigLen with Variable var_sig_length: too deep in the stack by 1 slots. forge coverage refuses a plain via_ir build, and --ir-minimum turns the optimizer down far enough that a PQC signature-verification function no longer fits the stack. No Foundry coverage number exists for this repository and none should be quoted until that is resolved.

Mutation testing.

# Solidity mutation testing, e.g. a Gambit or vertigo-style run over contracts/contracts,
# scored against the Hardhat suite:
# (tool not pinned in-repo yet) install the chosen mutation tool, then run it against the suite.

[MEASURE: select and pin a mutation-testing tool, run it against the Hardhat suite, and publish the mutation score (killed / total). No mutation number is claimed here.]

5. What is NOT in this bundle

By design, this reproducibility bundle excludes:

• Keys. No validator or Foundation private keys, no signing material, no .env with real values, no API tokens. Deployed contract addresses are public and checkable via eth_getCode on https://rpc.aere.network; the keys that control them are not here and never will be.
• Infrastructure. No host addresses, SSH access, nginx or firewall configuration, relayer, oracle, or indexer operational material. The live infra box runs production services and must never take heavy compute; every heavy harness in this document is explicitly routed to a scratch box or the fork host, not to infra.
• Business material. No funding, cost, partner, or internal-operations content. Public copy is scrubbed of it as a matter of policy.
• Frontier research and development held private. Only the "verify-yourself" core (already public or intended for the public research repo) is in scope. Private frontier work stays private; the moat is the live network, not the unpublished code.

Publishing any of section 3's artifacts remains gated on the secret scan plus green CI of section 1, and on the account-readiness that gates step zero of section 2. This document prepares the verification story; it does not push anything.