Explore a groundbreaking system for automatically synthesizing formal network specifications in this 21-minute conference talk from NSDI '20. Dive into Config2Spec, a tool that mines network policies from existing configurations and failure models, addressing the challenge of efficient policy space exploration. Learn how the system combines data plane analysis and control plane verification to scale to large networks with up to 150 routers. Discover the technical challenges involved in specification synthesis, including dense and sparse violations, conflict resolution, and candidate space management. Gain insights into the performance and environmental selection aspects of this innovative approach to network verification and configuration synthesis.