Zenon Modulo est un solveur de preuves automatisé pour la logique du premier ordre classique avec types polymorphes. Il accepte les fichiers d'entrée avec la syntaxe TPTP (FOF et TFF1) et Dedukti. Il peut produire des certificats de preuve pour Dedukti. Il est utilisé dans les projets FoCaLiZe et BWare.

CoqInE est un plugin pour le logiciel Coq qui traduit les preuves Coq en termes Dedukti vérifiables. Il fournit un fichier de signature fidèlement encodant la théorie sous-jacente de Coq. La sortie générée est destinée à être vérifiable à l'aide de la dernière version de Dedukti.

Ce programme vérifie la terminaison d'autres programmes en utilisant le critère de terminaison Size-Change. Il accepte en entrée des fichiers Dedukti ou des fichiers XML de la Termination Problem Data Base.

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.

Ekstrakto est un outil permettant de traduire des preuves au format TSTP en preuves lambdapi. Il génère des fichiers TPTP pour chaque étape de la preuve TSTP, ainsi qu'un fichier de signature lambdapi et un fichier de preuve lambdapi complet. Il peut ensuite être utilisé avec des preuves automatisées pour générer des fichiers de preuve lambdapi pour chaque étape.

STTfaXport est un outil permettant d'exporter des théories écrites dans le langage de déduction Dedukti vers d'autres assistants de preuve en utilisant l'encodage de STTfa. Il nécessite OCaml, Dedukti et dune pour fonctionner.