A Coq formalization of the Stable Routing Problem and of effective abstractions as presented in the paper Control Plane Compression. Only the fact that choice-equivalence implies label and forwarding-equivalence has been proved. It remains to show that stable solutions of the concrete and abstract network are choice-equivalent.