[dspillett]

> There is no reason the device should get in an undefined state

That is impossible to guarantee. It isn't even possible to completely generally[†] test for - what you have there is a variant of the halting problem (https://en.wikipedia.org/wiki/Halting_problem).

[†] added "generically" there as it is possible, using formal methods from the start, to prove that a program is correct so will not error (in an unexpected manner) on any input, but such methods are time-consuming so outside of certain specific fields you'll not find them used