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.

Ce projet propose une bibliothèque Rocq (anciennement Coq) qui traduit automatiquement la bibliothèque HOL-Light dédiée à la logique. Il permet de manipuler des types et fonctions idiomatiques en Rocq tout en conservant les propriétés et théorèmes originaux. L'objectif est de faciliter l'interopérabilité entre ces deux environnements de preuve formelle pour des applications en vérification mathématique et en intelligence artificielle.

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.

Spécification formelle pour la modélisation et la vérification de workflows sécurisés. Ce projet permet de définir des propriétés de sécurité à l'aide de la logique temporelle linéaire (LTL) et de les valider sur des modèles de tâches et de flux de données. Il s'appuie sur des outils de model checking pour garantir le bon fonctionnement et la sécurité des processus modélisés.

Outil d'analyse et de vérification formelle de programmes pour détecter des erreurs logiques, optimiser des blocs de code et valider des propriétés de sécurité. Utilisé principalement dans la recherche académique et l'ingénierie logicielle pour améliorer la fiabilité des systèmes critiques.

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.

VeriFast est un outil d'analyse statique conçu pour vérifier la sécurité et la correction des programmes. Il permet de détecter des vulnérabilités potentielles dans le code source, notamment en Java, en s'appuyant sur des annotations et des propriétés formelles. L'outil est utilisé pour garantir la robustesse des systèmes critiques, comme les cartes à puce ou les applications embarquées, en identifiant les erreurs de logique ou les failles de sécurité avant leur déploiement.

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é.

Ce projet vise à fournir une preuve formelle de la sécurité des systèmes informatiques en utilisant la logique de séparation avec crédits de temps. Il permet de vérifier des propriétés temporelles dans des programmes concurrents et de développer des spécifications formelles pour des systèmes temps-réel.