DARPA Resilient Software Work on MQ-9 Needs Scope Discipline

DARPA’s resilient software work on MQ-9 operational code is interesting because it tests formal methods against a real legacy platform.

The Resilient Software Systems Capstone applies formal methods tools to operational software over roughly two years. DARPA’s Resilient Software Systems Capstone materials frame the work around cyber resilience, integration effort, and adoption evidence. The hard question is not whether formal methods work. They do. The hard question is where they work on an operational codebase without a ground-up redesign.

DARPA’s own HACMS program is the precedent. The HACMS case study says the team rewrote about 80,000 of 100,000 lines with formal methods and partitioned mission-control software. That success was not “verify the legacy stack.” It was closer to “rebuild the trusted core.”

That distinction matters for MQ-9. A large operational platform has history. It has legacy code, interfaces, safety constraints, airworthiness evidence, operational procedures, vendor boundaries, and fielded behavior that people already rely on. Formal methods cannot make all of that simple by declaration.

The credible path is targeted. Choose the boundaries where failure matters most. Prove input validation where untrusted data enters. Prove state machines where mode confusion can create unsafe behavior. Prove fault logic where a bad transition can cascade. Use partitioning to narrow the trusted base. Then connect the proof artifacts to the evidence the program actually needs.

The less credible path is broad promise. “Mathematically prove the MQ-9 software estate correct” sounds strong, but it ignores cost, scope, and the mixed assurance level of the surrounding system. It also ignores the human parts of the platform: procedures, maintenance, training, and operational decisions.

The integration cost also has to be measured honestly. A verified component still has to connect to unverified code, operating systems, networks, and sensors. The proof may be sound, but the boundary can leak assumptions. That is why the architecture around the proof matters as much as the proof itself.

Program offices should treat that boundary as a deliverable. It needs interface definitions, threat assumptions, test cases, and sustainment guidance. Without those artifacts, the verified work can be impressive and still hard for the platform owner to use.

Formal methods earn their value when they are applied with architectural discipline. They are not a spell cast over old code. They are a way to make selected properties precise and checkable. The engineering work is deciding which properties matter, where the code must be changed, and how the result will be integrated.

The evidence path is just as important. If the Capstone can generate artifacts that support ATO decisions, airworthiness review, and future sustainment, it will have value beyond a demonstration. If the evidence cannot be used by program offices, test teams, and authorizing officials, the proof remains a research result.

Polyrhythm’s view: formal methods earn their value through scoping discipline and architectural partitioning, not through proving every legacy layer at once. DARPA resilient software work on MQ-9 is worth watching because it puts that claim against an operational system, where proof has to survive contact with integration.