The paper sketches a design process that starts with a mathematical solution of the enumeration problem presented and proved correct in [Maz97] and ends up with a distributed, efficient, and successfully terminating protocol in the specification language Estelle. The subsequent versions of the protocol are obtained from their predecessors by well controlled and small modifications that (almost) obviously preserve correctness. Hence, the correctness of the final version is assured by virtue of the original proof which could have remained relatively simple and elegant exactly because was not involved in realization details. The target, successful (successful with arbitrarily high probability) solution allows forgetting theoretical "impossibility results", which prove non-existence of such successful distributed solutions for some classes of networks that abstractly are characterized by, so called, "ambiguous" graphs.
Keywords: Distributed algorithms, Formal Specification, Verification, FDT Estelle.