Dedukti est un vérificateur de types et un langage dédié à la formalisation et à la vérification de systèmes logiques et mathématiques. Il permet de définir des règles de réécriture et de vérifier leur cohérence, facilitant ainsi la construction de preuves formelles et la validation de propriétés dans des calculs avancés comme le lambda-calcul ou les systèmes de types dépendants.

Ce projet implémente l'algorithme de calcul des ordres d'appel pour Parcoursup, une plateforme d'admission dans l'enseignement supérieur en France. Il fournit une spécification formelle de l'algorithme et des preuves de sa correction en utilisant différents outils de vérification.

Ce projet propose un cadre automatisé pour la vérification formelle de circuits matériels complexes. Il permet de vérifier des propriétés temporelles et de prouver des lemmes sur des architectures électroniques, notamment via des techniques de model-checking symbolique et de preuve automatique. L'objectif est d'améliorer la fiabilité et la robustesse des systèmes embarqués en détectant des erreurs de conception avant leur déploiement.

Le projet atom-dedukti est un éditeur de texte pour Atom dédié à la manipulation et à la vérification de preuves formelles dans le contexte de la déduction. Il permet de gérer des goals et hypothèses, de les lier entre elles et de les visualiser clairement. Il offre également des fonctionnalités de navigation dans les fichiers de déduction à l'aide de raccourcis clavier.

Le projet Dedukti est une plateforme dédiée à un outil de vérification de preuves formelles. Il permet aux chercheurs et développeurs de partager des travaux, des ressources et des avancées dans le domaine de la logique et de la vérification automatique. Le site sert de vitrine pour promouvoir l'outil et faciliter l'accès à sa documentation.

Projet de recherche en informatique théorique axé sur la vérification formelle de preuves mathématiques et le développement de tactiques dépendantes dans le langage Meta Dedukti. Il permet d'assurer la correction et la fiabilité des démonstrations logiques et mathématiques à l'aide de méthodes formelles avancées.

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.

VsRocq est une extension pour Visual Studio Code et VSCodium qui fournit un support avancé pour le prouveur interactif Rocq (anciennement Coq). Il permet aux utilisateurs de vérifier des preuves mathématiques, de développer des logiciels certifiés et d'enseigner la logique formelle grâce à une intégration fluide avec l'éditeur. L'outil offre des fonctionnalités comme la vérification continue des preuves, une interface interactive pour explorer les objectifs de preuve et un panneau dédié aux requêtes.

Projet dédié à l'automatisation et à l'assistance de la vérification de preuves mathématiques formelles à l'aide d'agents IA. Il propose des outils pour écrire, vérifier et corriger des preuves dans le langage Lambdapi, ainsi qu'un environnement de benchmarking pour évaluer les performances des agents. Le projet explore également différentes approches d'interaction entre agents et outils de preuve.

Projet dédié à l'optimisation des transferts de fichiers et des tactiques de preuve pour Meta Dedukti, un outil de vérification formelle. Il facilite la manipulation et l'échange de preuves mathématiques formalisées en utilisant des méthodes efficaces et automatisées.