Flux

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 these examples to learn about Refinement types and Rust.

You can try it online here.