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

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.