This project is the one requested for the MPRI course "Proof of programs" (MPRI 2.36.1). -- It contains an implementation, using Why3, of topological sorting. The task description can be found here (mirror).