In reply to Alex Horn.

Hello Alex, and thanks for your note.
Cisco's Network Assurance Engine is indeed based on formal verification techniques against the user-intended graph of connectivity and policy, as declared via an SDN controller.
Doing justice to your question at the level of depth of a technical paper would be a good thing for us to do. I'll prod us into working on that. :)

Thanks again for your interest!
Roland