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.