DARPA and U.S. Air Force launch cyber resilience upgrade for MQ-9 Reaper

Formal methods apply mathematical proofs during software development to ensure systems behave exactly as intended, reducing the risk of exploitable vulnerabilities. Unlike traditional approaches, which often identify flaws post-development, formal methods offer security from the outset.

DARPA’s Capstone programme includes jointly funded projects with military services, aiming to assess resilience, cost, timelines, and expertise needed to adopt formal methods. Each project, including the MQ-9 initiative, will run for approximately 24 months.

“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 programme 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.”

Traditionally, software development for defence systems relies on standardised industry controls and static code analysis to detect errors. However, these methods often result in prolonged test cycles of 12 to 18 months, especially on legacy platforms.

DARPA’s tools can analyse legacy code directly, generate validated behavioural models, and produce certification artefacts such as Authority to Operate (ATO) documentation. These tools shift verification earlier into the development process, increasing efficiency and stability.

The Air Force selected the MQ-9 Reaper due to its relatively low technical and cultural barriers for integrating new methodologies. The drone, developed by General Atomics-Aeronautical Systems Incorporated, serves as a pilot system for demonstrating the potential of formal methods.

“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. “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.”

Edwards also noted that perceptions of high transition costs are misplaced. “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,” he added.

Beyond the Air Force, DARPA is also collaborating with the Navy, Army, and NASA on similar Capstone platform experiments. The goal is to build a secure, adaptable software foundation for critical defence and aerospace systems.