We show how to use an interactive theorem prover, HOL, together with a model checker,
SPIN, to prove key properties of distance vector routing protocols. We do three case studies:
correctness of the RIP standard, a sharp real-time bound on RIP stability, and preservation
of loop-freedom in AODV, a distance vector protocol for wireless networks. We develop
verification techniques suited to routing protocols generally. These case studies show
significant benefits from automated support in reduced verification workload and assistance …

Formal verification of standards for distance vector routing protocols | CiNii Research …
Formal verification of standards for distance vector routing protocols …