Aere Network public source. Everything here can be checked against the live chain (chain id 2800, https://rpc.aere.network). Scope note, stated up front rather than buried: consensus on chain 2800 is classical secp256k1 ECDSA QBFT. The post-quantum work in this repository is at the signature, precompile, account and transport layers. Nothing here makes the consensus post-quantum, and no document in it should be read as claiming so.
3.8 KiB
aere-research
Formal verification models, post-quantum cryptography reference implementations, known-answer tests (KATs), and research specifications for Aere Network.
This repository is the "prove it yourself" half of the Aere Network verify-yourself core. It lets a third party re-run the machine-checked proofs, re-derive the cryptographic reference vectors, and read the research that underpins the protocol, without trusting any claim on faith.
Scope, stated up front
Aere Network runs post-quantum signature verification natively on mainnet: Falcon-512 (0x0AE1),
Falcon-1024 (0x0AE2), ML-DSA-44 (0x0AE3), SLH-DSA-128s (0x0AE4) and SHAKE256 (0x0AE5)
have been live as precompiles since block 9,189,161. You can call them yourself against
https://rpc.aere.network without asking us for anything.
Consensus on chain 2800 is classical secp256k1 ECDSA QBFT. The post-quantum work lives at the signature, precompile, account and transport layers. Nothing in this repository makes the consensus post-quantum, and nothing in it should be read as claiming so. Where you see post-quantum consensus discussed, it is research about what a future activation could look like, not a description of the running chain.
Two further limits worth knowing before you judge anything else here:
0x0AE6(ML-KEM-768) and0x0AE7(Falcon HashToPoint) are testnet only. They are not active on mainnet.- The on-chain zero-knowledge verifiers are classical BN254. They are broken by Shor's algorithm like any other elliptic-curve construction, and we do not describe them as quantum-safe.
The network is operated by seven Foundation-run validators, so its Nakamoto coefficient is effectively one today. That is a real limitation, it is on the roadmap, and it is not fixed by any code in this repository.
Layout
formal-consensus/Z3 / SMT models of consensus and contract safety properties (30 Python models plus a Quint specFalconQuorum.qnt), driven byrun_consensus_verification.py. These cover QBFT safety and liveness, the money-contract invariants, and a PROPOSED hybrid dual-quorum activation that is modelled research and is NOT running on chain 2800, and the invariants.CONSENSUS-VERIFICATION-2026-07-12.mddocuments the results.pq-stark/reference implementations and self-tests for the STARK verifier port: BabyBear field, Poseidon2, MMCS, FRI, the Fiat-Shamir challenger, and AIR quotient logic. Each component ships a Python reference, a JavaScript (.mjs) reference, a Java self-test, ground-truth JSON vectors, and a spec. The*-extractor/directories are small Rust reference extractors (source only). This is reference and test material, not key material.precompiles/Java sources for the post-quantum EVM precompiles (ML-KEM-768, Falcon HashToPoint, SP1 STARK verifier).kat/andvectors/NIST ACVP and Falcon known-answer test vectors and their generators.pq-finality-circuit/XMSS verify-core reference (Rust source) for the post-quantum finality circuit.bench/andresults/benchmark harness and recorded KAT / benchmark result JSON.aips/the Aere Improvement Proposal process and the accepted AIPs.research/research notes and long-form specifications (research/specs/).
Verify
The formal models run with Python 3 and z3:
cd formal-consensus
python run_consensus_verification.py
The STARK references are cross-checked against their ground-truth vectors; see each
spec-*.md and the test_*.py files. Full commands and expected outputs are in the aere-docs
repository (REPRODUCE.md).
What is deliberately not here
No private keys, no validator or Foundation key material, no infrastructure hostnames or credentials. Heavy prover runs must be executed on a throwaway non-infrastructure machine, never on production infrastructure.
License
MIT. See LICENSE.