We present a rigorous correctness proof, supported in temporal logic, for the distance vector with reset on failures protocol—an abstraction for a class of shortest-path routing protocols based on diffusing computations. This class includes the diffusing updates algorithm (DUAL), which is at the core of the Enhanced Interior Gateway Routing Protocol (EIGRP), widely used on the Internet. Our rigorous approach allows us to uncover counter-intuitive protocol behaviors which have not been reported previously. Finally, we show that the protocol exhibits exponential message complexity under asynchronous operation, and discuss its applicability beyond shortest-path routing, in particular using the composite bandwidth-delay metric of EIGRP.