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.

Predicativize is a tool used to translate proofs from an impredicative type system to a predicative one. It was used to translate Matita's arithmetic library to Agda, and can be used with Dedukti to translate other libraries as well.

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.

HOL Light est un assistant de preuve interactif écrit en Objective CAML, permettant la vérification formelle de preuves mathématiques et le développement de théories mathématiques formelles.

Verine is a project that automates logical reasoning and simplifies complex decision-making processes. It is designed to process and analyze large amounts of data and provide accurate and reliable results.

GeoCoqInE-Euclid est un projet de démonstration de théorèmes géométriques automatisée, utilisant le langage de programmation fonctionnelle Coq et la bibliothèque Euclid. Il permet le développement et la vérification de preuves formelles, ainsi que le travail collaboratif sur des théories mathématiques.

GeoCoqInE-Tarski est un projet de démonstration et de vérification automatique de théorèmes géométriques. Il s'appuie sur le système de déduction Dedukti et le logiciel de preuve Coq. Il permet de formaliser des preuves géométriques et de les vérifier automatiquement, ce qui facilite la certification des résultats et la détection d'erreurs.