The value of the proof comes from the things it enables. I guess the Rust memory safety guarantees are based on some proofs?
It's possible to write incorrect code and compile it with a correct compiler, so I don't think so. It's more like a citation that proven correct programs can use to say "I wrote this program correctly (see my own proof), and I compiled it correctly (see citation), thus I have a correct executable file".
> I guess the Rust memory safety guarantees are based on some proofs?
People have retroactively come up with formal proofs for much of it, but I believe the initial design was just based on intuition not a proof. For unsafe code some of the exact details of the memory model are still being worked out too (and thus definitely aren't proven correct).