Try SpecLens
Explore localized configuration explanations through our interactive user study tasks.
Why Trust SpecLens
SpecLens is supported by evidence from user studies and experiments on real-world and synthetic networks. These evaluations examine whether its explanations improve configuration reasoning, remain usable, and scale to large networks.
- User Study: 52% accuracy improvement and 23% time reduction.
- Usability: 62/100 average SUS; 70% would use SpecLens in daily practice.
- Scalability: A 1,280-router FatTree network analyzed in 25 minutes.
- Runtime: 10 minutes on Internet2 and 12–30 seconds on synthetic networks.
We evaluated SpecLens with 23 participants (15 professional network operators and 8 graduate students) on four configuration reasoning tasks.
User study task accuracy and completion time.
Participants completed the standard 10-item System Usability Scale questionnaire after the study tasks.
User-study System Usability Scale responses.
We assessed scalability by varying the number of routers, configuration lines, and threads.
Scalability of subspecification generation under different dimensions.
We benchmarked end-to-end subspecification generation on real and synthetic network configurations.
Run time of subspecification generation under different benchmarks.
Open Source
SpecLens is fully open source at github.com/declarative-systems-lab/batfish. The repository contains the implementation, configurations, and workflows needed to reproduce and extend our analyses.
- Batfish and Minesweeper extensions for simulation and verification encoding.
- The complete SpecLens subspecification analysis pipeline.
- User-study and benchmark network configurations.
- Reproducible end-to-end command-line workflows.
Research Extensions
Localized subspecifications provide a general explanation layer for network configuration analysis. Beyond explainable verification, we extend them to configuration repair and fault-tolerant reasoning.
- Explainable Network Verification via Localized Subspecification In Proceedings of ACM SIGCOMM 2026.
- Characterizing Network Configuration Repair Spaces with Localized Subspecifications In Proceedings of ACM APNet 2026. Best Paper Award.
- Explaining Network Configurations Under Failures via Localized Subspecifications In Proceedings of ACM FMANO 2026 (SIGCOMM Workshop).
Explainable Network Verification via Localized Subspecification
Introduces localized subspecifications as a sound explanation layer for verified network configurations: a scalable two-phase algorithm, a user study with network operators, and evaluation on Internet2 and large synthetic networks.
Characterizing Network Configuration Repair Spaces with Localized Subspecifications
Applies localized subspecifications to misconfigured networks by characterizing repair spaces at individual configuration locations, using a reference route propagation graph for modular computation instead of returning a single opaque patch.
Explaining Network Configurations Under Failures via Localized Subspecifications
Extends localized subspecifications to k-failure models. Fault-tolerant subspecifications aggregate branch-local constraints from failure-aware symbolic routes, explaining which fields are failure-critical across admissible failure scenarios.