The Therac-25 Lesson

Between 1985 and 1987, the Therac-25 radiation therapy machine caused at least six accidents where patients received approximately 100 times the intended radiation dose. Multiple patients died. It remains "the worst series of radiation accidents in the 35-year history of medical accelerators."

The cause was software. Specifically: race conditions in concurrent programming and the removal of hardware interlocks in favor of software-only safety checks.

The manufacturer initially dismissed user complaints as "impossible" — the software couldn't produce those readings. The software could. It did. Patients paid with their lives.

The Complexity Problem

Modern medical devices are orders of magnitude more complex than the Therac-25:

  • Contemporary pacemakers: up to 80,000 lines of code
  • Infusion pumps: more than 170,000 lines of code
  • A 200,000-line device can have more than 10^12 individual execution paths

Manual analysis of all paths in a 200,000-line device would require 20,000 developers working for over 100 years. Testing all paths isn't just impractical; it's mathematically impossible within any reasonable timeframe.

IEC 62304: The Software Lifecycle Standard

IEC 62304 is the international standard for medical device software lifecycle processes, recognized by the FDA, European regulators, and health authorities worldwide.

The standard classifies software by risk:

| Class | Risk Level | Example |

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

| A | No injury possible | Data display, documentation |

| B | Non-serious injury possible | Monitoring alerts, dosage calculations with manual override |

| C | Death or serious injury possible | Closed-loop drug delivery, radiation therapy control |

Class C software — where bugs can kill — requires the most rigorous verification. Changes must be verified through testing, regression testing is mandatory, and integration with ISO 14971 risk management is required throughout development.

The FDA recognizes IEC 62304 conformity, which can significantly reduce 510(k) submission documentation requirements.

Why Testing Isn't Enough

The fundamental limitation of testing is coverage. A test demonstrates that specific inputs produce correct outputs. It says nothing about untested inputs.

For the Therac-25, the race condition that caused overdoses occurred only under specific timing conditions — when operators entered commands at a particular speed in a particular sequence. Normal testing didn't trigger it. The condition existed in the code, invisible to testers.

Formal verification inverts this relationship. Instead of checking specific inputs, formal methods prove that properties hold for all possible inputs. "The radiation dose shall never exceed the prescribed maximum" becomes a mathematical statement verified against the code itself.

Formal Methods in Medical Device Verification

Research applications of formal verification in medical devices:

Insulin Infusion Pumps: Researchers have used Event-B modeling language and Rodin proof tools to verify safety properties of insulin pump software. The Generic Infusion Pump (GIP) Project created a reference implementation verifiable against safety requirements.

Pacemakers: Pacemaker software has been formalized using Event-B, with Abstraction Trees enabling closed-loop model checking — verifying not just the device software but its interaction with models of cardiac physiology.

Static Analysis: Formal methods-based static analysis can exhaustively explore software behavior in minutes, proving absence of runtime errors like null pointer dereferences, buffer overflows, and arithmetic exceptions.

The Regulatory Trajectory

The FDA has signaled increasing interest in formal methods for pre-market review. Guidance documents acknowledge that traditional testing alone may be insufficient for high-complexity, safety-critical software.

Current trends in FDA regulation emphasize:

  • Software as a Medical Device (SaMD): Software that itself qualifies as a medical device, regardless of hardware
  • Cybersecurity: Connected devices introduce vulnerabilities beyond functional correctness
  • Machine Learning: AI/ML-based devices require new verification paradigms

IEC 81001-5, now recognized by the FDA, addresses health software security lifecycle — verification must extend beyond functional correctness to include security properties.

Verification Techniques Applicable to Medical Devices

The same tools used in aerospace apply to medical devices:

Abstract Interpretation (Astrée): Proves absence of runtime errors including divisions by zero, buffer overflows, null pointer dereferences. Already used in nuclear reactor control systems.

Model Checking: Exhaustively explores finite state spaces. Effective for protocol verification and concurrent systems — exactly the kind of code that killed Therac-25 patients.

Theorem Proving (Z3, Coq): Generates mathematical proofs of program properties. Higher assurance than other methods; higher cost.

Formal Specification Languages: Event-B, TLA+, Alloy enable precise specification of system behavior for analysis.

LOGOS for Medical Requirements

Medical device requirements documents are written in natural language: "The pump shall cease infusion if the pressure exceeds the safety threshold." These requirements must be translated into software specifications, then into code, then verified.

LOGOS provides a formal semantics for this translation. The English requirement parses to first-order logic:

∀t∀p(Pressure(t) > SafetyThreshold ∧ Infusing(t) → Cease(t+1))

This formal specification can be:

  • Checked for internal consistency (does it contradict other requirements?)
  • Traced to implementation (does the code satisfy this property?)
  • Verified against the final system (does the compiled software maintain this invariant?)

The gap between what regulators read in requirements documents and what verification tools analyze becomes explicit and auditable.

The Stakes

A modern pacemaker makes life-or-death decisions millions of times over its operational lifetime. An insulin pump calculates drug doses that could cause hypoglycemic shock if wrong. A radiation therapy system delivers energy that heals at correct doses and kills at incorrect ones.

These devices cannot be recalled like smartphones. They cannot be patched over the air. They must work correctly from deployment through end of life, in patients whose physiological states the developers couldn't anticipate.

Formal verification doesn't make this easy. But it provides mathematical guarantees that testing cannot. For software that decides who lives and who dies, those guarantees matter.

Further Reading