CompCert isn't about a safe C, it's a verified C compiler. This means it has proofs that verify that the compiler correctly implements the C standard and that t

CompCert isn't about a safe C, it's a verified C compiler. This means it has proofs that verify that the compiler correctly implements the C standard and that the binary code it produces is a faithful implementation of the original program as determined by C's semantics. This is used, for example, as part of the verification for the high-integrity, high-security seL4 microkernel.