[jschwartzi]

That document is guidance. In it they suggest static analysis and formal methods, but they do not require them. You might get asked questions during a 510k if you don't explicitly call them out, though.

Therac-25 is actually an example of how a bad risk analysis and lack of appropriate mitigations for the level of concern can lead to patient injury or death. The design of the device meant that a single-fault condition in software could create a hazardous situation for the patient. When they revised the design for software control they removed a hardware mitigation.