Formal verification doesn't have to verify the entire functionality of the program to be useful; Rust's type system is supposed to formally verify that your program has no memory safety bugs.

(It doesn't. Because formal verification is hard. See cve-rs for how to corrupt memory without unsafe. Rust has stated they do not intend to fix cve-rs.)