What goes into proving two complicated programs are equivalent?
Formal analysis today is usually done on module or unit level. Unfortunately I'm not aware of a common metric which allows to predict if a formal analysis will be possible. Only structurally very simple codes can be formally analysed even with LOC's or cyclomatic complexities of up to a million. 

In your case here the code of any of the two programs is clearly too complex for a full formal analysis: 


Model-checking will not work.
A complete (bi-) simulation will not work either.


So the best practical solution I know is model-based testing. While it is not a proof still formal methods can be used. It ultimately eliminates the disaster of writing and maintaining manually written test cases. 




P.S.:

A short list of steps which can be done in this case:


An abstract model of the two programs is created. This is a third implementation which will omit all unimportant details. The abstraction has the advantage that this model is simple enough again to be formally analysed. The model can be implemented in any language you like if the model analyser will analyse the byte code.
The abstract model can be traversed and e.g. a condition coverage is reached in a test suite. This step is done using a model-based-testing tool.
Finally these test cases are tested on the two programs and it is checked if the abstract model can simulate the two program implementations. 
This simulation relation is of course not a proof of the equivalence.
The abstraction is a very clean specification what was taken into account in our tests and what was omitted. 
Two model-based testing tools which can be recommended: Microsoft Spec Explorer, Conformiq Designer