You can model physical devices to arbitrary degrees of precision. Lanyon is doing it. These are not limitations of verification. Metrological models of semiconductor fabrication can even do verification over the distribution of faulty circuit outcomes.
And while possible, good luck validating systems against intentional attacks-- fault injection, power tampering, bus attacks....
It is vital that "formally verified within X scope" does not turn into the leaky abstraction "is secure". Go watch Microsoft's talk on XBox security, and what they had to do to make it as secure as it is (primarily: tightly control hardware, code, and platform). It is not something you throw AI at, and it's not something that you can generalize to the entire computing world.