In this paper, we consider specific dataflow solvers, inspired by the work of Bourdoncle [5], in which an iteration order is pre-computed, based on the structure of the control-flow graph of programs. Our work aims at a clearer formulation and a better understanding of the folklore algorithms proposed three decades ago. We present a formalization of the dataflow solvers. Central to the proof of correctness is the general notion of a Weak Topological Ordering (WTO). Our correctness proofs are valid for any such ordering. The first solver implements an iterative strategy over the ordering, the second solver implements a recursive strategy. Our formalization is done within the Coq proof assistant and our solvers are extractable to OCaml code. Our formalization is fully compatible with the interface of dataflow solvers of the verified, optimizing C CompCert compiler. We conduct practical experiments on the wide range of forward and backward analyses of CompCert, demonstrating the practicality of our solvers in terms of efficiency and precision.