Tarjan’s algorithm for strongly connected components is used in the mCRL2 toolset. This algorithm finds all strongly connected components or SCC in a directed graph. Here an SCC is a maximal set of nodes such that there exists a directed path between all nodes in the set. The normal implementation of Tarjan’s algorithm uses recursion. Unfortunately, this implementation can cause stack overflow problems if the graphs are sufficiently large. The mCRL2 toolset uses an iterative implementation of Tarjan’s algorithm to circumvent this problem. In this project both the recursive and the much more complex iterative algorithm have been proven correct using the verification language Dafny. For the recursive algorithm a previous proof was already available. However this proof was nearing the limits of Dafny’s capabilities, which caused unstable results after minor changes. As part of this work techniques have been introduced to guarantee much more stable proofs.