A highly capable military requires advanced, resilient software to power the weapons and systems that U.S. warfighters rely on. However, the Department of Defense (DoD) continues to depend on outdated IT infrastructure and security policies developed over the past 30 years, creating systemic vulnerabilities across everything from legacy systems to modern weapons platforms.
Adversaries are actively exploiting these weaknesses—targeting critical systems, stealing sensitive software, and compromising national security through cyber intrusions.
To address this, DARPA is championing the use of formal methods, a mathematically rigorous approach that verifies software correctness during development, helping to eliminate vulnerabilities before deployment. The U.S. Air Force will apply this methodology to the MQ-9 Reaper program as part of its cyber resilience efforts.
Building Cyber-Resilient Software from the Ground Up
Unlike traditional processes that detect flaws after software is built, formal methods use mathematical proofs to ensure software behaves as intended from the start. DARPA’s tools built around this methodology are already transitioning to the services for operational use, but broader adoption is urgently needed to strengthen cyber resilience across the defense enterprise.
Resilient Software Systems Capstone Program
DARPA’s Capstone program is collaborating with all military branches to accelerate the adoption of formal methods on live platforms. Each 24-month project will assess key outcomes such as resiliency levels, development costs, required expertise, and testing efficiency.
Program goals include:
Developing inherently more secure software
Speeding up the Authority to Operate (ATO) process
Streamlining developmental testing
Publishing best practices to guide widespread implementation
The Air Force has selected the MQ-9 Reaper program, built by General Atomics-Aeronautical Systems Inc. (GA-ASI), as the initial Capstone project.
Currently, OEMs and Program Offices rely on static code analysis to detect manual errors during development. However, software changes on legacy platforms often result in extensive testing cycles, sometimes lasting up to 18 months.
Formal methods are showing potential to significantly reduce testing timelines by shifting verification activities earlier in the development process. DARPA’s tools can model software behavior directly from legacy code, assess system resilience, and produce certification artifacts such as airworthiness documentation and ATO approvals.
This new capability allows program teams to accelerate software updates while maintaining security and stability.
In addition to the MQ-9 Reaper, DARPA is working with the Navy, Army, and NASA on similar platform-based experiments under the Capstone framework.
