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".
This is really weird. Someone creating 4 new accounts just to call this project fraudulent because it can't statically analyze every property you'd like? Does this person have a personal grudge against the author, or something?
Kani Rust Verifier – a bit-precise model-checker for Rust - https://news.ycombinator.com/item?id=30786511 - March 2022 (12 comments)
Reminds me a bit of hypothesis auto in its simplest applications: https://github.com/timothycrosley/hypothesis-auto/