Now, the question is can we make some kind of formal verification language that forces checks everything and doesn't allow bugs? Maybe?
But that's assuming the underlying hardware and firmware doesn't have flaws that can break those assumptions too.
This is the general trade off for being correct. Being mostly right is easy, but leads to complex security issues later. Being correct is very hard, but should reduce the number of flaws to a manageable level.
I think Lean or Ada would be examples of different types of correctness contracts.
But even that isn't a foolproof winning strategy. When you start digging deeply you realize we exist in the allegory of platos cave. The reality we experience is an emergent phenomenon related to the scale at which humans operate. Things that operate at a much smaller scale experience a completely different reality than you do. For example gravity becomes so insignificant it's like it doesn't even exist when you're small enough. At least for me it's not hard to imagine nano machines that infect the substrate of a CPU and farm all your secrets out on side channels, or any number of other things that are pure sci-fi at the moment.