Formal proofs in the Rust language

I remember reading that the borrow checker is the last remnant of a larger formal proof and verification system, but I cannot find the source claiming this anymore. I'm also aware of several initiatives trying to bring formal verification to the rust language.

On my side the lack of formal verification feels like a big missed opportunity for Rust, as its success is a statement of the want and need of many engineers for approachable verification tools.

I currently use lean/rocq but it's a huge pain and I often have to make strong assumptions, creating a diverge between my formal specifications and the real code, rather than let the compiler enforce this for me.

Why do you think Rust lacks a formal verification system? Which approaches seem most promising at the moment? Do you have any sources to suggest for me to read on how to improve my proofs?