Comment by Jtsummers

https://verus-lang.github.io/verus/publications-and-projects... - The papers here go into their implementation. They take the proof statements and information about the program and turn it into an SMT problem (and run it through Z3 if I read correctly) and then they use that to prove the properties of the program.

SPARK/Ada and Dafny work similarly, and have good documentation if you want to try your hand at something with a (presently) better set of documentation.

https://mitpress.mit.edu/9780262546232/program-proofs/ - Dafny book, pretty good tutorial on the topic

https://learn.adacore.com/courses/intro-to-spark/chapters/01... - Free tutorial for SPARK