After proving the full functional correctness (that machine code implements spec), they did additional security proofs against the spec, including confidentiality and integrity. If you accept their TCB(no hardware bugs etc), the entire proof is incredibly strong.