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.