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 th

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.