The proof of the algorithm is available from the Git repository:
gitub.u-bordeaux.fr/parcoursup/why3.
The proof has been written in the language WhyML used by Why3 tool. language. The code is available in a pretty-printed form at the address: parcoursup.labri.fr/why3/calcul_ordre_appel.