In this talk, we present a proof of correctness for an algorithm computing strongly connected components in a directed graph by Tarjan [1972]. It will be the starting point of a discussion about the readability of formal proofs. This proof was achieved with the Why3 system and the Coq/ssreflect proof assistant. The same proof was redone fully in Coq/ssreflect and Isabelle/HOL.

This is joint work with Ran Chen and was presented at VSTTE 2017. The Coq and Isabelle proofs were achieved by Cyril Cohen, Laurent Théry and Stephan Merz.