Proofcraft News - 2026

Proofcraft News - 2026

News from other years:

2025

2024

2023

2022

2021

21 Aug 2026

seL4 security proofs now complete on AArch64

After completing the proofs of functional correctness and integrity,<br>Proofcraft has now established the proof that seL4 enforces confidentiality on<br>AArch64, providing a formal mathematical proof that the kernel prevents an<br>application running on top of seL4 from learning information without<br>authorisation.

Thanks to continued support from NCSC, this milestone completes the formal<br>proof that the seL4 implementation code on AArch64 enforces security isolation<br>of the applications running on top (under the assumptions listed here). This<br>isolation prevents attacks on non-critical applications from propagating to<br>critical applications and compromising them.

24 Jul 2026

Proof Engineering and Theory at LICS'26

The paper The Algebra of Iterative Constructions by Kevin Batz,<br>Benjamin Lucien Kaminski, Lucas Kehrer, Gerwin Klein, Henning Urbat, and Todd<br>Schmid was presented at the 41st Annual Symposium on Logic in Computer Science<br>(LICS) in Lisbon this week. This paper in theoretical computer science is<br>about an algebraic abstraction and reasoning principles for the iterative<br>construction of fixed points. Fixed points are a recurring theme in computer<br>science with many famous results such as the Kleene fixed point theorem. The<br>algebra shown in this paper allows expressing such theorems concisely and<br>enables reasoning about them in an abstract and streamlined way that can be<br>implemented efficiently in proof assistants such as Isabelle/HOL, which<br>Proofcraft is using for the verification of the seL4 microkernel.

The highly automated Isabelle/HOL implementation of iteration algebra in this<br>paper resulted from a spontaneous collaboration between Proofcraft&rsquo;s Chief<br>Scientist Gerwin Klein and Benjamin Kaminski that started at the IFIP Working<br>Group 2.3 (Programming Methodology) meeting in Athens in 2025. It shows that<br>proof engineering ranges from practical application all the way to deep theory.

29 Jun 2026

MCS seL4 now verified! (for RISC-V)

Proofcraft achieved a significant milestone in the seL4 verification roadmap<br>that was years in the making: the MCS configuration of seL4, providing support<br>for mixed-criticality systems, is now proved to be correct on RISC-V.

This configuration is the largest new seL4 feature, indispensable for mixed<br>criticality real-time applications such as automotive use cases. It contains<br>wide-ranging changes to the kernel&rsquo;s implementation and API. Its verification<br>therefore required considerable effort and has been a priority in the seL4<br>roadmap for a long time.

Proofcraft has now completed, for the very first time, the verification of<br>functional correctness for seL4 with MCS. Functional correctness is the largest and most central<br>proof in the seL4 verification stack. The proof targets the RISC-V architecture<br>and will now be ported to the Arm 64-bit architecture, as part of DARPA&rsquo;s PROVERS program.

1 Jun 2026

Dynamic Domain Scheduler for seL4

Proofcraft delivered the implementation and formal proof of more flexible<br>domain scheduling in seL4.

Before the change, the seL4 security proofs, and in particular the proof of<br>information flow enforcement, required a fully static schedule that was<br>compiled into the kernel. This meant that, when using seL4 to enforce the<br>information flow boundaries between applications, developers were required<br>to provide a fixed predetermined amount of time for each domain, for the<br>entire lifetime of the running system. This strict policy made it hard to apply<br>information flow control in practice and to support in SDK-style development such<br>as the Microkit.

Proofcraft proposed a new seL4 runtime API (Application Programming Interface)<br>allowing the loading of semi-static domain schedules. This means that a system<br>with information flow protection can go through different phases at runtime that<br>can satisfy different domain timing requirements. For instance, a boot phase of<br>the system can have longer time slices to allow virtual machines to start<br>without overrunning their domain time allocation, and an operational phase of<br>the system can provide shorter time slices so that each domain can be responsive<br>to outside interaction. Additionally, an SDK-based system such as the Microkit<br>can use the new API to set a domain schedule at boot time.

This new seL4 API is implemented, verified and available in seL4 15.0.0.

21 May 2026

June Andronick Keynote at CDIS Spring Conference in Stockholm

On May 21st 2026, CDIS – Swedish research Center for Cyber Defense and<br>Information Security – held its spring conference at KTH Royal Institute of<br>Technology in Stockholm.

Proofcraft CEO June Andronick was one of the two keynote speakers, alongside<br>August Martens from Mistral AI. June gave an overview of formal verification for<br>cybersecurity, and participated in a panel on Digital Sovereignty.

28 Apr...