Formal proofs of safety

The rust community is a vocal one to say the least. The so-called "rust evangelists" have managed to pique the interest of even the strongest C/C++ knuckleheads ( like myself ).

I'm interested. I'm open to adopt rust. There's just one thing stopping me.

Are there any formal proofs that prove the validity of the borrow checker and the memory bugs it prevents?

Thank you.