Incremental Network Configuration Verification via Localized Subspecification

Verifying large network configurations can take hours or even days. Yet, network updates occur frequently as operational goals and conditions evolve. In this work, we study the problem of incremental network verification. Leveraging the observation that many updates are small, we propose a lightweight verification method based on localized subspecifications. Given an update location, we extract from the original verification conditions a subset of constraints that is both necessary and sufficient to preserve the global property. If the update satisfies the subspecification, correctness is guaranteed without re-running full verification. This approach offers a promising direction for reducing verification overhead and enabling timely feedback during network evolution.