Le projet cv2fstar-material est un dépôt de code source contenant une extension pour l'outil CryptoVerif, qui permet de vérifier la correction et la sécurité des protocoles cryptographiques. Cette extension, développée dans le cadre d'une thèse de doctorat, permet de générer automatiquement du code sécurisé à partir de spécifications formelles, améliorant ainsi l'efficacité et la fiabilité du processus de développement de protocoles cryptographiques.

OpenEmbedd est un projet dédié à la modélisation, la simulation et la génération de code pour les systèmes embarqués. Il permet de vérifier formellement des propriétés sur les modèles et facilite le développement de systèmes embarqués critiques.

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.