Source: wikibot/compcert
= CompCert
{wiki=CompCert}
CompCert is a formally verified compiler for the C programming language, designed to ensure that the compiled code behaves according to the semantics of the source code. It aims to provide a high assurance of correctness, which is particularly important in critical systems where reliability is paramount (such as in aerospace, automotive, and medical applications).