Rust is supposed to be a "safe" language for low level use, and thus has borrow checker, unsafe, etc. Building a "verifier" on top of Rust seems a bit excessive and unneeded.
> Developers write specifications of what their code should do ... Verus statically checks ... the specifications for all possible executions of the code
This is what tests are for.