ONHS Report: DARPA-SN-27-17

Request for Information (RFI): Formal Learning and Abstractions for System Heterogeneity (FLASH)

Solicitation ID: DARPA-SN-27-17

Agency: DARPA/IPTO

Type: Special Notice

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

Eligibility: Yes (Unrestricted)

Funding: N/A

Doc Type: RFI

Clearance: TS/SCI

Program Manager: FLASH@darpa.mil

Last Updated: 2026-11-04 17:03

Analyzed File: DARPA-SN-27-17.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 laboratories.

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 Formal Learning and Abstractions for System Heterogeneity (FLASH) program. The RFI seeks to gather information on novel methodologies that use generative models and symbolic reasoning to automatically synthesize and understand high-assurance, heterogeneous cyber-physical systems from formal specifications. The central goal is to enhance system robustness by generating diverse instances that share core functionality but possess different failure modes and attack surfaces, thereby mitigating the transferability of adversary knowledge. DARPA is requesting information in two primary areas: (1) national security applications (e.g., autonomous platforms, secure communications, industrial control systems) that could benefit from this dynamic heterogeneity, and (2) potential technical frameworks, synthesis techniques, and evaluation criteria to achieve the FLASH vision of provably correct, varied system generation. (Source: DARPA-SN-27-17.pdf.)

Overall Technical Areas

Formal MethodsSystem HeterogeneityAutomated System SynthesisHigh-Assurance Cyber-Physical SystemsGenerative AI ModelsSymbolic ReasoningFormal Specification & VerificationProvable System CorrectnessAutomated Assurance GenerationFormal Knowledge RepresentationInductive SynthesisInteractive Theorem ProvingMulti-Agent System ArchitecturesAdversarial AI Resilience

Probable LBNL Areas

BSACSAEESAESAETAPSA

Focus Areas

Example Priorities:

formalizing system requirements, operational intent, and semantic invariants
exposing valid design degrees of freedom that allow for heterogeneous alternative choices
systematically decoupling high-level system requirements from instance-level design details
the functional, safety, security, timing, interoperability, and performance properties that must remain invariant across generated alternatives

Specific Technical Skills:

Formal MethodsSpecification LanguagesSystems EngineeringRequirements EngineeringSemantic ModelingCyber-Physical SystemsInvariant AnalysisDesign Space Exploration

Potential PIs for this Area:

Name	Score	Organization
Eric Masanet	0.75	ETA \| Energy Analysis \| Systems & Energy Tech Analysis · Systems Engineering
Christian Schmid	0.75	ETA \| Building & Industrial Energy Systems \| Bldg Technologies Dept · Semantic Modeling
Alexandre Bayen	0.75	ETA \| Energy Analysis \| Systems & Energy Tech Analysis · Cyber-Physical Systems
Luisa Caldas	0.74	ETA \| Building & Industrial Energy Systems \| Bldg Technologies Dept · Design Space Exploration
Daniel Arnold	0.74	ETA \| Energy Technologies and Systems \| Energy Storage & Dist Dpt · Cyber-Physical Systems
Scott Beamer	0.73	CSA \| AMCR \| Computer Science · Design Space Exploration
Gregory Lemieux	0.73	EESA \| CESD \| Earth System Sciences · Requirements Engineering
Koushik Sen	0.72	CSA \| AMCR \| Computer Science · Formal Methods
Katherine Rasmussen	0.72	CSA \| AMCR \| Computer Science · Specification Languages
Gunther Weber	0.72	CSA \| SciData \| Data Science Applications · Invariant Analysis

Example Priorities:

augment generative-model-based agents with symbolic reasoning techniques to formally represent design intent
developing models and techniques to generate different system design instances while guaranteeing functional equivalence and formally provable correctness
structurally constrained induction and deduction approaches such as oracle-guided inductive synthesis
combining generative multimodal foundation models with interactive theorem provers for design
single-agent and multi-agent architectures suitable for system design and understanding

Specific Technical Skills:

Generative ModelsSymbolic ReasoningProgram SynthesisAutomated ReasoningInductive SynthesisInteractive Theorem ProvingFormal VerificationFoundation ModelsMulti-Agent Systems

Potential PIs for this Area:

Name	Score	Organization
Zixi Hu	0.73	CSA \| AMCR \| Mathematics · Generative Models
Koushik Sen	0.73	CSA \| AMCR \| Computer Science · Symbolic Reasoning
Eric Chagnon	0.72	CSA \| AMCR \| Mathematics · Foundation Models
Sascha Diefenbacher	0.72	PSA \| PHY \| Theory Group · Generative Models
Alexandre Bayen	0.72	ETA \| Energy Analysis \| Systems & Energy Tech Analysis · Multi-Agent Systems
Matthew Henderson	0.71	CSA \| SciData \| Data Science Applications · Foundation Models
Katherine Rasmussen	0.70	CSA \| AMCR \| Computer Science · Program Synthesis
Angelos Ioannou	0.70	CSA \| AMCR \| Computer Science · Formal Verification
Gregory Lemieux	0.70	EESA \| CESD \| Earth System Sciences · Interactive Theorem Proving
Kevin Cruse	0.69	ESA \| MSD \| Material Physics · Inductive Synthesis

