The Border Gateway Protocol (BGP), the inter-domain routing protocol for the Internet, allows for a wide variety of routing policies that may interact in unintended and unstable ways. Recent work on BGP and related protocols has begun to incorporate formal protocol models, which have enabled rigorous descriptive analyses of BGP. More recently, such models have been used to give prescriptive guidelines for the design of new protocols. These guidelines include both sufficient conditions for good routing behavior and limitations on what can be achieved without coordination between routers. Here we review potential routing problems, formal models that describe routing at different levels of abstraction, and the design guidelines that they have been used to prove. There are additional complications when policy interactions within an autonomous domain are considered; we discuss ongoing work to address these concerns as well as future directions for our work.