Undefined Behaviour as usual

The thing to bear in mind is that, technically, the type checking in a safe language is also a valid proof of safety (or else it would not type check). So every safe Rust program (and every Java program, etc.) is verifiably safe, assuming the type system is sound.*

The question is, is that good enough? Most formal verification wants to prove more than "mere" type safety or soundness, and that tends to be hard because the property you're trying to prove is complex and highly specific to the individual application. But if you just want to prove a lack of UB, that's probably more feasible.

* There are soundness bugs in the current implementation of Rust. Most of them are rather hard to trigger accidentally, but they do exist.