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.

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.

Uclid-RV est un projet visant à fournir des outils pour la vérification formelle de propriétés logicielles. Il permet d'analyser et de vérifier des preuves formelles, contribuant ainsi à garantir la correction des logiciels.

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.

Agda2Dedukti est un traducteur permettant de convertir des preuves formelles écrites dans le langage Agda vers les langages Dedukti et Lambdapi, facilitant ainsi la vérification de ces preuves.

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.

Coq est un assistant de preuve interactif qui permet la vérification formelle de preuves mathématiques et la spécification et vérification de systèmes informatiques. Il utilise un langage de programmation dédié, le Gallina, pour écrire des preuves et des spécifications.

Bibliothèque de support pour l'assistant de preuve Coq, fournissant des fichiers vernaculaires pour l'importation des certificats générés par Gappa et un tactic `gappa` pour appeler Gappa sur le but courant dans Coq. Gappa est un outil destiné à aider à la vérification et à la preuve formelle de propriétés sur des programmes numériques utilisant des calculs arithmétiques en virgule flottante ou à point fixe.

HOL Light est un environnement interactif de démonstration et vérification de théorèmes mathématiques. Écrit en Objective CAML, il utilise le toplevel d'OCaml comme interface. Il est principalement utilisé pour la vérification formelle de preuves dans les domaines de la logique, de l'informatique théorique et des mathématiques.

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.