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.

Construkti est un outil qui applique la traduction de Kuroda aux preuves écrites en Dedukti. Il transforme des preuves classiques en preuves intuitionnistes en ajoutant des doubles négations aux formules et quantificateurs universels. Cela permet de valider des théorèmes mathématiques tout en garantissant leur cohérence dans un cadre logique plus restrictif.

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.

COQQTL est un projet visant à porter l'intermédiaire de représentation FIRRTL pour les langages de description matérielle (HDL) dans l'assistant de preuve Coq. Il permet de vérifier formellement des circuits électroniques en utilisant des méthodes de preuve mathématique, garantissant ainsi leur correction et leur fiabilité. Le projet s'adresse principalement aux chercheurs et ingénieurs en électronique et en informatique qui souhaitent valider des architectures matérielles de manière rigoureuse.