There are formalization of C, e.g. compcert, which also compiles to machine code in a way that should guarantee proofs all the way though execution (assuming the machine modeling is correct).

It seems like it is a long way off from being possible to do that for rust.