Developing cutting-edge, resilient software is essential for maintaining a strong and capable U.S. military. However, the Department of Defense’s reliance on outdated IT systems and decades-old security policies leaves critical defense platforms exposed to cyber threats. Legacy systems and even modern weapon platforms are vulnerable, and adversaries are actively exploiting these weaknesses to target infrastructure, steal sensitive software, and undermine national security.
To counter this, DARPA is advancing the use of formal methods, a rigorous software development process that mathematically proves software security and correctness at the design stage. The U.S. Air Force is incorporating this methodology into its MQ-9 Reaper program.
A Shift in Software Assurance
Traditional methods rely heavily on static code analysis and lengthy testing cycles—sometimes up to 18 months—to uncover software vulnerabilities. Formal methods, in contrast, enable developers to verify software integrity as it’s being built, significantly reducing risk and testing time.
DARPA’s formal methods tools are designed to work with legacy code, allowing system developers to verify security and stability, generate certified models, and streamline the Authority to Operate (ATO) process.
The Capstone Initiative
Through its Resilient Software Systems Capstone program, DARPA is partnering with all U.S. military branches to drive adoption of formal methods across key platforms. The Capstone projects will run over 24 months and aim to:
Deliver more secure software
Accelerate ATO timelines
Improve testing efficiency
Develop best practices for scaling formal methods across the services
The Air Force selected the MQ-9 Reaper for the pilot effort due to its lower technical and cultural barriers to entry.
DARPA is also coordinating with the Navy, Army, and NASA on additional platform demonstrations under the Capstone initiative to enable faster, safer software updates for critical defense systems.
