I don't have any, I haven't thought about it enough. However, the reason I think it might be interesting is that checking if something is a correct solution is often easier than coming up with a correct solution for a lot of classes of problems (assuming P!=NP and all that).

And maybe you can't make a polynomial time verifier which works in the general case, but maybe you can make a useful one which handles a lot of cases.

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.