The verification of seL4 on the 64-bit Arm architecture has reached another milestone. After completing the proofs of functional correctness and integrity, Proofcraft has now established the proof that seL4 enforces confidentiality on AArch64, providing a formal mathematical proof that the kernel prevents an application running on top of seL4 from learning information without authorisation. This milestone completes the formal proof that the seL4 implementation code on AArch64 enforces security isolation of the applications running on top (under the assumptions listed here [0]). This isolation prevents attacks on non-critical applications from propagating to critical applications and compromising them. https://proofcraft.systems/news-2026/#2026-08-21 [0] https://sel4.systems/Verification/assumptions.html June