Ce projet rassemble les vérifications de faits et les met à disposition via un flux RSS. Les métadonnées associées aux vérifications de faits et aux affirmations qu'elles investiguent doivent être au format JSON-LD et suivre les schémas ClaimReview et MediaReview, couramment utilisés par les vérificateurs de faits. Les métadonnées enrichies à partir des plateformes de médias sociaux nécessitent l'invention de certaines nouvelles propriétés et types ClaimReview, dont le schéma est documenté sur le référentiel GitHub AFP-Medialab.

Verde est un plugin GDB écrit en Python qui vise à aider les développeurs lors des sessions de débogage interactif en utilisant la vérification d'exécution. Il permet de détecter les violations de propriétés et de déclencher des actions spécifiques lorsque cela se produit, comme donner accès au développeur au prompt du débogueur.

Le projet Residual Runtime Verification with BISM est une implémentation en tant que plugin pour l'outil d'instrumentation Java BISM. Il permet la vérification de propriétés à l'exécution en instrumentant le code pour capturer des événements de programme spécifiques et détecter les exécutions non conformes.

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.

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.

Ce projet implémente un algorithme de vérification de modèles basé sur la construction parallèle d'un graphe d'observation symbolique (SOG) pour la vérification de propriétés temporelles linéaires (LTL) sur des systèmes parallèles, améliorant ainsi les performances et la scalabilité de la vérification de modèles.

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.