"Dafny’s ability to statically check critical properties of your program goes well beyond what mainstream languages can do (that includes you, Rust)."
Ada supports Design by Contract preconditions, postconditions, and type invariants that were pioneered by the Eiffel programming language:
https://learn.adacore.com/courses/intro-to-ada/chapters/cont...
The SPARK subset of Ada also does static proofs / formal verification:
https://learn.adacore.com/courses/intro-to-spark/chapters/01...
===
Rust has Design by Contract capabilities via the contracts crate:
https://docs.rs/contracts/latest/contracts/
Maybe one day Rust will have formal verification too?
Work is under way: https://alastairreid.github.io/automatic-rust-verification-t...
You might be interested in the Prusti project, which statically checks for absence of reachable panics, overflows etc. It also allows user-defined specifications such as pre and post-conditions, loop body invariants, termination checking and so on.