I'm pretty sure that program equivalence is undecidable, ie you literally can't write this validation pass at all. There's a C compiler (compcert) that is forma

I'm pretty sure that program equivalence is undecidable, ie you literally can't write this validation pass at all. There's a C compiler (compcert) that is formally verified to preserve the semantic of its input C code down to assembly, but it takes a lot of human developed proofs in Coq to get there.