aion_verify 3.0.0

A two-tier proof engine, pure Rust: tier 4 checks a predicate against EVERY input in a bounded domain (exhaustive); tier 5 proves properties over UNBOUNDED, multi-variable domains (all of u64) via interval abstract interpretation, including function CONTRACTS (precond -> postcond) — Proven / Refuted-with-witness / honest Unknown, never a false result. no_std, no unsafe, no external solver. A first-party alternative to symbolic model checkers like Kani.
Documentation

Builds

aion_verify's sandbox limits

All the builds on docs.rs are executed inside a sandbox with limited resources. The limits for this crate are the following:

Available RAM 6.44 GB
Maximum rustdoc execution time 15m
Maximum size of a build log 102.4 kB
Network access blocked
Maximum number of build targets 10

If a build fails because it hit one of those limits please open an issue to get them increased.