Crate aion_verify 

AION OS — first-party proof engine (aion_verify).

“Our validation and proof functions should do everything Kani does” — for enumerable and bounded domains, this delivers exactly that: it checks a predicate against every input in the domain and returns a Verdict of either Proven { cases } (complete coverage — a proof) or Refuted with the counterexample that broke it. That is the same guarantee a bounded model checker gives over a bounded space: not a sample, the whole space.

What it does NOT do (and why Kani stays): it brute-force enumerates, so it cannot cover astronomically large domains the way Kani’s symbolic/SAT reasoning (CBMC) can. So aion_verify is the everyday, first-party tier-4 engine for finite/bounded invariants, and Kani (tier 5) remains the independent, third-party proof — symbolic coverage of the large cases plus an outside confirmation of ours. Two tiers, two independent methods, per AION’s validation doctrine.

no_std, #![forbid(unsafe_code)].

Modules

ledger

A tamper-evident, append-only hash-chain ledger (with a pure-Rust SHA-512) for recording proof results so they cannot be forged or silently deleted. A tamper-evident, append-only ledger for proof results.

mss

Many-time post-quantum signatures: a Merkle tree (mss, XMSS-style) over the one-time WOTS, so one published root signs 2^height proofs from a single key. Many-time post-quantum signatures — a Merkle Signature Scheme (XMSS-style) over the one-time WOTS of crate::pqsig.

pqsig

Post-quantum authenticity: a hash-based (WOTS) pqsig signature over the ledger head, so the log is provably yours and immune to Shor’s algorithm — using only SHA-512, still zero-dependency. Post-quantum authenticity — a WOTS (Winternitz one-time) hash-based signature over SHA-512.

symbolic

TIER 5 — symbolic verification over unbounded domains (interval abstract interpretation). Proves properties over all of u64 without enumerating it, entirely in first-party Rust. See symbolic. TIER 5 — symbolic verification over unbounded integer domains, in pure Rust.

Enums

Verdict

The outcome of a proof attempt over a domain.

Functions

for_all

Prove pred holds for EVERY item produced by inputs. Complete coverage of the domain = a proof.

for_all_in

Exhaustive proof over the inclusive range [lo, hi].

for_all_pairs

Exhaustive proof over the cartesian product of two finite domains (binary invariants). Returns the (a, b) pair that breaks pred, if any.

for_all_u8

Exhaustive proof over the entire u8 domain (all 256 values).

for_all_where

Like for_all but only over inputs satisfying precond — the equivalent of a kani::assume guard. Proves pred on every input where the precondition holds.