The Future of Safety for SaMD Assurea Team Rhea Malhotra, Biomedical Engineering Researcher · Tanya Sharma, Co-Founder · Krisha Patel, Co-Founder · Satvika Sharma, Design Verification Researcher
arXiv:2609.15438v1 [cs.SE] 14 Sep 2026
Industry Professionals Heena Purkait, Senior Engineering Project Manager, Fresenius Medical Care · Mehak Nehal Makhija, Quality Assurance and Validation Specialist, Baxter Healthcare Runtime Verification Team · Everett Hildenbrandt, CEO · Palina Tolmach, CTO
Aellison Cassimiro∗ , Formal Verification Engineer
Virginia Tech University Jaidev Shastri, Graduate Research Assistant
September 14, 2026
Abstract An artificial organ carries failure consequences on the scale of an aircraft or a reactor, but the software driving it is rarely held to the same standard. Teams building them rely on testing, which only reaches the failure modes someone thought of in advance. In a pump or controller that runs inside a patient for months, the dangerous cases are the ones nobody anticipated. Formal verification closes that gap. Applied to the device’s software, it proves the code meets its specification for every execution that specification allows, and where a proof fails, it returns the exact input sequence that breaks it. The same methods already protect rail, aviation, and nuclear control systems, and they extend the IEC 62304 lifecycle that a manufacturer already follows rather than replacing it. In this paper, we explore how to apply formal verification to artificial organs, stage by stage, and what each technique actually guarantees about the device.
1 Our Motive Within the market for artificial organs, companies must use appropriate means to verify and validate their software and designs due to the life-critical nature of their products. Regulatory frameworks like the FDA’s and the EU’s Medical Device Regulation ensure that these devices are able to operate correctly for the sake of a patient’s life, and therefore enforce hard audits and guidelines for validation teams. The current most widely employed method of verification is the traditional “spot-checking”, where engineers use tools to test against specific failure modes in a device’s software or design. This approach gives some assurance as to the efficacy of their product, however, if only certain genres of failure modes are tested against, then there may be infinite unique corner cases or other modes that are left unchecked. For this reason, developers within nuclear, automotive, aerospace, and other industries use an alternative method for validating their device, one that checks against every possible failure mode and ensures that their product will always perform as expected. Formal verification (FV) allows an engineer to say that their product will at all times perform as outlined by a set of requirements, and within the medical device world, can give a patient the assurance they need when dealing with a device so integral to their health and wellness. ∗ Corresponding author: Aellison Cassimiro, [email protected].
1
2 What is Formal Verification? Let us consider a driver that paces an artificial heart. Its software must raise an alarm when it detects a fault, hand control to a backup controller if the main computer fails, and keep pumping while any power source remains. A test suite can exercise these behaviors for chosen inputs and report what happened. It tells us whether the software worked for the cases we thought of running. The behaviors we did not anticipate remain unexamined, and for a device that runs continuously for months inside a patient, the untested cases are where the risk is concentrated. Formal verification takes a different route to confidence by establishing mathematical arguments that a program satisfies a specification, covering every execution the specification admits, rather than a sample of them. It works, at a high level, by translating a device’s requirements into a formal model, then using tools like model checkers and theorem provers to either prove that the model satisfies those requirements or produce a concrete counterexample showing exactly where it fails. That counterexample is the real value: instead of a vague sense that something might be wrong, engineers get an exact input sequence or state that breaks the system. Within a given device, one that possesses software that drives the function of the product, certain properties of this software can be formally specified. If a property reflects a behavior that must be truthful at all times of the system execution, we can refer to it as an invariant. Written in logic rather than prose, such statements become objects that a tool can verify. These invariants can be tested to some extent using the approaches currently used in the field, including unit tests, integration tests, coverage testing, fuzzing, and other techniques. Still, these do not provide concrete proof with certainty of safety. A formally verified property is guaranteed to hold for any configuration that the system can find itself in. In other words, while traditional testing approaches guarantee that a device’s functionality works for a specific input or set of inputs, formal verification can validate these same functionalities for all semantically valid inputs, either mathematically proving safety or identifying configurations in which the device’s safety is compromised. Work on proving properties of programs began in the 1960s and has been going on continuously since. The logics came first, then machine assistance for the proofs, then solvers fast enough for industrial problems, and more recently analysers that work on production source. The earliest safety cases built on proof date from around 1990, and systems verified this way have entered service ever since, several still running today. A team adopting these methods now takes up a discipline developed and tested in the field for more than sixty years. Formal verification as a field is recognized for the strength of the guarantees it provides, and it is used in multiple crucial systems with the same level of severity as medical devices. Some of them are: • Rail (Paris Métro): The driverless trains on Line 14 run on software whose logic was proven mathematically before it was written as code. Proof replaced unit testing entirely, and the developers report no faults found since the line opened in October 1998. [1, 2] • Air travel (Airbus flight controls): The software moving the control surfaces on the A340 and A380 was analyzed across every possible execution, not a selection of test cases, and shown to be free of arithmetic and memory faults even in its floating-point calculations. [3, 4] • Naval aviation (helicopter landing advice): A system advising crews whether a helicopter can safely land on a moving warship was built for proof, with roughly 150 proofs on its specification and 9,000 on its code. The team found proof was more efficient at catching faults than the testing they ran alongside it. [5] • Nuclear power (reactor shutdown): The software shutting down the reactors at Ontario’s Darlington station was written as precise tables of required behavior, with a theorem prover confirming the design met them. It stands among the earliest cases of a national regulator accepting mathematical proof in 2
place of testing alone. [6] • Spacecraft (NASA probe): Before Deep Space 1 launched, formal analysis of its autonomous control software found five timing faults that the developers said testing would have missed. Faults of that same kind later suspended the probe’s operations in flight. [7, 8]
3 Closing the Verification Gap Artificial organs carry the failure consequences of aerospace or nuclear control systems, but rarely the verification rigor of those industries. Formal verification (FV) closes that gap with exhaustive mathematical proof that a system behaves correctly across every possible input and state instead of just the scenarios an engineer tests. Before any artificial organ reaches a patient, it has to clear regulatory approval, whether that’s the FDA in the United States, the EU’s Medical Device Regulation in Europe, or an equivalent regime elsewhere in the world. Despite operating in different countries, these regulators largely converge on the same underlying standards for medical device software, requiring manufacturers to prove their devices have been thoroughly checked for errors before reaching patients. Right now, most companies do this through testing: running the device through thousands of scenarios and checking that nothing goes wrong. Formal verification covers those scenarios and every single other one, leaving nothing to chance and ensuring successful operation. For a device like an artificial heart or an insulin pump, where a single overlooked scenario could be fatal, that distinction matters. Because formal methods produce a clear, provable record of what was checked and why, they fit naturally into the kind of documentation regulators worldwide already expect, which makes them not just safer, but easier for regulators to trust [9], regardless of where the device is headed to market. To assess and analyze how that integration would occur, and its benefits within the company and for consumers, let us examine the pathway for incorporating formal methods into the existing device development. 3.1 Incorporating FV Methodologies into Artificial Organs & Why It Is an Effective Solution While artificial organs are a relatively novel innovation, it is clear that their need for safety is paramount. Any small infraction of the device requirements or a system bug can snowball into catastrophic failure, resulting in medical complications or even death. Medical devices with software-based systems benefit from the coded formal model, while mechanical, software-lacking devices have formalized continuous properties that address mechanical failure. Where traditional testing leaves gaps in assurance through unexplored corner cases, timer overflows, and other limitations, formal methods ensure that the device is working correctly as defined at all times. The development of medical device software, as laid out by IEC 62304 [10], begins by classifying the software according to how much harm its failure could cause, which sets how demanding every later step becomes. The team then fixes its ground rules, naming the coding standards, methods and tools it will use. Engineers verify each unit of code against acceptance criteria they have defined, usually by testing and measuring how much of the code those tests reach. They then combine the units and check that the interfaces behave and that the safety measures engage, often by deliberately inducing faults. The assembled software runs on the real hardware. At release, every known defect still present is recorded with a written justification for leaving it. Once the device reaches patients, later changes are handled as maintenance, with each change assessed for the risk it introduces and the untouched software re-tested around it. Version control and problem reporting run throughout. Every step in this sequence rests on running the software and observing what happens, which means the evidence it produces covers the situations the engineers thought to create. The design stage is the primary and most crucial point for FV incorporation; however, the methodology can be applied throughout the development lifecycle. The differences between the two main device
3
types (software-based vs purely mechanical) lie primarily in how formal methods are approached, rather than directly employed. A device’s properties are outlined similarly, and hazards are established. The divergence occurs when setting physical versus software requirements, and the following models are generated and tested. Once properties are proved and counterexamples or violations are fixed, device compliance regulation submissions can occur (FDA, CE Mark, etc.). FV’s most mature tooling, including model checkers and theorem provers, target software and digital logic. For software-driven organs (insulin pumps, pacemaker firmware, dialysis controllers) [11–13], the path is borrowing directly from aerospace and automotive safety-critical practice [14–16]. For primarily mechanical or biomaterial devices (a mechanical heart valve, a biomaterial scaffold), FV’s role narrows to the control systems, design, build, and safety interlocks around the device, which ensure the device’s physical operation. Formal methods are applicable across all medical devices, and the steps taken to ensure the formal properties shift accordingly. It is important to highlight that, while it is possible and extremely beneficial to apply FV in the development of purely mechanical medical devices, the process of applying formal methods to it becomes something that is tailored.
spans all
ARTEFACT BUILT · CHECK PERFORMED
GUARANTEE OBTAINED
Classify
Cl. 4.3
No new artefact — classification fixes how much must be proven
Depth of formal evidence follows the safety class
Plan
Cl. 5.1.4 (C)
Write the property set and assumption register (Cl. 5.2); build the design model (Cl. 5.3); select and qualify the tools
A checkable definition of correct behaviour, and tools whose results may be relied on as evidence
Units
Cl. 5.5.2–5.5.5 (C)
Derive unit contracts from the property set and the decomposition (Cl. 5.4); write them into the source and discharge by proof; sound static analysis; unit tests remain
Correct for all inputs, not a sampled subset, and free of runtime errors. Proven on the source, so no model-to-code gap arises here
Integration Cl. 5.6, 7.3
Model-check the design model; argue that composed unit contracts entail it, and that the model abstracts the code
Every interleaving explored, and unit proofs made to bear on system properties. Subject to both arguments holding
System
Cl. 5.7
Build a plant and patient model; verify timing and Worst-case deadlines bounded and the closed-loop behaviour against it loop shown to stay in a safe envelope, given stated assumptions
Release
Cl. 5.8
Assemble the evidence into an assurance case; Residual risk stated as named unproven carry open properties and unmet assumptions into properties, not only as a count of known the risk file defects
Change
Cl. 6.2, 7.4
Update property set, design model and contracts A revision inherits proofs rather than together; re-establish only the proofs the change assumptions, with no accumulating invalidates unverified legacy
Always
Cl. 8, 9
Version properties, model, contracts and proofs with the code; monitor at runtime the assumptions proof left undischarged
Evidence stays synchronised with the code, and undischarged assumptions are watched in service
Figure 1: Formal Verification Applied to the Artificial Organ Software Development Pathway
As seen in Figure 1, formal methods change what each of those checks establishes. Each phase has an added security technique using applied formal methods to generate artefacts. Artefacts are any concrete work product the process creates and keeps. It can be a document, a model, a specification, a set of test 4
cases, or a proof that represents the goal of that stage. Planning gains two products the process did not have before: the properties themselves, and a register of the assumptions they depend on. At the units stage, sound static analysis [17] reasons over every state the program could reach, without running any of it, and proves the code cannot overflow, divide by zero or read outside an array on any run. It needs nothing specified in advance. Deductive verification goes further. A contract on each unit states what it needs from its caller and what it promises in return [18, 19], tools translate the code and its contract into logical obligations, and a prover discharges them. Each proof holds for every input the contract permits, and it applies to the shipping source. The question shifts from whether the chosen test values behaved correctly to whether any value could behave otherwise. During integration, model checking [20, 21] takes a simplified model of the design, records the states the system can occupy and how it moves between them, and explores every path the model allows. Claims about failover and deadlock get settled across all interleavings rather than the handful of faults an engineer thought to induce, and a failing property comes back as a step-by-step trace to the violation. At the system stage, the same exploration, extended over time, runs against a model of the patient and pump, and bounds the worst-case for alarm and pump-cycle deadlines instead of reporting the slowest case seen on the bench. At release, the record lists which properties were proven and which remain open, stating residual risk in terms of behavior rather than a count of known defects. During maintenance, the team re-establishes only the proofs that a change breaks, so later versions inherit proofs instead of assumptions. Once the device is in service, runtime verification compiles those same properties into monitors that run beside the software and report a violation the moment it occurs. These are just a few examples of techniques available to enhance the security of the medical device development lifecycle. 3.1.1 Industry Perspective by Heena Purkait: Engineering Project Management From a project management perspective, the value of formal methods within an artificial organ development process is closely tied to how regulatory expectations shape the schedule itself. Regulators may converge on the same underlying standards, but compliance execution rarely does. Working across EMEA, every country carries its own certification requirements and its own logic, and obligations like GDPR can stall an otherwise ready product if they aren’t accounted for at the design stage. That gap between shared standards and fragmented compliance is where a provable record matters most: each company’s QMS runs on SOPs built around FDA guidance, and a formal, traceable model of what was checked and why holds up the same across every regulator’s submission, even when the surrounding paperwork does not. Verification rigor does not stay uniform across a project either, it shifts with device complexity and with where the product is being submitted. If the right people are not assigned early, or a defect turns out to be a requirements gap rather than an implementation error, that is a coordination failure as much as a technical one. Formal verification, integrated early and tied to SMART, specific, measurable, achievable, relevant, time-bound goals, gives a way to surface those gaps before they collapse a timeline late in the project. Selling that shift to stakeholders who are measured on delivery dates, not defect rates, is the harder part of the role. It comes down to making sure every function (engineering, quality, human factors, and risk) is informed at each phase, and reminding people of their responsibility when it is easy to lose track in a complex project. Existing methodologies like RACI (responsible, accountable, consulted, informed) and each company’s QMS systems can be better supported by formal verification methods, and when these engines are able to produce definable traces to the root causes of a bug, then each team member benefits from that clarity. Ultimately, the integration of FV within the standard artificial organ development pathway occurs at each and every stage, and every team member is responsible for engaging with formal methodologies. This process allows us to identify risks and errors early on and move forward efficiently, and as a project 5
manager, this methodology can be integrated seamlessly within our scheduling and regulatory standard teams, which are better equipped to deal with issues. 3.2 Quality Considerations for Employing Formal Methods Formal Verification is an addition to existing Quality Assurance (QA) processes, not a replacement. Manufacturers in the US, for example, operate under ISO 13485 [22], IEC 62304, and FDA design controls. FV slots into that framework as a rigor layer, not a replacement for it. The necessary scaffolding for the generation of proofs over properties can be abstracted to a two-stage process. First, someone must write down what “correct” means with enough precision to reason about. Second, a tool must relate these statements to the program. The first stage encompasses the definition of a set of properties, which are formally expressed claims about the software’s behavior. As previously explored, we can also mature our properties into invariants once we define the behaviors that should hold at any given moment in the device’s lifecycle. The second element varies by technique, which can be used in conjunction to identify issues both related and unrelated to the properties and invariants raised so far. These invariants are the guiding principles of the strategies employed during the development process, explored in Figure 1, and it is of utmost importance that they are well defined and understood. Both failure and correct functioning must be clear at design time to assure the highest extraction of value possible from the formal verification techniques. 3.2.1 Industry Perspective by Mehak Makhija: QA & Validation From a Quality Assurance and Validation perspective, Formal Verification (FV) should strengthen, not replace, traditional verification and validation methods by addressing the finite limitations of current testing. It shifts the focus from checking representative scenarios to mathematically proving that critical safety properties hold across all possible system states. This is particularly valuable because software failures can emerge from rare interactions between functions that individually passed verification. In traditional QA practice, these gaps may be identified proactively through FMEAs, risk assessments [23], design and protocol reviews, or traceability assessments; others may only surface through deviations, nonconformances, complaints, or post-market investigations. An intermittent timing or communication failure, for example, may require event-log reconstruction, root-cause analysis, corrective action, and expanded regression testing before the failure sequence is understood. Applying formal methods earlier creates an opportunity to identify some of these edge cases before they become validation failures, CAPAs, field corrections, or patient safety events. From a validation standpoint, FV can be integrated directly into the existing requirements-to-risk-toverification traceability structure. A safety-critical requirement, such as an artificial pancreas suspending insulin delivery under an unsafe glucose condition or an artificial heart controller maintaining safe operation during failover, would still link to its hazard analysis, risk controls, verification activities, acceptance criteria, and validation evidence. Formal proof simply adds another layer of objective evidence for design review and regulatory assessment. However, FV also introduces responsibilities for defining appropriate safety properties, validating assumptions, maintaining models as designs change, and interpreting proof results. A proof is only as meaningful as the requirements and model on which it is based, making QA oversight and traceability essential. Ultimately, FV’s greatest value is defect prevention. Stronger audit defensibility and regulatory readiness are important benefits, but for artificial organs and other life-sustaining devices, the primary objective is to identify critical failures as early as possible and prevent them from reaching the patient.
6
3.3 Traditional Verification’s Gaps within Life-Critical Environments Within an artificial organ, the situation is as immediately life-critical as aerospace or nuclear environments, if not more so. A single bug could cause immediate health issues or death (cardiac arrest, glucose overdose, etc). Formal verification closes the gap that traditional spot testing leaves open, oftentimes missing race conditions at exact clock boundaries, mode-transition deadlocks (two valid moves collide), timer overflows, threshold boundary bugs (sensor exactly at limit), general concurrency and non-determinism issues between different modules of a complex system, and unexplored corner cases. It is not that traditional approaches neglect these properties, but rather that they have limitations on how to test them. Integrating formal verification into the regular development pathway for an artificial organ will ultimately increase the safety coverage of the claim a medical device company can make. A checkable mathematical object is categorically stronger than “X tests passed at Y% coverage” and directly strengthens the FDA Class III safety-and-effectiveness case. The effectiveness of this methodology lies in its ability to ensure a device that will never compromise a patient’s life: an artificial organ that cannot spontaneously reach a shutdown state and cause immediate organ failure, or encounter a unique corner failure mode and enter a static or false state that administers the incorrect amount of medication. This level of assurance is not only superior to that of traditional testing, but vital in the life-critical environment that medical devices such as artificial organs exist within. Testing samples the input space, while a proof ranges over everything the specification admits, which makes coverage measurement largely beside the point at the unit level. The guarantee is complete in one direction and conditional in another. It holds for every input and every execution. Although it only holds for the properties someone wrote down, under the assumptions someone recorded, and, when a model is used, only as far as that model matches the code. The gaps, therefore, do not disappear. They move to three places that can be named and managed: properties nobody thought to state, assumptions about hardware and environment taken on trust, and the argument connecting a model to the software it stands for. Runtime monitoring addresses the second of these by watching in service for assumptions that could not be settled. The practical difference is that what remains uncertain becomes explicit. In a testing-only process, whatever was not examined stays unknown and uncounted. With proofs in place, whatever remains unproven has a name, can be written into the safety file, and can be argued about or watched.
4 To Conclude A patient-oriented market such as that of artificial organs requires certain levels of trust between both the company and the person utilizing their product. That trust ensures the safety and health of the patient, and it is dependent on the regulations set by the governing organization and the validation methods of the company. If this trust can be fortified and the device’s design verified against each and every possible failure mode, then customers would be more willing to reach out to companies in pursuit of a better quality of life facilitated by their products. Formal verification methods are the key to strengthening trust, and employing methods like model checking, timed automata, and more can allow a safer and more trustworthy environment within the patient community.
References [1] P. Behm, P. Benoit, A. Faivre, and J.-M. Meynadier. “Météor: A Successful Application of B in a Large Project”. In: FM’99 — Formal Methods. Vol. 1708. Lecture Notes in Computer Science. Springer, 1999, pp. 369–387. url: https://link.springer.com/chapter/10.1007/3-540-48119-2_22.
7
[2] CLEARSY. Extension of Line 14 of the Paris Metro: over 25 years of reliability thanks to the B formal method. url: https://www.clearsy.com/en/the-tools/extension-of-line-14-of-the-parismetro-over-25-years-of-reliability-thanks-to-the-b-formal-method/. [3] J. Souyris and D. Delmas. “Experimental Assessment of Astrée on Safety-Critical Avionics Software”. In: SAFECOMP 2007. 2007. url: https://www.researchgate.net/publication/221147374_ Experimental_Assessment_of_Astree_on_Safety-Critical_Avionics_Software. [4]
The Astrée Static Analyzer. url: https://www.astree.ens.fr/.
[5] S. King, J. Hammond, R. Chapman, and A. Pryor. “Is Proof More Cost-Effective Than Testing?” In: IEEE Transactions on Software Engineering 26.8 (2000), pp. 675–686. url: https://ieeexplore.ieee. org/document/879807/. [6] M. Lawford and A. Wassyng. Formal Verification of Nuclear Systems: Past, Present, and Future. Information & Security. url: https://isij.eu/system/files/2023-01/28.18_Lawford_Wassyng.pdf. [7] K. Havelund, M. Lowry, and J. Penix. “Formal Analysis of a Space-Craft Controller Using SPIN”. In: IEEE Transactions on Software Engineering (2001). url: https://www.semanticscholar.org/ paper/a06bf55a3bee974e6abd559583cfe789129a3beb. [8] K. Havelund et al. Formal Analysis of the Remote Agent Before and After Flight. Tech. rep. NASA Technical Reports. url: https://ntrs.nasa.gov/api/citations/20000055731/downloads/20000055731. pdf. [9] U.S. Food and Drug Administration, Center for Devices and Radiological Health. Infusion Pump Software Safety Research at FDA. fda.gov. [10]
International Electrotechnical Commission. IEC 62304:2006/A1:2015. Medical Device Software — Software Life Cycle Processes.
[11]
D. Arney, R. Jetley, P. Jones, I. Lee, and O. Sokolsky. “Formal Methods Based Development of a PCA Infusion Pump Reference Model: Generic Infusion Pump (GIP) Project”. In: Proceedings of HCMDSS. Boston, 2007, pp. 23–33.
[12]
Y. Zhang, R. Jetley, P. Jones, and A. Ray. “Generic Safety Requirements for Developing Safe Insulin Pump Software”. In: Journal of Diabetes Science and Technology 5.6 (2011), pp. 1403–19.
[13]
P. Masci, Y. Zhang, P. Jones, P. Curzon, and H. Thimbleby. “Formal Verification of Medical Device User Interfaces Using PVS”. In: FASE 2014. Springer, 2014, pp. 200–214.
[14]
RTCA. DO-178C. Software Considerations in Airborne Systems and Equipment Certification. 2011.
[15]
RTCA. DO-333: Formal Methods Supplement to DO-178C and DO-278A. Standard record via GlobalSpec. 2011.
[16]
ISO. ISO 26262:2018. Road Vehicles — Functional Safety, Part 6, Clause 6.4.7.
[17]
P. Cousot and R. Cousot. “Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints”. In: Proc. 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages. 1977.
[18]
C. A. R. Hoare. “An axiomatic basis for computer programming”. In: Communications of the ACM 12.10 (1969).
[19]
B. Meyer. “Applying ‘Design by Contract’”. In: IEEE Computer 25.10 (1992).
[20]
E. M. Clarke and E. A. Emerson. “Design and synthesis of synchronization skeletons using branching time temporal logic”. In: Logic of Programs. 1981. 8
[21]
J. P. Queille and J. Sifakis. “Specification and verification of concurrent systems in CESAR”. In: International Symposium on Programming. 1982.
[22]
ISO. ISO 13485:2016. Medical Devices — Quality Management Systems — Requirements for Regulatory Purposes.
[23]
ISO. ISO 14971:2019. Medical Devices — Application of Risk Management to Medical Devices.
9