On the verification side, it's never had more users that I'm aware of. SPARK and Frama-C are very active compared to almost non-existent use of formal methods in industry decades ago. Rust could similarly have a subset integrated with Why3 platform to make the formal methods easier to use. Further, I've seen extraction done from Coq to C and Rust. There's also one person modeling C in WhyML to write the algorithms in the latter but extract to former. Or something like that. Could be done for Rust, too.
On the verification side, it's never had more users that I'm aware of. SPARK and Frama-C are very active compared to almost non-existent use of formal methods in industry decades ago. Rust could similarly have a subset integrated with Why3 platform to make the formal methods easier to use. Further, I've seen extraction done from Coq to C and Rust. There's also one person modeling C in WhyML to write the algorithms in the latter but extract to former. Or something like that. Could be done for Rust, too.