Proof happens before compilation, and doesn't require compilation. You can follow the Verus tutorials for the specifics, but you can use it as a standalone veri

Proof happens before compilation, and doesn't require compilation. You can follow the Verus tutorials for the specifics, but you can use it as a standalone verifier or as a compilation "stage" where it'll run its verification and then conditionally continue on to compilation. Their tutorial seems ok: https://verus-lang.github.io/verus/guide/overview.html https://verus-lang.github.io/verus/guide/overview.html But if you want a more complete tutorial on this concept using similar tools (so what you learn from them will transfer well to Verus, even if you need to learn Verus or Rust specific details) check out Dafny or SPARK/Ada. The latter is mature and used in some parts of the software industry today. The former, I don't know if anyone actually uses it in production though theoretically you can (it generates code in several languages, I have not used it for that myself, just in an instructional capacity).