CoqTL est un langage de programmation interne (DSL) pour la transformation de modèles dans l'environnement de preuve formelle Coq. Il permet de spécifier des transformations de modèles de manière déclarative et de générer des preuves pour ces transformations. Ce dépôt contient des exemples et des preuves pour CoqTL, ainsi que des générateurs pour créer des métamodèles et des modèles à partir de fichiers Ecore et XMI.

Bibliothèque de support pour l'assistant de preuve Coq, fournissant des fichiers vernaculaires pour l'importation des certificats générés par Gappa et un tactic `gappa` pour appeler Gappa sur le but courant dans Coq. Gappa est un outil destiné à aider à la vérification et à la preuve formelle de propriétés sur des programmes numériques utilisant des calculs arithmétiques en virgule flottante ou à point fixe.

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.