Uclid-RV est un projet visant à fournir des outils pour la vérification formelle de propriétés logicielles. Il permet d'analyser et de vérifier des preuves formelles, contribuant ainsi à garantir la correction des logiciels.

TTool est un ensemble d'outils dédié à la création et à la vérification de diagrammes UML et SysML. Il permet de simuler et de vérifier la sécurité, la performance et d'autres propriétés formelles de ces diagrammes.

Bibliothèque de support pour l'assistant de preuve Coq, fournissant des fichiers vernaculaires pour l'importation des certificats générés par Gappa et un tactic `gappa` pour appeler Gappa sur le but courant dans Coq. Gappa est un outil destiné à aider à la vérification et à la preuve formelle de propriétés sur des programmes numériques utilisant des calculs arithmétiques en virgule flottante ou à point fixe.

Gappa est un outil conçu pour aider à la vérification et à la preuve formelle de propriétés sur des programmes numériques traitant des calculs en virgule flottante ou à point fixe.

ParTraP est un interpréteur pour le langage ParTraP, proposé dans le projet MODMED, qui vérifie que les traces d'exécution satisfont des propriétés formelles données dans un langage de haut niveau.

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.

Outil d'analyse et de traduction de contrats intelligents Ethereum vers des réseaux de Petri colorés (CPNs). Il permet de vérifier des propriétés formelles sur ces contrats à l'aide de la logique temporelle linéaire (LTL).

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.

Ce projet concerne la transformation de modèles et l'analyse de code réactif, en vérifiant des propriétés spécifiques grâce à la sémantique formelle de Haskell.