CompCert — проект по созданию официально верифицированных компиляторов. В рамках проекта разработан компилятор CompCert C для языка Си (стандартов ISO C90 / ANSI C с некоторыми незначительными ограничениями и отдельными расширениями, вдохновлённые последующими стандартами), а также полностью написана и продемонстрирована система верификации Coq. Основной разработчик — Ксавье Леруа. У этого компилятора есть машинная проверка того, что сгенерированный код ведёт себя так же, как и исходный код. Компилятор позволяет генерировать машинный код для архитектур процессора PowerPC, ARM и x86.

Код, сгенерированный CompCert, примерно вдвое быстрее, чем сгенерированный GCC без оптимизации и немного медленнее, чем сгенерированный с более высокими уровнями оптимизации^[3]

• Формальная верификация
• Формальные методы

• http://compcert.inria.fr/
• https://www.absint.com/compcert/