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.

Outil dédié à l'analyse et à l'optimisation de modèles de compteurs abstraits utilisés en vérification formelle. Il permet de déterminer des tailles de ensembles concrets à partir de modèles pseudo-booléens, facilitant ainsi la validation de propriétés logiques complexes. Développé dans le cadre du projet BLaSST, il s'intègre dans des workflows de preuve automatisée pour les systèmes critiques.

Projet open source dédié à la simulation et à la validation d'un processeur RISC-V pipeliné avec gestion des interruptions et exceptions. Basé sur une réimplémentation partielle du processeur Kôika, il permet de tester des programmes personnalisés cycle par cycle, d'effectuer des preuves formelles et de synthétiser des designs pour FPGA. Utilisé pour l'enseignement, la recherche et le prototypage matériel.

Ce projet développe des preuves formelles en Coq pour valider des modèles de mémoires tampons (store buffers) parallèles. Il explore des configurations avec verrous fins ou complets et démontre leur monotonie ou leurs contre-exemples. Les travaux servent de base théorique pour l'analyse de systèmes concurrents et la correction de protocoles de cohérence mémoire.

Cadre de travail Coq dédié à la conception et à la vérification formelle de contrôleurs de mémoire DRAM. Permet aux chercheurs et ingénieurs de modéliser des architectures mémoire complexes et de valider leur comportement à l'aide de preuves formelles. Utilisé dans le cadre de travaux académiques ou industriels pour garantir la fiabilité des systèmes mémoire.

Outil dédié à la résolution de problèmes de satisfaction de contraintes (CSP) et à la validation de propriétés logiques sur des modèles formels. Il permet d'analyser des systèmes critiques en vérifiant leur cohérence et en générant des contre-exemples ou des preuves de validité. Développé dans le cadre d'un projet de recherche financé par l'ANR, il s'appuie sur des techniques avancées de logique et de satisfiabilité.

Outil en ligne de commande conçu pour prouver des obligations de preuve au format POG en utilisant la plateforme Why3. Il permet de transformer des fichiers de preuve en formats compatibles avec divers prouveurs automatiques (Zenon, SMT-LIB, TPTP, etc.) pour valider des théorèmes mathématiques ou des propriétés logiques. Idéal pour les chercheurs et développeurs en vérification formelle ou en logique mathématique.

COQQTL est un projet visant à porter l'intermédiaire de représentation FIRRTL pour les langages de description matérielle (HDL) dans l'assistant de preuve Coq. Il permet de vérifier formellement des circuits électroniques en utilisant des méthodes de preuve mathématique, garantissant ainsi leur correction et leur fiabilité. Le projet s'adresse principalement aux chercheurs et ingénieurs en électronique et en informatique qui souhaitent valider des architectures matérielles de manière rigoureuse.

Projet open source permettant de transformer du code écrit en WhyML, un langage de spécification et de preuve, en code Java exécutable. Il facilite la vérification formelle de propriétés logiques sur des algorithmes tout en produisant un code source compatible avec l'écosystème Java. Utilisé principalement dans le domaine de la recherche académique et de la validation de programmes.