This paper outlines the rigorous formal construction of a compiler program 
in a unified framework. Starting from a correct compiling specification
specifying a relation between source and target language programs, 
the methodology of stepwise refinement is utilized to formally derive 
a compiler program. 

The PVS system is used as a vehicle to carry out the formal mechanized
derivation process. The development steps involved include both
functional refinement as well as data and operation refinement.  The
considered compiler is part of an initial fully correct compiler from
ComLisp, a subset of CommonLisp, into binary transputer code.  The
construction of an initial correct compiler is an ongoing effort of
the Verifix project.