Resolution and superpostion provers rely on the given clause procedure to saturate the clause set. Using Isabelle/HOL, we formally verify four variants of the procedure: the well-known Otter and DISCOUNT loops as well as the lesser-known iProver and Zipperposition loops. For each of the variants, we show that given a fair data structure to store the formulas that wait to be selected, the procedure guarantees saturation. Our formalization of the Zipperposition loop clarifies some fine points previously misunderstood in the literature.