Dedukti est un vérificateur de types et un langage dédié à la formalisation et à la vérification de systèmes logiques et mathématiques. Il permet de définir des règles de réécriture et de vérifier leur cohérence, facilitant ainsi la construction de preuves formelles et la validation de propriétés dans des calculs avancés comme le lambda-calcul ou les systèmes de types dépendants.

MCsimCoq est un outil de simulation de systèmes de mémoire informatique. Il permet d'analyser les performances de différents types de mémoire, tels que DDR3 et DDR4, en utilisant des modèles formels générés par Coq. Il vérifie également la conformité des commandes de mémoire avec les protocoles spécifiés.

VeriFast est un outil d'analyse statique formelle conçu pour vérifier la correction de programmes écrits en C et Java. Il permet de détecter des erreurs de typage, des violations de propriétés de sécurité et des bugs potentiels avant l'exécution. Utilisé principalement dans les domaines critiques comme les systèmes embarqués ou les applications sécurisées, il aide les développeurs à prouver que leur code respecte des spécifications formelles.

Sukerujo est un système de déduction pour le lambda-calcul et les démonstrations formelles. Il permet de vérifier des preuves, d'inférer des types pour des expressions lambda, et d'analyser les dépendances entre modules.

Ce projet propose une bibliothèque Rocq qui automatise la traduction des bibliothèques HOL-Light vers Rocq, permettant d'utiliser des théorèmes et fonctions mathématiques dans Rocq. Il facilite l'interopérabilité entre ces deux systèmes de preuve formelle en alignant types et fonctions, et offre un accès à plus de 20 000 théorèmes couvrant des domaines variés comme l'arithmétique, l'algèbre, l'analyse ou la topologie. Les preuves traduites sont fournies sous forme d'axiomes pour une utilisation rapide, avec la possibilité de régénérer et vérifier les preuves originales si nécessaire.

Projet de recherche en informatique théorique visant à simplifier et automatiser l'élimination de l'univalence dans les systèmes de types. Il permet de transformer des preuves complexes en calculs plus simples et plus efficaces, facilitant ainsi le développement de logiciels formellement vérifiés. Basé sur des concepts avancés de théorie des types, il s'adresse principalement aux chercheurs et développeurs en informatique fondamentale.