The problem with formal verification of systems like this is that checking whether software matches the specification or whether the specification is self-consistent is not the interesting problem. Whether specification matches the real world is the interesting problem and there is no formal way to verify that.