Timbuk est un cadre de vérification régulier basé sur les Automates d'Arbres et les Systèmes de Réécriture de Termes. Il fournit un ensemble de bibliothèques pour créer et manipuler des Automates d'Arbres et des TRS, effectuer une analyse de faisabilité à l'aide de l'Algorithme de Complétion, et calculer des abstractions capables de vérifier des propriétés de sécurité sur des programmes fonctionnels de haut niveau.

PMC-SOG est un outil de vérification de modèles parallèles utilisant des graphes d'observabilité symbolique. Il permet de vérifier des propriétés temporelles sur des systèmes concurrents et distribués, de construire des graphes d'observabilité symbolique et d'analyser les performances de ces systèmes.

Catala est un langage de programmation dédié à la rédaction et à l'analyse de textes législatifs. Il permet de définir des règles complexes de manière claire et précise, et de générer automatiquement du code à partir de ces règles. Catala vise à améliorer la fiabilité et la transparence des systèmes législatifs en automatisant certaines tâches de vérification et de mise en œuvre.

AlphaZ est un outil de modélisation et d'analyse de systèmes, permettant la manipulation de systèmes affines et la génération de code à partir de modèles. Il offre des fonctionnalités avancées d'analyse et de vérification de systèmes, et s'appuie sur des technologies telles qu'Xtext pour la génération de code.

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.

Ce projet fournit une implémentation de l'outil Imitator, permettant l'analyse de performances et la vérification de propriétés temporelles de systèmes asynchrones, ainsi que la synthèse de stratégies pour des systèmes paramétrés.

Rdbg est un débogueur programmable ciblant les programmes réactifs pour lesquels un plugin rdbg existe. Il permet l'analyse du comportement de systèmes synchrones et la vérification de la correctitude de programmes concurrents.

Un plugin de surveillance Nagios/Icinga pour monitorer systemd. Il permet de vérifier l'état des unités systemd, de détecter les unités défaillantes et d'analyser les temps de démarrage des services systemd.

Prototype Python utilisant le solveur Z3 SMT pour encoder et analyser les mesures socio-fiscales françaises. Il permet de répondre à des questions sur le système socio-fiscal sous la forme d'une recherche dichotomique pour maximiser ou minimiser une valeur donnée, en fonction de divers paramètres tels que les revenus, les allocations familiales, les aides au logement, etc.

BuDDy est une bibliothèque C++ de deuxième génération dédiée aux Diagrammes de Décision Binaire (BDD). Développée initialement par Jorn Lind-Nielsen, elle permet de simplifier et d'optimiser des circuits logiques, d'analyser et de vérifier des systèmes numériques, ainsi que de réduire la complexité algorithmique.