ONHS Report: DARPA-SN-27-13

Request for Information (RFI): Verification and Compliance Checking for Natural-Language Network Requirements (FastVacc)

Solicitation ID: DARPA-SN-27-13

Agency: DARPA/IPTO

Type: Special Notice

Deadline: 2026-11-13T17:00:00 ET

Eligibility: Yes (Unrestricted)

Funding: N/A

Doc Type: RFI

Clearance: No

Program Manager: FastVacc@darpa.mil

Last Updated: 2026-10-30 16:03

Analyzed File: DARPA-SN-27-13.pdf

Eligibility Reasoning

Responses are welcome from all capable sources including, but not limited to, private or public companies, individuals, universities, university-affiliated research centers, not-for-profit research institutions, and U.S. Government-sponsored labs.

Note: This is an AI-generated summary...

Summary

The Defense Advanced Research Projects Agency (DARPA) Information Processing Techniques Office (IPTO) has issued a Request for Information (RFI) for the Verification and Compliance Checking for Natural-Language Network Requirements (FastVacc) program. The program seeks to dramatically reduce the time and cost (by 2-3 orders of magnitude) of verifying that network configurations comply with security requirements written in natural language. DARPA envisions a capability that accepts two inputs: a natural language requirements document and a concrete network configuration. The system would first perform an offline analysis of the requirements to identify and resolve inconsistencies, redundancies, and incompleteness. It would then perform a near real-time check to verify if the network's configuration satisfies the refined requirements. The RFI identifies three core challenges: Natural Language Understanding, Reasoning (about abstract requirements), and Evaluation (against concrete configurations). DARPA is requesting information on potential approaches, including the adequacy of Large Language Models (LLMs), the need for an intermediate formal system or Domain-Specific Language (DSL), metrics for success, and existing relevant technologies. (Source: DARPA-SN-27-13.pdf.)

Overall Technical Areas

Natural Language UnderstandingNetwork Formal VerificationAutomated Reasoning SystemsSecurity Compliance CheckingNetwork Configuration AnalysisLarge Language Model ApplicationsDomain-Specific Language (DSL) DesignFormal SemanticsDeductive SystemsSymbolic EvaluationAbstract InterpretationRequirements Consistency AnalysisInductive ReasoningFormalized Proof Libraries

Probable LBNL Areas

BSACSAEESAESAETA

Focus Areas

Example Priorities:

Requirements cannot be understood in isolation. Often, they are defined in terms of document-specific, mission-specific abstractions that can only be understood in the context of the full document.
Document-specific abstractions need to be identified in configurations. Network configurations are not labeled with these abstractions.
The instantiated requirements need to be further translated into scripts for running network tests and the query language of network verification tools.
A baseline solution is to upload a requirement document and a concrete configuration into a large language model and ask it to perform the above tasks.

Specific Technical Skills:

Natural Language ProcessingLarge Language Models (LLMs)Semantic ParsingKnowledge ExtractionOntology EngineeringDomain-Specific Language (DSL) DesignContextual UnderstandingNetwork Configuration Analysis

Potential PIs for this Area:

Name	Score	Organization
Eric Chagnon	0.76	CSA \| AMCR \| Mathematics · Large Language Models (LLMs)
Rafael Zamora-Resendiz	0.74	CSA \| AMCR \| Computer Science · Natural Language Processing
Matthew Henderson	0.74	CSA \| SciData \| Data Science Applications · Contextual Understanding
Arpit Gupta	0.73	CSA \| ESNET \| Tech Adv and Engagement · Network Configuration Analysis
Chris Mungall	0.72	BSA \| Env. Genomics & Sys. Biology \| BioSystems Data Science · Ontology Engineering
Dale Carder	0.72	CSA \| ESNET \| Networking Services · Network Configuration Analysis
Katherine Rasmussen	0.72	CSA \| AMCR \| Computer Science · Domain-Specific Language (DSL) Design
Kevin Cruse	0.72	ESA \| MSD \| Material Physics · Knowledge Extraction
Gazi Mahmud	0.72	BSA \| Env. Genomics & Sys. Biology \| Molecular Ecosystems Bio · Ontology Engineering
Harry Caufield	0.72	BSA \| Env. Genomics & Sys. Biology \| BioSystems Data Science · Knowledge Extraction

Example Priorities:

