[yeslibertarian]

hopefully in a future not so far away, most safety-critical code will be formally verified, like http://sel4.systems/ for example

[kevinr]

Code like the Boeing 787's avionics package gets one better: the spec specifies what the register values should be after each step of execution, and there's a company which takes the code, puts the processor in single-step mode, and checks.