formalize tarjan's algorithm in why3 formalize kosaraju's algorithm in why3 formalize kosaraju's algorithm in lean4 related work https://github.com/coq-community/tarjan