Comment by worldsavior

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.