Therac-25 is the poster child for this kind of failure mode. Formal verification and behavioral equivalences would be invaluable, I think, but I can't pretend I understand much about the underlying math of the former.