seL4 security proofs now complete on AArch64
Summary
Proofcraft announces that seL4 now has a complete confidentiality proof on AArch64, completing the trio of formal proofs (functional correctness, integrity, confidentiality) for the kernel. The result formalizes isolation guarantees that prevent apps from learning or tampering with data, supported by NCSC. The post also highlights related verification milestones (MCS on RISC-V), a new dynamic domain scheduler, and Proofcraft’s engagement with the seL4 summit and community.