Flux is a refinement type checker for Rust that lets you specify a range of correctness properties and have them be verified at compile time.
See the examples -- listed in the summary on the left -- to learn about Refinement types and Rust.
You can try it online here.