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.