Example Priorities:

techniques to co-generate assurance and explanation artifacts that are applicable across design instances
Co-generation of design collateral for assurance and understanding helps provide evidence that correctness, heterogeneity, and resilience can be formally assessed
generate reusable formalizations of domain-specific engineering knowledge
reusable libraries of formalized specifications, models, and proofs for specific application areas

Specific Technical Skills:

Assurance Case EngineeringExplainable AI (XAI)Automated Documentation GenerationKnowledge RepresentationModel-Based Systems Engineering (MBSE)Software AssuranceFormal VerificationDomain-Specific Languages

Potential PIs for this Area:

Name	Score	Organization
Koushik Sen	0.75	CSA \| AMCR \| Computer Science · Software Assurance
Katherine Rasmussen	0.73	CSA \| AMCR \| Computer Science · Domain-Specific Languages
Gregory Lemieux	0.72	EESA \| CESD \| Earth System Sciences · Model-Based Systems Engineering (MBSE)
Zachary Needell	0.72	ETA \| Energy Analysis \| Systems & Energy Tech Analysis · Model-Based Systems Engineering (MBSE)
Chris Mungall	0.71	BSA \| Env. Genomics & Sys. Biology \| BioSystems Data Science · Knowledge Representation
Gazi Mahmud	0.70	BSA \| Env. Genomics & Sys. Biology \| Molecular Ecosystems Bio · Knowledge Representation
Anna Giannakou	0.70	CSA \| SciData \| Data Science Applications · Explainable AI (XAI)
Eric Chagnon	0.70	CSA \| AMCR \| Mathematics · Automated Documentation Generation
Angelos Ioannou	0.70	CSA \| AMCR \| Computer Science · Formal Verification
Talita Perciano Costa Leite	0.70	CSA \| SciData \| Data & Computational Science · Explainable AI (XAI)

Example Priorities:

metrics for heterogeneity; methods to validate functional equivalence and other invariant system properties
experiments assessing resilience against adaptive, including autonomous exploit development using intelligent agents
how dynamic heterogeneity and FLASH technical thrusts could mitigate vulnerabilities, common-mode failures, or attack pathways
Exploitation of such variation could reduce the durability and transferability of instance-specific adversary knowledge

Specific Technical Skills:

System EvaluationMetrics DevelopmentResilience EngineeringCybersecurity TestingAutonomous Exploit GenerationAttack Surface AnalysisVulnerability AssessmentFormal Assessment

Potential PIs for this Area:

Name	Score	Organization
Koushik Sen	0.75	CSA \| AMCR \| Computer Science · Cybersecurity Testing
Tiffany Connors	0.74	CSA \| NERSC \| Data Center Department · Attack Surface Analysis
Jeetika Malik	0.73	ETA \| Building & Industrial Energy Systems \| Bldg Technologies Dept · Resilience Engineering
Sunhee Baik	0.73	ETA \| Energy Analysis \| Energy Markets & Planning · Vulnerability Assessment
Sarah Poon	0.72	CSA \| SciData \| Data Science Applications · System Evaluation
Jingjing Zhang	0.72	ETA \| Building & Industrial Energy Systems \| Whole Building Sys Dept · System Evaluation
Alexandre Bayen	0.72	ETA \| Energy Analysis \| Systems & Energy Tech Analysis · Attack Surface Analysis
Gregory Lemieux	0.71	EESA \| CESD \| Earth System Sciences · Metrics Development
Hannah Cohoon	0.71	CSA \| SciData \| Data Science Applications · Metrics Development
Katherine Rasmussen	0.71	CSA \| AMCR \| Computer Science · Formal Assessment

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
Anastasiia Butko	0.74	CSA \| AMCR \| Computer Science · System Heterogeneity
Daniel Arnold	0.73	ETA \| Energy Technologies and Systems \| Energy Storage & Dist Dpt · Adversarial AI Resilience
Koushik Sen	0.73	CSA \| AMCR \| Computer Science · Automated Assurance Generation
Alexandre Bayen	0.73	ETA \| Energy Analysis \| Systems & Energy Tech Analysis · High-Assurance Cyber-Physical Systems
Angelos Ioannou	0.72	CSA \| AMCR \| Computer Science · Automated System Synthesis
Eric Chagnon	0.72	CSA \| AMCR \| Mathematics · Generative AI Models
Steven Hofmeyr	0.72	CSA \| AMCR \| Computer Science · Formal Knowledge Representation
Gregory Lemieux	0.71	EESA \| CESD \| Earth System Sciences · Formal Specification & Verification
Houjun Tang	0.71	CSA \| SciData \| Data Science Applications · Multi-Agent System Architectures
Xiaoye Sherry Li	0.71	CSA \| AMCR \| Applied Mathematics · Symbolic Reasoning

Fundamental Research Exemption (FRE)

Not Mentioned