No. I am saying you don't need rust for largely correct.

PS: The term you are looking for is formally verified not mathematically proven.

Oh and btw their borrow checker is the kind of system that you would want formally verified.