CompCert is a C compiler. It is developed and formally verified in the Coq proof assistant.
The CompCert project is headed by Xavier Leroy.
The CompCert project originally targeted a fairly large subset of C - called Clight - which it compiled to PowerPC assembly code [Leroy 2009].
It has since been extended to cover almost all of ISO C 2011, generating code for ARM, PowerPC, RISC-V, and x86.
For the development of CompCert, seven researchers received the 2021 ACM Software System Award.
YouTube video for the 2021 ACM Software System Award.
A 2009 report on the CompCert project is given in the CACM article
Xavier Leroy. 2009. Formal verification of a realistic compiler. Communications of the ACM 52, 7 (July 2009), 107–115. https://doi.org/10.1145/1538788.1538814 [pdf]
@article{10.1145/1538788.1538814,
author = {Leroy, Xavier},
title = {Formal Verification of a Realistic Compiler},
year = {2009},
issue_date = {July 2009},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {52},
number = {7},
issn = {0001-0782},
url = {https://doi.org/10.1145/1538788.1538814},
doi = {10.1145/1538788.1538814},
journal = {Commununications of the ACM},
month = {jul},
pages = {107–115},
numpages = {9}
}