Just like humans program; you write code and have unit tests (if you are lucky). What is different about this? It has the same inputs / outputs so the unit tests will be there. Formal verification would be better; aka having a model for the original and having the computer prove that new version is mathematically identical to the original. But both the formal verification and the transformation proof are far off for almost all software projects in practice.