aion_verify

An exhaustive bounded proof engine for Rust. Check a predicate against every input in a finite or bounded domain and get back either a proof (Proven { cases } — complete coverage) or the exact counterexample that broke it (Refuted). Not a random sample — the whole space.

• no_std, zero dependencies, #![forbid(unsafe_code)].
• A real proof over the domain, not property-based fuzzing: if it says Proven, every input was checked.
• Returns the counterexample on failure, so a red result is immediately actionable.

Why

Property-based testing (proptest, quickcheck) samples an input space and can miss the one value that breaks your invariant. Symbolic model checkers (like Kani) prove properties over astronomically large spaces with a SAT/SMT backend, but need a toolchain and can be slow. For the very common case of a finite or small bounded domain — every u8, a range, a cartesian product of a few slices — you can just check all of it, fast, in plain safe Rust. That's aion_verify.

It was built as the tier-4 engine of the AION OS verification stack, alongside Kani as the independent tier-5 formal check. It complements Kani; it does not replace it.

Example

use aion_verify::{for_all_u8, for_all_in, for_all_pairs};

// Prove a property over the entire u8 domain (all 256 values):
let v = for_all_u8(|x| (x as u16) + 1 > x as u16);
assert!(v.is_proven());
assert_eq!(v.cases(), 256); // every input checked — a proof

// A failing property hands you the counterexample:
let v = for_all_u8(|x| x < 200);
assert_eq!(v.counterexample(), Some(&200u8));

// Bounded ranges and cartesian products of finite domains:
let v = for_all_in(0, 1000, |x| x * 2 >= x);
assert!(v.is_proven());

let a = [1u32, 2, 3];
let b = [10u32, 20];
let v = for_all_pairs(&a, &b, |&x, &y| x + y == y + x);
assert!(v.is_proven());

API

Each returns a Verdict<T>: is_proven(), cases(), and counterexample() -> Option<&T>.

When to reach for something else

aion_verify enumerates, so it's for domains you can actually iterate. For unbounded or astronomically large spaces, use a symbolic tool like Kani (the two pair well: prove the small/bounded cases exhaustively here, the large cases symbolically there).

License

Licensed under the Mozilla Public License 2.0 (MPL-2.0) — a file-level copyleft.

In plain terms: you can use aion_verify in any project, including proprietary ones, but any modifications you make to its source files must themselves be released under the MPL-2.0 (i.e. kept open source). Improvements to the engine stay free for everyone; the wider project you build around it does not have to be. Contributions submitted for inclusion are licensed under the same terms.

Note: 0.1.0 was briefly published under MIT/Apache-2.0 and has been yanked; 0.2.0 onward is MPL-2.0.