“Formal verification” for Rust code -- does that actually exist yet, or do people just hope/assume that the language will be proven consistent and that awesome theorem-checking tools will emerge eventually?

I agree that Rust has a great model that seems to lead to very solid code, but “formal verification” is a high bar to clear.