Is Miri still required?

The answer is yes:

> Soundness and panic semantics.

> (...)

> Panics (from assert!, unwrap(), arithmetic overflow, or out- of-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.

Bloody frauds, you must still run Miri and hope for the best.

Their old paper: https://dl.acm.org/doi/pdf/10.1145/3510457.3513031

The tutorial is helpful: https://model-checking.github.io/kani/kani-tutorial.html

Reminds me a bit of hypothesis auto in its simplest applications: https://github.com/timothycrosley/hypothesis-auto/