CompCert C 是一款用于 C 编程语言的编译器，旨在编译高度安全可靠的关键任务软件。它支持大部分 ISO C 99 语言，并生成 PowerPC、ARM、RISC-V 和 x86 架构的机器代码。CompCert C 的独特之处在于其经过机器辅助数学证明的形式化验证，确保编译过程的正确性，生成的可执行代码与源代码语义完全一致。