In general, there's no formal way to prove that two programs do the same thing

That is true, but in this particular case the OP would be generating the code himself and would not just be given two programs and asked if they are equivalent. Thus, he could just prove that he is converting all simple instructions properly, that the execution model is the same (eg. instructions are processed sequentially except in conditionals and loops and those are processed in equivalent ways) and the equivalence of the programs would follow.

The next best thing is to device as many test cases as feasible

This is a commendable suggestion at any rate.