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.