In January of this year, four U.S. government agencies - the Cybersecurity and Infrastructure Security Agency (CISA), the Defense Advanced Research Projects Agency (DARPA), the Office of the Under Secretary of Defense for Research and Engineering (OUSD R&E), and the National Security Agency (NSA) - jointly issued a call to action. Their message was unambiguous: the U.S. government must take decisive and coordinated action to close what they refer to as the “software understanding gap.” Their full report outlines both the urgency of this challenge and a strategic path forward https://media.defense.gov/2025/Jan/16/2003629074/-1/-1/1/Joint-Guide-Closing-the-Software-Understanding-Gap.PDF

The concept of software understanding extends well beyond code readability or basic maintainability. It refers to the ability to construct, analyze, and assure software-controlled systems so their functionality, safety, and security are comprehensively verified, not only in normal operating conditions but also in abnormal and hostile scenarios.

The software understanding gap arises when the ability to reason about and analyze software falls behind the pace of software production. For decades, investment in the tooling, methodologies, and education necessary to understand software has lagged behind the push to develop and deploy ever-more complex and feature-rich systems. As a result, mission owners and system operators are frequently left without the insight needed to assess or manage the behavior of the software they rely on, particularly in environments where failure or compromise has critical consequences.

This disparity has tangible, real-world consequences. It impairs our collective ability to:

• Develop software that is free of latent defects,
  

• Efficiently identify and remediate vulnerabilities,
  

• Maintain software systems with agility and confidence, and
  

• Secure them against a rapidly evolving landscape of cyber threats.
  
  

The stakes are high. The impact of the software understanding gap is visible in incidents of national significance, including:

• The 2021 Colonial Pipeline ransomware attack, which disrupted fuel distribution across the U.S. East Coast,
  

• The SolarWinds Orion supply chain compromise, which enabled widespread infiltration of government and private-sector networks and
  

• There are ongoing cyber campaigns, such as Volt Typhoon and Salt Typhoon, which have targeted critical infrastructure and telecommunications systems.
  
  

Because so much existing software is so difficult to understand, it's extremely difficult to add security after the fact. To address these challenges, the authoring agencies advocate a shift in how software is conceived and built, placing security at the heart of the design process rather than bolting it on after the fact.

What Does It Mean to Be Secure by Design?

A Secure by Design approach means treating security not as a peripheral concern but as a core engineering and business requirement. From the earliest phases of development, products should be architected to prevent entire classes of vulnerabilities, reduce attack surfaces, and facilitate meaningful assurance. The following points are salient:

• Ensure that security considerations inform every design decision. This reduces the need to identify and remediate vulnerabilities after deployment, which is dangerous, costly, and time-consuming.

• Eliminate insecure defaults and latent defects. Insecure defaults refer to pre-configured settings or behaviors that are not secure out of the box. If not changed or hardened, they can expose systems to risk. Latent defects are flaws present in the system that go undetected during development or testing. They may remain dormant for long periods and only surface under specific, often rare, conditions. These defects can lead to threats such as information leakage and may be exploited by attackers before developers are even aware of them.

• Embed security features. Due to the rapidly evolving landscape of cyber threats, it is important to include built-in security mechanisms, such as static and dynamic validation of input data and checks for out-of-bounds accesses, to ensure systems fail securely.

Crucially, Secure by Design also implies a shift in accountability. The burden of security should not fall solely on end-users or system integrators. Software manufacturers must take proactive responsibility for delivering secure, understandable systems. System integrators also have to ensure security, as even when all system components are secure, there may still be vulnerabilities when all the elements are integrated. Because of this shift in accountability, developers need tools that will allow them to accomplish security by design. Formal methods address this need and are discussed in the following section.

Closing the Gap with Formal Methods via SPARK

Simply improving visibility into existing systems is not enough to meaningfully address the software understanding gap. Traditional testing, while necessary, is insufficient on its own as it can reveal the presence of defects but not prove their absence.

This is where formal methods play a pivotal role.

Formal methods bring mathematical precision to software development. By expressing software requirements, designs, and implementations in formal logic, they enable automated reasoning and verification. Unlike conventional approaches, formal methods do not rely on incomplete test coverage or assumptions about execution environments. They provide proof-based confidence that a system behaves as intended under all specified conditions.

In safety- and security-critical domains, this level of assurance is not only desirable but often essential.

The Role of SPARK

SPARK provides Ada's strong typing and safety guarantees and is supported by an advanced formal verification engine that can prove a program's key properties at compile time.

This capability is not theoretical; it is deployed in practice today across aerospace, rail, defense, and other high-assurance sectors. SPARK supports scalable verification: projects can adopt formal techniques incrementally, focusing effort on the most critical components while still benefiting from static guarantees and tool-based feedback throughout the development lifecycle.

SPARK eliminates insecure defaults (such as uninitialized variables) and reduces failures by proving the absence of runtime errors (AoRTE). SPARK ensures that software has fewer latent defects (because of AoRTE) and allows developers to encode requirements derived from the security design decisions as contracts and prove them.

In the context of Secure by Design, SPARK enables software manufacturers to:

• Prove the absence of entire classes of vulnerabilities before code is ever executed,
  

• Rely on trusted, machine-checked proofs rather than manual review or reactive patching,
  

• Define the intended functionality clearly with contracts that explain what a software component needs (via preconditions) and what it does (via postconditions) without exposing all of the computation's details.

When considering how best to plan a secure-by-design system, formal proof provides the means to make high-assurance security, safety, and mission-critical arguments and shouldn't be overlooked. Read more about SPARK here.