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.
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.