Hopefully, for the pacemaker, the authors of the code would be using a verified compiler like CompCert (although it's only verified for the compilation, not the parsing or the preprocessor), but you don't have control at every level, like for the hardware. You can't verify centrifuge timings, but you can specify software and verify that it fits the specification to the point that it won't be the point of failure (assuming you have everything under control, like the pacemaker SDK, everything). I do see what you're saying about it being infectious, though.
