> Soundness and panic semantics. Kani interprets Hoare triples under partial correctness with panic safety: [omitted] means that if [omitted] holds and [omitted] terminates normally (without panicking), then [omitted] holds. Panics (from assert!, unwrap(), arithmetic overflow, or outof-bounds access) are translated into assertion violations and are therefore checked as part of the verification. A successful Kani run guarantees both the absence of panics and the postcondition, for all inputs satisfying the precondition, up to the following assumptions: harness coverage of reachable inputs, aliasing closure of Mod for unsafe code, user-guaranteed termination, sequential execution (no threads or async), no Stacked Borrows [28] / Tree Borrows [44] pointer-aliasing modeling (the primary class of UB in unsafe Rust), and FFI calls executing outside CBMC’s memory model unless stubbed (§4.6). The last two are the most significant in practice. Miri [30] checks aliasing violations dynamically, making it a natural complement.
tl;dr: you still need to run miri and hope for the best lol
bloody frauds