Outil de traduction automatique permettant de convertir des fichiers au format Rec vers le format Dedukti. Ce projet facilite l'interopérabilité entre différents systèmes de preuve formelle, notamment pour la vérification de théorèmes en logique mathématique. Il s'adresse principalement aux chercheurs et développeurs travaillant dans le domaine de la démonstration automatique et de la logique formelle.

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.

Le projet pvs-with-proofs est un outil permettant la vérification formelle de preuves mathématiques en utilisant le système de preuve PVS. Il s'intègre avec différentes bibliothèques déductives telles que Nasalib, Dedukti et MetiTarski, et permet d'exporter les preuves vers divers formats.

Eo2lp est un outil de traduction qui convertit les signatures et scripts de preuves du solveur cvc5 (Eunoia) vers le format LambdaPi, compatible avec l'écosystème Dedukti. Il permet de vérifier automatiquement des preuves générées par cvc5 dans un cadre formel dédié, assurant leur cohérence et leur réduction de type. Le projet cible un sous-ensemble spécifique de cvc5 et offre des fonctionnalités de benchmark pour évaluer la couverture et la fiabilité des traductions.