Holide est un traducteur de fichiers de théories formelles de HOL vers Dedukti. Il permet de vérifier la validité des théories formelles dans le langage Dedukti.

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.

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.