The right next sentence is, "And by now it has proofs about further security properties (which show that the specification has the right properties)". In parti

The right next sentence is, "And by now it has proofs about further security properties (which show that the specification has the right properties)". In particular, they formalized notions of confidentiality, integrity, and availability, and proved the specification (hence the source code, hence the binary) satisfies these notions. Now you can ask whether these notions were formalized correctly. But that's still a LOT better than asking it for binary/source/specification.