seL4 microkernel achieves full formal security verification on AArch64

Proofcraft has announced the completion of formal mathematical proofs for the seL4 microkernel on the AArch64 architecture. The latest milestone establishes that seL4 enforces confidentiality, providing a rigorous guarantee that the kernel prevents an application running on top of the system from learning information without authorisation.

This achievement marks the final step in the verification process. Prior to this announcement, Proofcraft had already completed proofs of functional correctness and integrity for the microkernel. The new confidentiality proof completes the formal demonstration that the seL4 implementation code on AArch64 enforces security isolation for the applications running on top of it.

The verification was achieved with continued support from the National Cyber Security Centre (NCSC). According to Proofcraft, the formal proofs are valid under a specific set of assumptions listed in their documentation. While the mathematical proof is definitive within those parameters, it confirms the logical structure of the security model rather than guaranteeing the absence of all real-world implementation errors.

The primary benefit of this proven security isolation is the containment of threats. By preventing unauthorised information leakage, the architecture stops attacks on non-critical applications from propagating to critical ones. This isolation is designed to protect essential system functions from being compromised by vulnerabilities in less important software layers.

For institutions relying on high-assurance operating systems, the completion of these proofs on AArch64 represents a significant step towards broader adoption. The AArch64 architecture is widely used in modern servers and embedded systems, making the verified status of seL4 on this platform a key development for infrastructure security.

The announcement was published on 21 August 2026, following the release of the final proof components. The project underscores the growing role of formal verification in modern software engineering, where mathematical certainty is increasingly valued over traditional testing methods for critical infrastructure.