In recent years, computer scientists have become more and more convinced that verification is an important part of software development. We give an example for formal verification of "realistic" software: we show how to prove correctness of code generators that are developed within the compiler generating system CAT. Such code generators are large and involved programs specified in META IV. The proofs that are necessary become even larger and more involved, and to carry them out by hand seems to be an unfeasible task. Therefore automatic proof support is needed. We demonstrate that it is possible to give this support; we have written a proof support system which does essential parts of the proof. It is based on term rewriting and on specification by pre- and postconditions.