aion_verify

First-party proof engine, no_std, no unsafe, no external solver. TIER 4 enumerates: it checks a predicate against EVERY input in a bounded/enumerable domain, returning Proven{cases} or Refuted with the counterexample -- complete coverage, not a sample. Combinators: for_all, for_all_where, for_all_u8, for_all_in, for_all_pairs. TIER 5 proves properties over UNBOUNDED integer domains -- all 2^64 values of u64, any number of variables -- WITHOUT enumerating them, by interval abstract interpretation, via an Expr/Prop DSL and prove_contract for pre/postcondition contracts. Tier 5 is SOUND BUT INCOMPLETE: transfer functions over-approximate, so it answers Proven, Refuted with a concrete counterexample, or UNKNOWN when the abstraction is too imprecise (typically relational properties) -- never a false Proven or Refuted. An SMT-based checker such as Kani/CBMC decides cases this returns Unknown on, so Kani remains a stronger independent second opinion rather than being replaced.