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.

Network synthesis simplifies network management by automatically generating distributed configurations that fulfill high-level intents. However, typical network synthesizers operate as monolithic algorithms, obscuring the internal workings of the synthesis process and showing no clear connection between the generated configurations and the global intents. Given the critical role of networks as infrastructure, it is crucial for network operators to understand the synthesized configurations to establish trust in these automatic tools. To address this challenge, we propose using subspecifications localized to each component in the network topology to enhance the interpretability of network synthesis. These subspecifications provide insights into the workings of synthesizers by connecting each component's functionalities with the global configuration intents.

The hope of allowing programmers to more freely express themselves has led to a proliferation of program synthesis techniques. These tools automatically derive implementations from high-level specifications of user intent. These specifications may take the form of logical formulas, demonstrations, or input-output examples. Synthesizers guarantee that when synthesis is successful, the implementation satisfies the specification. However, they provide no additional information regarding how the implementation works or the manner in which the specification is realized. As a result, they remain algorithmic black boxes which are prone to producing unidiomatic code with procedurally generated identifier names, like $x 1, x 2$, etc. As a result, complicated implementations produced by modern program synthesizers are becoming increasingly hard to understand. One solution to this comprehensibility problem is to produce meaningful identifier names for its variables, functions, etc. While large language models (LLMs) suggest a simple way to obtain human-readable names, our experiments reveal that LLMs frequently produce nonsensical or misleading names when applied to code emitted by program synthesizers. In this paper, we develop an approach to reliably augment the implementation with explanatory names: We recover finegrained input-output data from the synthesis algorithm to enhance the prompt supplied to the LLM and use a combination of a program verifier and a second language model to validate the proposed names before presenting them to the user. Together, these techniques improve the accuracy of the proposed names from $\mathbf{2 4 \%}$ to $\mathbf{7 9 \%}$. A two-phase user study indicates that users significantly prefer the names produced by our technique, and that the proposed names greatly help users in understanding synthesized implementations.

The traditional formulation of the program synthesis problem is to find a program that meets a logical correctness specification. When synthesis is successful, there is a guarantee that the implementation satisfies the specification. Unfortunately, synthesis engines are typically monolithic algorithms, and obscure the correspondence between the specification, implementation and user intent. In contrast, humans often include comments in their code to guide future developers towards the purpose and design of different parts of the codebase. In this paper, we introduce subspecifications as a mechanism to augment the synthesized implementation with explanatory notes of this form. In this model, the user may ask for explanations of different parts of the implementation; the subspecification generated in response is a logical formula that describes the constraints induced on that subexpression by the global specification and surrounding implementation. We develop algorithms to construct and verify subspecifications and investigate their theoretical properties. We perform an experimental evaluation of the subspecification generation procedure, and measure its effectiveness and running time. Finally, we conduct a user study to determine whether subspecifications are useful: we find that subspecifications greatly aid in understanding the global specification, in identifying alternative implementations, and in debugging faulty implementations.