Parcoursup est la plateforme nationale de préinscription en première année de l'enseignement supérieur en France. Ce document présente une partie des travaux de sûreté logicielle autour d'un des algorithmes de cette plateforme, appelé "calcul des ordres d'appel" : spécification de l'algorithme, vérification à l'exécution de la spécification, et preuve formelle de correction de l'algorithme. Ces travaux ont été réalisés à l'aide des outils de preuve Why3 et COQ et de techniques de vérification à l'exécution du code Java. Cela permet d'atteindre un très haut niveau de confiance dans l'algorithme de calcul des ordre d'appel de Parcoursup.