> Software doesn't exist in a platonic state like formal mathematics
Doesn't it? Like all these things you can model in the end, your state space, and thus necessary proofs and even just the spec itself would explode in size.
But that's how every single model works.
Software doesn't exist in a platonic state like formal mathematics, which at least can be consistent with all other results. Software interacts with the real world and "bugs" can be any number of security weaknesses like emitting useful timing signatures, buffer overflows that depend on the compiler used, weaknesses on certain hardware, etc.
It is great that Google has formalized code to some degree and for software that MUST be hardened, this may be valuable. It may be generally useful, but we need to get a feel for the gaps that inevitably will persist.