Kani: A Model Checker for Rust

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/

[dead]

You have now created four accounts to make basically this post, but the point is unclear. All of the highly automated theorem provers have some limitations to what they can guarantee, some of which comically strict. You are not really explaining how this operating on MIR makes it so distinctly useless/"fraudulent".