CompCert：经形式化验证的 C 编译器
使用 Coq 证明助手形式化验证的 C 编译器，生成代码的行为被保证与源程序语义一致。
CompCert 是面向核心 C 语言的编译器，可为 ARM、PowerPC、RISC-V 和 x86 处理器生成代码。其核心特性是使用 Coq 证明助手进行了形式化验证：生成的汇编代码在形式上被保证与源 C 代码的语义规定行为一致。支持的平台、C 特性、安装与使用方法见其网站和用户手册。许可证方面，本仓库的非商业版本并非自由软件，仅可用于评估、研究、教育和个人用途；商业版本需向 AbsInt 购买。版权归属 INRIA 与 AbsInt Angewandte Informatik GmbH，用户讨论通过 compcert-users@inria.fr 邮件列表进行。