Le projet Capla Compiler est une version modifiée du compilateur CompCert, un compilateur C formellement vérifié. Il permet de transformer du code source C en code assembleur pour différentes architectures matérielles (ARM, PowerPC, RISC-V, x86) tout en garantissant la conformité du code généré par rapport au code source. Ce projet est utilisé dans des contextes où la fiabilité et la sécurité des programmes compilés sont critiques, notamment dans les domaines de la recherche, de l'éducation et de l'industrie.

Chamois est un fork du compilateur C formellement vérifié CompCert, avec des ajouts de Verimag et Kalray. Il s'agit d'un compilateur pour un sous-ensemble important du langage C, générant du code pour les processeurs PowerPC, ARM, x86, RISC-V et KVX. La particularité de CompCert est qu'il a été prouvé correct à l'aide de l'assistant de preuve Coq : le code assembleur généré est garanti de se comporter comme prescrit par la sémantique du code C source.

CompCert est un compilateur pour un large sous-ensemble du langage C qui génère du code pour plusieurs architectures de processeurs. Il est unique car il a été formellement vérifié à l'aide de l'assistant de preuve Coq, garantissant ainsi le comportement du code assembleur généré par rapport aux semantiques du code source C.

Dx est un outil permettant de dériver automatiquement du code C à partir de code Gallina monadique, proche du code C final. Il facilite la conversion de définitions formelles en code exécutable en générant une représentation intermédiaire puis un module C compilable. Principalement utilisé dans le domaine de la vérification formelle et des compilateurs, il s'intègre avec des outils comme CompCert pour produire du code C optimisé et vérifié.