seL4 completes formal security proofs on 64-bit ARM

Proofcraft announced on August 21, 2026, that the security proofs of the microkernel seL4 are complete on the AArch64 architecture, the 64-bit variant of ARM. As a result, there is now a formal mathematical proof that the kernel prevents an application running on top of seL4 from obtaining information without authorization, a property known as confidentiality.

This was the last missing piece. The proofs of functional correctness and integrity (that the kernel prevents an application from modifying data without authorization) had already been completed for AArch64. Closing confidentiality completes the entire security proof stack for the 64-bit ARM architecture. The work had continued support from NCSC, the UK's cybersecurity agency.

What "formal proof" means here

seL4 is not an ordinary kernel. It is the first general-purpose operating system kernel whose code implementation has been mathematically verified, using the Isabelle/HOL proof assistant. Instead of relying on testing, fuzzing and code review to reduce the chance of bugs, formal verification demonstrates, with mathematical rigor, that the code does exactly what the specification says, under an explicit set of assumptions.

In the case of security, this translates into a guarantee of isolation: an attack that compromises a non-critical application cannot spread to a critical application running on the same machine. According to Proofcraft, this is exactly the isolation that the proof stack now guarantees on AArch64, within the assumptions listed by the team. One caveat is worth noting: the proof holds under these assumptions (for example, about hardware and compiler behavior); it is not an absolute guarantee against any physical or side-channel attack outside the model.

Why AArch64 is the relevant target

seL4 was born with verification on the ARMv7 (32-bit) architecture and had been expanding its coverage. One of the recent milestones, announced at Proofcraft's five-year mark, was that seL4's proofs came to cover 100% of the ARM platforms on which the kernel runs, allowing users to freely choose an ARM platform knowing they are on a verified foundation. This effort is part of DARPA's PROVERS program.

AArch64 is the architecture behind practically everything modern and embedded: phone SoCs, IoT gateways, automotive control units, edge devices. Having the complete security proof stack on 64-bit ARM means that those who design these systems now have a kernel option with a formal guarantee of isolation on the architecture they already use in practice, without having to fall back on the older ARMv7.

The advances that came along with it

The previous months show an active roadmap beyond confidentiality:

• MCS verified on RISC-V (June 2026): the mixed-criticality systems (MCS) configuration, seL4's biggest new feature, had its functional correctness proven for the first time, targeting RISC-V. MCS is essential for real-time applications with mixed criticality, such as automotive use cases, and the proof is also being ported to 64-bit ARM as part of DARPA's PROVERS program.
• Dynamic domain scheduler (June 2026): previously, the information-flow proof required fully static scheduling, compiled into the kernel, which forced developers to fix each domain's time slice in advance for the entire life of the system. The new API allows semi-static scheduling: a system with information-flow protection can have a boot phase with larger time slices (so VMs can come up without running out of allocated time) and an operational phase with smaller slices for greater responsiveness. This is already implemented, verified and available in seL4 15.0.0, and it makes it easier to use SDK-style tools such as Microkit.
• Static multikernel: Proofcraft has been extending the proofs to a multikernel configuration, in which each CPU core runs a separate instance of seL4, allowing performance gains from multiple cores without giving up kernel-level guarantees.

What changes for those building in Brazil

For the Brazilian developer working with embedded systems, IoT or critical infrastructure, the practical takeaway is that there is now a kernel with a mathematical guarantee of isolation ready for the 64-bit ARM architecture that dominates the hardware market. In sectors such as automotive, medical devices, defense and industrial systems, where an isolation failure can have physical consequences, this foundation changes the security argument: instead of "we tested it extensively," it becomes possible to say "there is proof that non-critical applications cannot compromise critical ones."

seL4 is open source and maintained by the seL4 Foundation, so there is no license barrier to experimenting with it. To truly adopt it, however, the system needs to be architected around the kernel's capability model and the ecosystem's tools (such as Microkit), which requires a learning investment. The formal guarantees also only hold within the stated assumptions, a point any team needs to understand before using the proof as a compliance argument.

What is still open

Some efforts are still ongoing and worth watching: porting MCS from RISC-V to 64-bit ARM, the evolution of the multikernel configuration, and the maturing of the dynamic scheduling APIs. Proofcraft runs three major projects in parallel, funded by DARPA, Germany's Cyberagentur, and the UK's NCSC. The seL4 summit 2026 takes place in Vancouver, September 1-3, and is usually where the next steps of the roadmap appear.