Proofcraft completes the seL4 confidentiality proof on AArch64, closing the security proof stack for 64-bit Arm

Sources: primary, discussion
Summary: Proofcraft reports that the seL4 confidentiality proof now covers AArch64, joining the existing functional correctness and integrity proofs on that architecture. The proof holds under the assumptions listed in the announcement.
Why it matters: Functional correctness and integrity were already proved on AArch64, and confidentiality was the missing property, so an Arm seL4 system now carries a machine-checked isolation argument under the listed assumptions.