Proofcraft achieved a significant milestone in the seL4 verification roadmap that was years in the making: the MCS configuration of seL4, providing support for mixed-criticality systems, is now proved to be correct on RISC-V.
This configuration is the largest new seL4 feature, indispensable for mixed criticality real-time applications such as automotive use cases. It contains wide-ranging changes to the kernel’s implementation and API. Its verification therefore required considerable effort and has been a priority in the seL4 roadmap for a long time.
Proofcraft has now completed, for the very first time, the verification of functional correctness for seL4 with MCS. Functional correctness is the largest and most central proof in the seL4 verification stack. The proof targets the RISC-V architecture and will now be ported to the Arm 64-bit architecture, as part of DARPA’s PROVERS program.
Proofcraft delivered the implementation and formal proof of more flexible domain scheduling in seL4.
Before the change, the seL4 security proofs, and in particular the proof of information flow enforcement, required a fully static schedule that was compiled into the kernel. This meant that, when using seL4 to enforce the information flow boundaries between applications, developers were required to provide a fixed predetermined amount of time for each domain, for the entire lifetime of the running system. This strict policy made it hard to apply information flow control in practice and to support in SDK-style development such as the Microkit.
Proofcraft proposed a new seL4 runtime API (Application Programming Interface) allowing the loading of semi-static domain schedules. This means that a system with information flow protection can go through different phases at runtime that can satisfy different domain timing requirements. For instance, a boot phase of the system can have longer time slices to allow virtual machines to start without overrunning their domain time allocation, and an operational phase of the system can provide shorter time slices so that each domain can be responsive to outside interaction. Additionally, an SDK-based system such as the Microkit 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.
On May 21st 2026, CDIS – Swedish research Center for Cyber Defense and Information Security – held its spring conference at KTH Royal Institute of Technology in Stockholm.
Proofcraft CEO June Andronick was one of the two keynote speakers, alongside August Martens from Mistral AI. June gave an overview of formal verification for cybersecurity, and participated in a panel on Digital Sovereignty.
In April 2026, Germany’s Cyberagentur held a Milestone Research summit to present the progress and outcomes of its funded programs, including the Ecosystem trustworthy IT research program (ÖvIT), which Proofcraft is a recipient of, partnering with Kry10.
Proofcraft’s Chief Scientist Gerwin and Kry10’s Chief Scientist Martin Dehnel-Wild presented the progress on the Dyvercon project, to deliver dynamism, performance, and proof for complex cyber-physical systems. In particular, Gerwin reported on Proofcraft’s work on extending the seL4 proofs to support a static multikernel configuration, where applications can benefit from the use of multiple CPU cores for performance, while at the kernel level a separate instance of seL4 run on each core.
Gerwin additionally gave a general introduction to formal verification and overview of its use in the real world.
Proofcraft is happy to be supporting the 2026 seL4 summit as a Silver sponsor.
The seL4 summit is an annual international gathering of participants from industry, government and universities with interests in the world’s most highly assured OS kernel. Attendees and presenters include the creators and maintainers of the seL4 technology such as the Proofcraft team.
This year’s seL4 summit will be held in Vancouver, Canada, on Sep 1-3, 2026.