Rust has the same level of rigour, other than lacking totality. Not having dependent types makes properties a lot more cumbersome and less practical to encode, but the actual proofs you get of the properties you do model are just as valid as those in Coq and Idris (modulo nontermination).