This paper describes how program-checking can be used to
  significantly reduce the amount of verification work to establish
  the implementation correctness of software systems which may be
  partly generated by unverified construction tools. We show the
  practicability of our approach with an application to the
  construction of verified compiler back-ends.  The basic idea of
  program-checking is to use an unverified algorithm whose results are
  checked by a verified component at run time. Run-Time Result
  Verification in our approach assures formal correctness of the
  software system and its implementation if partial correctness of the
  application is sufficient. In our example the approach does not only
  simplify the construction of verified compilers because checking the
  result of the transformations is much simpler to verify than the
  verification of an optimizing code selection. Furthermore, we are
  still able to use existing compiler generator tools without
  modifications.  Compiler verification plays two roles in this paper:
  First it closes the gap between verification on high-level
  programming language and the implementation on machine level using a
  verified compiler to translate the verified program to machine code.
  Second it serves as a large-scale case study for software
  verification. This work points out the tasks which still have to be
  verified and it discusses the flexibility of the
  approach.