seL4 Home

Development Roadmap

seL4's leading position keeps solidifying through an active, public development community roadmap, both on the Systems side and the Verification side. You can help accelerate or contribute to this roadmap.

Roadmap markers on an abstract path with a blue background

Systems Roadmap

On the Systems side, the roadmap includes further development for the kernel itself, as well as updates to the expanding ecosystem of frameworks, tools, components, and languages.

  • seL4 Microkit:
    A simple operating systems framework for building systems on seL4.
    By UNSW
    Ongoing research & development. Available for use. Detailed roadmap available here.
  • seL4 Device Driver Framework (SDDF):
    A high-performance and secure driver framework for seL4.
    By UNSW
    Ongoing research & development. Available for use. Find out more here.
  • LionsOS:
    A secure, fast, and adaptable OS based on the seL4 Microkit.
    By UNSW
    Ongoing research & development. An initial release containing a non-trivial example system has been made. Find out more here.

Verification Roadmap

On the Verification side, the roadmap includes further extensions of the seL4's formal proofs.

  • Verification of MCS Kernel extensions:
    Functional correctness proofs for a new scheduling model to support trustworthy mixed-criticality real-time systems.
    By Proofcraft
    C verification to complete Q3/27
  • Verification of AArch64 port:
    Functional correctness proofs for the AArch64 port of seL4 completed. Integrity (access control) ongoing.
    By Proofcraft
    Integrity verification to complete Q2/25
  • Automated Platform Port Verification:
    Reducing the need for verification experts for new platform ports and expanding the set of supported configuration parameters. Making the seL4 proofs applicable to a broader range of platforms and applications without the need for verification experts.
    By Proofcraft
    Increased platform support available. Further platform and configuration support ongoing. Project to complete Q3/27
  • Multikernel Verification:
    Specifications, verification tools, and proofs for the multi-kernel configuration of seL4. Providing gradually increasing assurance for multi-core seL4 systems as the verification progresses.
    By Proofcraft
    Project scheduled to complete Q3/28

How to Accelerate or Contribute

  • In some cases, the roadmap could be accelerated with more funding for the contributors who work on them, or by volunteering time. If you are interested, email us at foundation@sel4.systems.
  • If you are working on a larger feature or addition to the seL4 ecosystem, possibly contracted to deliver it, and ideally with an approved RFC to go with it, your contribution would be an ideal addition to the roadmap. If you would like to add to the roadmap, email us at foundation@sel4.systems.