Static verification of function pre- and post-conditions for Rust.

Not as powerful as full dependent types, but could be a good middle ground between something like ATS and down-to-earth plain Rust.