Reasoning requirements mean evaluating e.g., if requirements are contradictory, redundant or incomplete.
The hardness is compounded by the fact that reasoning has to be carried out in the abstract without reference to a concrete structure or configuration.
When such features are added, analysts must infer the original security intent and formulate additional requirements needed to preserve it in the modified architecture.
Network verification tools... are designed for analysis of a specific, fully-specified network configuration, not for reasoning about the requirements themselves.

Specific Technical Skills:

Formal MethodsAutomated ReasoningTheorem ProvingModel CheckingSymbolic LogicDeductive SystemsRequirements EngineeringConstraint SolvingInductive Reasoning

Potential PIs for this Area:

Name	Score	Organization
Koushik Sen	0.72	CSA \| AMCR \| Computer Science · Formal Methods
Gregory Lemieux	0.71	EESA \| CESD \| Earth System Sciences · Requirements Engineering
Steven Hofmeyr	0.71	CSA \| AMCR \| Computer Science · Deductive Systems
Eric Chagnon	0.71	CSA \| AMCR \| Mathematics · Automated Reasoning
Michael Mahoney	0.70	CSA \| SciData \| Data Science Research · Inductive Reasoning
Xiaoye Sherry Li	0.70	CSA \| AMCR \| Applied Mathematics · Constraint Solving
Abdelilah Essiari	0.70	CSA \| SciData \| Data Science Applications · Deductive Systems
Zachary Needell	0.69	ETA \| Energy Analysis \| Systems & Energy Tech Analysis · Requirements Engineering
Angelos Ioannou	0.69	CSA \| AMCR \| Computer Science · Model Checking
Talita Perciano Costa Leite	0.69	CSA \| SciData \| Data & Computational Science · Inductive Reasoning

Example Priorities:

Then, it would check, in near real-time, whether the concrete configurations satisfy all of the requirements.
Often, requirements are tested, not formally verified.
Manually checking all such instances against configuration is slow, labor-intensive and error prone.
Existing network verification tools can overcome this limitation by symbolically evaluating all requirement instances.

Specific Technical Skills:

Network VerificationFormal VerificationSymbolic EvaluationReal-Time SystemsNetwork Security AuditingConfiguration ManagementAutomated Compliance CheckingScalable Systems Design

Potential PIs for this Area:

Name	Score	Organization
Cees De Laat	0.76	CSA \| ESNET \| Tech Adv and Engagement · Scalable Systems Design
Scott Beamer	0.76	CSA \| AMCR \| Computer Science · Scalable Systems Design
Koushik Sen	0.74	CSA \| AMCR \| Computer Science · Automated Compliance Checking
Adam Slagell	0.73	CSA \| ESNET \| Security · Network Security Auditing
Arpit Gupta	0.72	CSA \| ESNET \| Tech Adv and Engagement · Network Verification
Gregory Lemieux	0.72	EESA \| CESD \| Earth System Sciences · Configuration Management
Angelos Ioannou	0.72	CSA \| AMCR \| Computer Science · Real-Time Systems
Alexandre Bayen	0.71	ETA \| Energy Analysis \| Systems & Energy Tech Analysis · Network Verification
Vern Paxson	0.71	CSA \| SciData \| Data Science Applications · Network Security Auditing
Katherine Rasmussen	0.71	CSA \| AMCR \| Computer Science · Symbolic Evaluation

Potential LBNL PIs (Overall)

Note on PI Matching: These suggestions are generated through an AI-driven semantic analysis of LBNL staff profiles.

Name	Score	Organization
Eric Chagnon	0.77	CSA \| AMCR \| Mathematics · Large Language Model Applications
Matthew Henderson	0.73	CSA \| SciData \| Data Science Applications · Natural Language Understanding
Koushik Sen	0.73	CSA \| AMCR \| Computer Science · Symbolic Evaluation
Arpit Gupta	0.73	CSA \| ESNET \| Tech Adv and Engagement · Network Configuration Analysis
Dale Carder	0.72	CSA \| ESNET \| Networking Services · Network Configuration Analysis
Katherine Rasmussen	0.72	CSA \| AMCR \| Computer Science · Domain-Specific Language (DSL) Design
Alexandre Bayen	0.72	ETA \| Energy Analysis \| Systems & Energy Tech Analysis · Network Formal Verification
Adam Slagell	0.71	CSA \| ESNET \| Security · Security Compliance Checking
Gregory Lemieux	0.71	EESA \| CESD \| Earth System Sciences · Requirements Consistency Analysis
Rafael Zamora-Resendiz	0.71	CSA \| AMCR \| Computer Science · Natural Language Understanding

Fundamental Research Exemption (FRE)

Not Mentioned