This paper presents the development and formal verification of CompCert, a compiler that translates Clight (a subset of C) to PowerPC assembly code. The verification process uses the Coq proof assistant to ensure semantic preservation, meaning that the compiled code behaves as prescribed by the semantics of the source program. The paper discusses the challenges and approaches to establishing trust in the compilation process, including verified compilers, translation validation with verified validators, and proof-carrying code. It provides an overview of the CompCert compiler, its structure, and the formal verification of its back-end, focusing on the register allocation pass. The paper also highlights the performance of CompCert compared to GCC and outlines future work, including extending the compiler to handle a larger subset of C and targeting other processors.This paper presents the development and formal verification of CompCert, a compiler that translates Clight (a subset of C) to PowerPC assembly code. The verification process uses the Coq proof assistant to ensure semantic preservation, meaning that the compiled code behaves as prescribed by the semantics of the source program. The paper discusses the challenges and approaches to establishing trust in the compilation process, including verified compilers, translation validation with verified validators, and proof-carrying code. It provides an overview of the CompCert compiler, its structure, and the formal verification of its back-end, focusing on the register allocation pass. The paper also highlights the performance of CompCert compared to GCC and outlines future work, including extending the compiler to handle a larger subset of C and targeting other processors.