Putting it together





Determine which aspects of correctness apply at each stage of BGP's operation.
Express constraints.
Try to test constraints with static analysis.