Pentagon eyes FLASH program to outsmart hackers

The Defense Advanced Research Projects Agency, the Pentagon’s research and development arm, is asking industry and researchers how to automatically generate many different versions of the same military system, each mathematically proven to do the same job but built differently enough that an attack or fault that breaks one would not carry over to the others. The request for information, issued on Nov. 3 by DARPA’s Information Processing Techniques Office, covers an effort called Formal Learning and Abstractions for System Heterogeneity, or FLASH, and responses are due by 5 p.m. Eastern on Nov. 30.

The notice, DARPA-SN-27-17, is market research rather than a solicitation, and DARPA has not announced a program, a budget or a schedule for any follow-on award. The agency says it will discard any abstract or proposal submitted against the request and will not pay for responses.

At the center of FLASH is the idea that diversity can be engineered as a defense. DARPA wants to separate a system’s high-level requirements from the details of any single design, then use that separation to produce multiple design instances that keep the same specified properties while differing in their failure modes and attack surfaces. If an adversary discovers a vulnerability, a configuration weakness or a common fault in one instance, the agency argues, that knowledge would be less durable and harder to transfer to the others.

The agency describes three technical thrusts. The first is formalizing a system’s requirements, operational intent and invariants, the properties that must never change, while exposing the design choices that are free to vary. The second is generating different design instances with guaranteed functional equivalence and formally provable correctness. The third is producing assurance and explanation material alongside each design, so that correctness, heterogeneity and resilience can be shown mathematically instead of being judged only by testing.

To do that, DARPA wants to combine generative-model-based software agents with symbolic reasoning, the rule-based logic used in formal verification, to capture design intent and synthesize what it calls semantically heterogeneous cyber-physical engineering systems. Cyber-physical systems are those in which software directly controls physical hardware, such as flight controls, weapons, vehicles or industrial equipment. The request names specific techniques it wants respondents to address, including oracle-guided inductive synthesis, in which a program is built from examples and repeatedly checked against a verifier, and the pairing of generative multimodal foundation models with interactive theorem provers, tools in which engineers and software construct machine-checked mathematical proofs.

DARPA lists autonomous tactical platforms, secure communication pipelines, industrial control systems, fleets of autonomous robots, high-performance computing clusters, edge computing networks and cybersecurity tools as examples of where the approach might apply. It asks respondents to define a target application and its threat environment, explain where current hardening methods fall short, and identify which functional, safety, security, timing, interoperability and performance properties must stay fixed across every generated version.

The second set of questions covers how such a system would be built and measured. DARPA asks for metrics for heterogeneity, methods to validate functional equivalence and experiments that test resilience against adaptive adversaries, including what it calls autonomous exploit development using intelligent agents. It also asks about single-agent and multi-agent architectures for system design and about reusable libraries of formal specifications, models and proofs for particular applications.

In 1977, Liming Chen and Algirdas Avizienis proposed N-version programming, in which independent teams write separate programs from the same specification and a voter compares their outputs, on the assumption that separately developed software would fail separately. In 1986, John Knight and Nancy Leveson tested that assumption with 27 versions of the same program written independently at two universities and run through one million test cases, and found that the versions failed together far more often than independence would predict. The Knight and Leveson study concluded that analysis of multiversion software must account for dependent errors, and the result has shaped skepticism about design diversity since.

FLASH differs from N-version programming in where it seeks its guarantees. Instead of relying on independent human teams and statistical independence, DARPA wants a common formal specification, automatically generated variants and machine-checked proofs that each variant satisfies the same properties. The request does not say how the agency expects to measure whether generated variants are diverse enough to avoid the correlated failures the 1986 experiment found, which is why it asks respondents to propose heterogeneity metrics.

The request also builds on DARPA’s own formal methods work. In the High-Assurance Cyber Military Systems program, which ended in 2017, a red team at first took remote control of a quadcopter and of Boeing’s Unmanned Little Bird helicopter, but after engineers rebuilt key software using formal methods, the same team failed to break in during six weeks with full access to the system, including a test with two pilots aboard in flight. DARPA later applied the program’s tools to satellites and self-driving convoy trucks, and in 2025 it began working with the U.S. Air Force to bring formal methods tools to the MQ-9 Reaper through its Resilient Software Systems Capstone program.

FLASH is one of the first focused efforts to emerge from the Information Processing Techniques Office since DARPA revived that name in May 2026. The office, formerly the Information Innovation Office, took back the title of the original IPTO, which funded the ARPANET and early interactive computing under J.C.R. Licklider in the 1960s before merging into the Information Innovation Office in 2010. Director Patrick Lincoln has said the renamed office would focus on the resilience and understanding of complex systems, alongside cybersecurity and privacy.