The mCRL2 toolset uses Tarjan’s strongly connected components algorithm at several places. To gain experience with automated provers, we have made a proof of this algorithm using Dafny, an automatic program verifier. In this talk I will explain our solution, and tell something about our experiences with Dafny.

This is joint work with Kees Huizing.