Yeah, Rust mostly just eliminates memory safety and data race problems, which is an enormous improvement compared to what we had previously. Unfortunately right now if you really want to write software that's guaranteed to be correct, there's not alternative to formal verification.
I would say it can go further than that: Rust enables you to construct many APIs in a way that can’t be misused. It’s not at all unique in this way, but compared with C or Go or the like, you can encode so many more constraints in types.
Only if the data structures aren't exposed to outside of the program, in which case, Rust cannot guarantee safety from data race problems caused by OS IPC mechanisms like memory mapped data, shared memory segments or DMA buffers, accessed by external events.
Minor nit: formal verification doesn't guarantee correctness.