The Future of Safety for Software as a Medical Device (SaMD)
Software failures and exploits are not uncommon phenomena. With the emergence of Software as a Medical Device (SaMD), software exploits become personal attack vectors.
A pacemaker that miscounts a beat can do so quietly for years before anyone notices. The same is true of an insulin pump that misjudges a dose by a small margin, or a neurostimulator whose state machine takes an unintended branch under a rare combination of inputs. In an implantable device, a software malfunction may not be as easily recognizable as a software event from the start. A slightly wrong dose or a slightly wrong pacing interval reads as disease progression first, and as a software event much later, if at all.
This isn't a hypothetical problem. From 1990 to 2000, firmware-related recalls of pacemakers and implantable defibrillators affected more than 200,000 devices in the United States alone, accounting for 41% of recalls in that period [ref]. Each of those recalls would represent a property that escaped the robust testing methodologies available at the time, or that held during testing but quietly stopped holding in the field.
The category is harder to address today than it was in 2000. Implantable devices are more complex, networked, learning, and longer-lived than the regulatory frameworks they ship under were originally designed to govern. FDA-cleared closed-loop insulin systems are now in commercial deployment, including adaptive-learning algorithms that adjust to individual patient physiology over time. Cardiac devices communicate with home monitoring stations over wireless protocols that did not exist when the devices' verification methodology was first developed. The FDA's premarket cybersecurity guidance, formalized into a Refuse to Accept policy in 2023, is now an explicit gating requirement [ref]. And devices designed today are expected to remain inside patients for ten to fifteen years, against threat models no one writing today's specifications can fully anticipate, including AI-empowered malicious entities.
The industry has built a deep toolkit for this, including but not limited to hazard analyses, hardware-in-the-loop bench testing, animal studies, clinical trials, post-market surveillance with mandatory device reporting, all integrated in structured development methodologies such as the V-model lifecycle (IEC 62304). It has produced an industry that, in aggregate, is remarkably safe. But "in aggregate" is not the same as "in every device line." The gap between what the toolkit can guarantee and what the deployed device may eventually encounter has not closed. For software inside an implant, where the recall is not a patch but an explant procedure, the case for adding machine-checked proofs to the assurance stack is unusually strong.
Formal verification is what that kind of evidence looks like in practice. It produces mathematical proofs that a controller stays within the limits specified in its hazard file, regardless of input, and it exhaustively checks the safety of state machines rather than against the subset of transitions a test plan happened to exercise. The technique isn't new. It's been used in academic settings for decades and is finally reaching the kind of integration with commercial development that the regulatory environment now demands. For devices whose failures are measured in human lives rather than in dollars, that shift is overdue.
