The United States Air Force will incorporate formal methods-based tools on the MQ-9 Reaper via DARPA’s Resilient Software Systems Capstone program
Jun 17, 2025
A strong, lethal military demands cutting-edge and resilient software to power every weapon and support system our U.S. warfighters depend on. However, the Department of Defense’s (DOD) reliance on aging IT infrastructure, using security policies developed over the last 30 years, creates inherent vulnerabilities in its systems, from legacy architectures to advanced weapons.
Meanwhile, threat actors are actively exploiting these vulnerabilities, targeting critical infrastructure, stealing sensitive military code, and reengineering sensitive systems to compromise national security.
In response, DARPA has been developing powerful tools leveraging formal methods—a mathematically rigorous approach to software development that helps eliminate exploitable vulnerabilities before software is deployed. Working closely with DARPA, the U.S. Air Force will incorporate this rigorous approach into its MQ-9 Reaper program.
Formal Methods: A secure foundation for the future
Rather than testing software for vulnerabilities after it’s built, formal methods use mathematical proofs to verify software behavior as it’s developed. This approach ensures software performs exactly as intended, making it inherently more secure.
Many of DARPA’s formal methods tools have already transitioned to military services for further development and operational deployment. Strong overall cyber resilience requires urgent, broader adoption.
Resilient Software Systems Capstone program
The agency is partnering with each of the services via its Resilient Software Systems Capstone program to address this pressing need. The Capstone program comprises jointly funded projects on operational platforms aimed at assessing critical findings, including level of resiliency, cost, time, and level of expertise required to adopt various formal methods capabilities.
Each project will run for approximately 24 months. Objectives include:
- Achieving inherently more secure software;
- Accelerating the Authority to Operate (ATO) process;
- Streamlining software developmental testing; and
- Developing a “Best Practices Guide” to support broad adoption.
“The current patch-and-pray approach to software development for DOD systems is simply unacceptable when lives depend on those systems,” said Stephen Kuhn, DARPA Capstone program manager. “DARPA’s transition approach through the Capstone brings resilient software tools to both the services and industry partners and will allow us to capture the lessons learned to drive broad adoption of correct by construction. This effort will serve as a template that can be used by others to help jumpstart their efforts to incorporate DARPA’s resilient software tools into their platforms and development pipelines.”
The U.S. Air Force is the first organization to identify their pilot weapon system – the MQ-9 Reaper program, developed by General Atomics-Aeronautical Systems Incorporated (GA-ASI).
Traditionally, when developing resilient cyber-physical systems, original equipment manufacturers (OEMs), such as GA-ASI, and Program Offices design to standardized industry controls. They use static code analysis tools to identify manual coding errors that may lead to issues in software stability and/or potential cyber vulnerabilities.
The challenge is that the span and complexity of software changes on legacy weapon systems often result in vast amounts of developmental and cyber testing, which can last 12-18 months in a typical software upgrade program.
Formal methods have shown promise in combating these lengthy test and evaluation cycles. DARPA’s suite of software assurance/cyber resiliency tools have demonstrated the ability to conduct more verification activities upstream into the development environment, as opposed to the typical test stages when the software is already finalized. Designed for use on existing legacy source code, these tools can generate validated models of software behaviors directly from that code, dynamically assess those behaviors for resiliency/stability/safety, and can even generate specific artifacts used for certification purposes such as ATOs and airworthiness.
Simply put, Program Offices and OEMs now have software acceleration tools to use on existing code, that complement policy improvements such as the Software Acquisition Pathway.
Air Force selects MQ-9 as capstone
The Air Force team working with DARPA on the Capstone chose the MQ-9 due to the lower technical barriers-to-entry of the weapon system itself, as well as the lower cultural barriers-to-entry within the organizational enterprise.
“The MQ-9 Capstone program will improve DARPA program support by providing a step-increase in our ability to accelerate robust and resilient weapon system software to the field,” said Oren Edwards, Chief Engineer of the Air Force Life Cycle Management Center’s Medium Altitude UAS Division.
“One of the cultural barriers-to-entry of digital transformation is the misperception that massive investments in time and money are required to show any transition wins on a program, a misperception we commonly associate with the ‘valley of death’” he said. “Investments are, in fact, required, but there’s an entire cottage industry of government and commercial tools that continuously show that misperception to be false, and that’s what we’re doing here. Using DARPA’s assurance acceleration tools to move certain verification activities upstream in the software development cycle will improve agility not only for the MQ-9 but will also present significant leverage opportunities for follow-on programs across the USAF and DOD.”
DARPA is also working with the Departments of the Navy and Army, and the National Aeronautics and Space Administration (NASA) on additional Capstone program platform experiments.
To learn more about formal methods and related DARPA programs, visit https://www.darpa.mil/formal-methods.
###
Media with inquiries should contact DARPA Public Affairs.