When Reboot Isn't an Option

The Artemis II flight software — approximately 50,000 lines of code controlling human lives on the journey to lunar orbit — was "flown" more than 100,000 simulated times before the actual launch. But simulation alone can't guarantee correctness. For that, NASA increasingly relies on formal methods: mathematical techniques that prove software properties hold for all possible inputs, not just the ones you thought to test.

The NASA Formal Methods Program

The NASA Formal Methods Symposium, now in its 17th year, brings together researchers working on "formal techniques for software and system assurance in space, aviation, and robotics." The 2025 symposium at William & Mary focused on verification challenges for the next generation of space systems.

NASA's formal methods infrastructure includes:

  • NASA-STD-8739.8: Software Assurance and Safety Standard
  • NASA-STD-8739.9: Software Formal Inspections Standard
  • Independent Verification and Validation (IV&V): Applied to all human spaceflight programs

Projects currently under formal verification scrutiny include the Roman Space Telescope, Europa Clipper, Regenerative Fuel Cell systems, and all Artemis program elements — SLS, Orion, and Gateway.

The seL4 Verified Microkernel

seL4 represents the gold standard in formally verified operating systems. This microkernel — 8,700 lines of C and 600 lines of assembler — comes with a machine-checked proof from abstract specification down to the actual C implementation.

The proof guarantees: no code injection attacks, no buffer overflows, no null pointer dereferences. These aren't claims based on testing; they're mathematical certainties derived from the code itself.

Space Applications of seL4:

NASA's core Flight Software (cFS), which runs on the Artemis program and Roman Space Telescope missions, has been ported to seL4. This led to the development of Magnetite, a real-time operating system built on verified foundations.

Defense Applications:

DARPA's PROVERS and INSPECTA programs (started 2024) fund continued seL4 development. The CASE project with Collins Aerospace and Galois explores verified software for military aviation systems. DornerWorks has deployed seL4 for aerospace, defense, medical, and automotive customers since 2015.

DO-178C and the Formal Methods Supplement

Commercial and military aviation software follows DO-178C, released in December 2011 and recognized by the FAA, EASA, and Transport Canada. The standard defines Design Assurance Levels (DAL) A through E based on failure severity, with Level A — "catastrophic failure" — requiring the most rigorous verification.

The formal methods supplement, DO-333, provides specific guidance for applying theorem proving, model checking, and abstract interpretation to certification. Crucially, formal methods can complement or replace dynamic testing — you can prove properties instead of testing for them.

Additional supplements cover Model-Based Development (DO-331), Object-Oriented Technology (DO-332), and Tool Qualification (DO-330).

Astrée: Static Analysis at Scale

Astrée is a commercial static analyzer built on abstract interpretation theory. It doesn't test code; it mathematically analyzes all possible execution paths to prove the absence of runtime errors.

Aerospace Deployments:

  • Airbus (since 2003): Safety-critical software for the A380 and subsequent aircraft
  • European Space Agency (2008): Proved absence of runtime errors in the Jules Verne ATV automatic docking software — the system that autonomously docked supply vessels with the International Space Station

Other Safety-Critical Industries:

  • Bosch Automotive Steering (2018): Replaced legacy analysis tools, acquired worldwide license
  • Framatome: TELEPERM XS platform for nuclear reactor control systems

Astrée is certified by NIST as satisfying criteria for sound static code analysis (2020) and complies with ISO 26262 (automotive), DO-178B/C (aerospace), IEC-61508 (functional safety), and EN-50128 (railway).

Technical Capabilities:

The analyzer detects divisions by zero, buffer overflows, null pointer dereferences, data races, and deadlocks. It also estimates Worst-Case Execution Time (WCET) — critical for real-time systems where missing a deadline can be as dangerous as computing the wrong answer.

SpaceX: A Different Philosophy

SpaceX takes a somewhat different approach to software verification. Falcon 9 runs three dual-core x86 processors executing Linux, with code written in C/C++. The architecture relies on triplex redundancy — three independent computers that vote on decisions — to tolerate both hardware failures and potential software bugs.

As SpaceX engineers have noted: "Writing the software is some small percentage of what actually goes into getting it ready to fly." The verification process involves extensive simulation, defensive programming, and fault-tolerant architecture.

For NASA's Commercial Crew Demo-1 mission, the requirement was explicit: software must be tolerant to any two simultaneous faults. Redundancy compensates for uncertainty.

The Verification Spectrum

These approaches represent different points on a verification spectrum:

| Approach | Assurance Level | Cost | Applicability |

|----------|-----------------|------|---------------|

| Formal proof (seL4) | Mathematical certainty | Very high | Critical kernels, security foundations |

| Static analysis (Astrée) | Absence of specific bug classes | High | Safety-critical applications |

| Model checking | Exhaustive state exploration | Medium-high | Protocol verification, concurrent systems |

| Redundancy (SpaceX) | Fault tolerance | Medium | Systems where verification cost exceeds redundancy cost |

| Testing | Confidence, not proof | Variable | Everything (necessary but not sufficient) |

LOGOS and Space Systems

Natural language requirements documents are standard in aerospace. "The system shall not permit commanded thrust during crew egress" is a requirement that must be translated into verified software behavior.

LOGOS enables this translation explicitly. A requirement stated in controlled English can be parsed into first-order logic, which can then be checked against formal specifications of the software. The gap between what the requirement document says and what the code does becomes formally verifiable.

Combined with tools like Z3 for satisfiability checking, this pipeline could reduce the manual effort in aerospace verification while increasing confidence in the translation from requirements to implementation.

The Stakes

When software fails in space, there's no patch deployment. The Artemis astronauts will be 250,000 miles from the nearest software engineer. Every line of code, every state transition, every interrupt handler must work correctly the first time and every time after.

Formal verification doesn't make this easy. But it makes it possible to know — with mathematical certainty — that critical properties hold. In an environment where "pretty sure" isn't good enough, proof matters.

Further Reading