FastVacc: A Formal Layer for Requirement Checking — Response to DARPA-SN-27-13
Response to DARPA Special Notice DARPA-SN-27-13, Verification and Compliance Checking for Natural-Language Network Requirements (FastVacc). This working paper proposes an intermediate formal layer (a domain-specific language whose abstractions follow the structure of the requirements documents themselves) between natural-language security requirements and concrete network configurations. The core claim is that the absence of such a checkable layer is the common cause of the three challenges named in the RFI. The response addresses all seven RFI questions. It defines contradiction, redundancy, incompleteness, and extension admissibility over requirement sets; proposes design principles for the DSL; outlines metrics and go/no-go gates; and situates the approach relative to existing network verifiers (Batfish, Timepiece, Kirigami, NetKAT) and recent intent-driven systems (TopoIntent, Game of Zones). Primary scope is segmentation and reachability requirements drawn from Commercial Solutions for Classified (CSfC) capability packages, with Zero Trust Architecture and Secure Controls as secondary design-intent targets. The evaluation protocol and most quantitative claims remain untested hypotheses. This is an independent technical response submitted by AionSystem. It is UNCLASSIFIED.
Authors
- Sheldon K Salmon (Mr. AI/ON) (ORCID: https://orcid.org/0009-0005-8057-5115)
Publication Details
- Journal
- Zenodo (CERN European Organization for Nuclear Research)
- Published
- 2026-11-11
- DOI
- https://doi.org/10.5281/zenodo.24140208
- Primary Topic
- Formal Methods in Verification
- Type
- preprint