Claim #1 — Verification of even_or_odd::is_even (with kani 0.68.0)
pub fn is_even<T>(number: T) -> bool where T: std::ops::Rem<Output = T> + std::cmp::PartialEq<T> + From<u8>Tool: kani 0.68.0
Preconditions
true
Evidence
What is trusted
From the report
The result relies on Kani and CBMC correctly modeling and checking Rust u32 operations. No user-defined stubs or assumed helper contracts are used.
Technical limitations
From the report
Only is_even instantiated with u32 is covered. Other instantiations of this generic API, custom trait implementations, and is_odd are not verified. Equivalence of the entire verification fork to the crates.io release is not formally proved.
Tool limitations
Verification is scoped to the selected harnesses, assumptions, concrete types, target architecture, and any stubs or models used. Kani does not detect every form of Rust undefined behavior. In particular, data races and violations of reference aliasing rules are not fully checked. Uninitialized-memory checks require experimental support. Concurrent execution and panic stack unwinding are not modeled. A successful run should not be interpreted as excluding all Rust UB. References: https://model-checking.github.io/kani/undefined-behaviour.html https://model-checking.github.io/kani/rust-feature-support.html