SeL4 security proofs now complete on AArch64
Proofcraft News Archive: 2026
Exploring the frontier of formal verification and secure systems.
Navigation: [2026] | [2025] | [2024] | [2023] | [2022] | [2021]
🛡️ AArch64 Security Proofs Reach Completion
Date: 21 August 2026
Proofcraft has announced a landmark achievement: the completion of the confidentiality proof for seL4 on the AArch64 architecture. This follows the previous successful proofs regarding integrity and functional correctness.
Mathematically, this ensures that the kernel strictly prohibits any application from accessing unauthorized information. With the ongoing backing of the NCSC, this milestone solidifies the formal evidence that the AArch64 implementation of seL4 maintains rigorous security isolation.
The Core Benefit: This isolation ensures that a breach in a non-critical application cannot leak into or compromise a critical system component.
Verification Status Table
| Proof Layer | Status | Objective |
|---|---|---|
| Functional Correctness | ✅ | Code matches specification |
| Integrity | ✅ | No unauthorized writes |
| Confidentiality | ✅ | No unauthorized reads |
🎓 Theoretical Advances at LICS'26
Date: 24 July 2026
The paper titled "The Algebra of Iterative Constructions" was presented at the 41st Annual Symposium on Logic in Computer Science (LICS) in Lisbon.
Authorship:
- Kevin Batz
- Benjamin Lucien Kaminski
- Lucas Kehrer
- Gerwin Klein
- Henning Urbat
- Todd Schmid
The research focuses on an algebraic framework for reasoning about the iterative creation of fixed points. In computer science, fixed points are fundamental, as seen in the :
By utilizing this algebra, complex theorems can be expressed more concisely. This is particularly useful for implementation in Isabelle/HOL—the proof assistant Proofcraft employs for the seL4 microkernel. This work grew from a 2025 collaboration in Athens between Chief Scientist Gerwin Klein and Benjamin Kaminski.
(* Conceptual representation of iterative construction *)
let rec iterate f x n =
if n = 0 then x else iterate f (f x) (n - 1)
🚀 RISC-V Milestone: MCS Verification
Proofcraft has hit a major target in the seL4 roadmap: the Mixed-Criticality Systems (MCS) configuration is now proven correct on RISC-V.
The MCS configuration is a massive addition to the kernel, essential for real-time environments like automotive systems. Because it fundamentally alters the API and internal implementation, its verification was a high-priority, labor-intensive effort.
Roadmap Progress:
- Functional correctness for MCS on
RISC-V - Porting functional correctness to
Arm 64-bit(via DARPA's PROVERS program)
⏱️ Introducing the Dynamic Domain Scheduler
Date: 1 June 2026
Proofcraft has released a more versatile approach to domain scheduling within seL4.
Old Method: Fully static schedules compiled into the kernel.
New Method: Semi-static domain schedules loaded via a new runtime API.
Previously, developers had to assign a rigid, unchanging time slice to every domain for the system's entire duration. This was impractical for SDK-based development (e.g., Microkit). The new API allows the system to transition through different operational phases:
This updated API is fully verified and integrated into seL4 15.0.0.
🎤 Public Engagements & Partnerships
CDIS Spring Conference (Stockholm)
Date: 21 May 2026 At the KTH Royal Institute of Technology, CEO June Andronick delivered a keynote alongside August Martens (Mistral AI). The discussion centered on:
- The role of formal verification in modern cybersecurity.
- A panel discussion regarding Digital Sovereignty.
Cyberagentur Milestone Research Summit
Date: 28 April 2026 Proofcraft participated in the ÖvIT (Ecosystem trustworthy IT) program summit, partnering with Kry10.
Chief Scientist Gerwin Klein and Martin Dehnel-Wild presented the Dyvercon project, which aims to bring performance and proof to complex cyber-physical systems. A key highlight was the extension of seL4 proofs to support a static multikernel configuration:
- Architecture: Each CPU core runs its own separate instance of
seL4. - Benefit: Applications gain multi-core performance without sacrificing kernel-level isolation.
🤝 Community Support
Date: 17 April 2026 Proofcraft is proud to announce its role as a sponsor for the seL4 summit 2026.