I just wsnt to add that not even formal methods absolutely guarantee absence of errors. Firstly, there might be errors in the proof itself. Secondly, you always make assumptions about the CPU, memory and other hardware components. These might fail due to a variety of reasons: hardware bugs, electricity disturbances, heat, radiation, physical damage and more.
You're right that formal methods do not guarantee absence of 'errors' in the sense of unforseen unwanted behavior.
But formal methods, which typically are based on computer-checked proofs, can help you to eliminate certain possibilities. They are severely underestimated and underused because of our dependence on C.
The formal methods do not 'fail' as such. They just fail to prove anything boyond the proven property. Such properties can very well (and often do) include failure (of whatever kind) of parts in the system.
Apart from AI, which as an approach to embedded systems is almost by definition the opposite, I only see one way forward from the mess we're in now: formal methods.
That's why aerospace electronics have temporal and physical redundancy as well as voting algos. These generally rule out the radiation, physical damage, and RF issues.
