Conclusion


BGP needs systematic verification techniques, regardless of configuration language.

Verification can inspire the design of new configuration languages.

Early version of the tool (RoLex) is available.
Several operators have downloaded the tool 
Talking with Cisco about incorporating configuration checking on the routers themselves.

http://nms.lcs.mit.edu/bgp/rolex