Explainable Network Verification via Localized Subspecification

Abstract

Network verification, synthesis, and repair tools help enforce high-level operational intent, but their limited explainability makes configuration maintenance costly in practice, as operators must still manually reason about large, low-level configurations. We propose localized subspecifications, which explain how individual configuration elements preserve a given network property by constraining their admissible behaviors. A user study with 15 professional network operators and 8 graduate students shows 52% higher accuracy and 23% time savings, and 70% of participants reported that they would like to use subspecifications in daily operations, demonstrating practical benefits. To support real deployments, we develop SpecLens, an explainable network verification system that generates localized subspecifications using a scalable algorithm with soundness guarantees. SpecLens computes line-level and field-level subspecifications in 10 minutes on the real-world Internet2 configuration and 25 minutes on FatTree networks with up to 1,280 routers.