seL4 Project Roadmap
The seL4 project roadmap lists larger planned contributions to the seL4 ecosystem, such as new architecture ports, new large formal verifications, large or fundamental new features, user-level frameworks, or components with general interest to the community.
The purpose is to provide a timeline to the community of when larger contributions will become available with a reasonable level of commitment, and for contributors to advertise to others which larger contributions they are working on.
Features that are in progress are currently being worked on, features that are planned have not yet had work started on them.
To put a feature on the roadmap, the respective contributor will have made a commitment to delivering it, but these are not contracts — any dates are indicative and subject to change!
Some features may become available in experimental preview branches before they are merged into the master branch. The dates in the table are for the completion of the feature in master. The preview branches may undergo significant changes before they are merged and may also be abandoned. Some of these branches may be long-lived, because features can only be merged into master when they are either formally verified or do not affect the verified configurations of the kernel. Typically, while a larger feature undergoes formal verification, it will be available in a branch or a non-verified configuration. Such features often undergo smaller API-level changes while the verification progresses and either finds flaws or otherwise influences the design.
In many cases, the roadmap could be accelerated with more funding for the contributors who work on them, or, in some cases, by volunteering time. If you are interested, talk to the seL4 Foundation or directly to foundation members, e.g. when it involves formal verification to Proofcraft or for major seL4 kernel features to the Trustworthy Systems group.
seL4 Development
| Feature | Description | Assigned | Status |
|---|---|---|---|
| MCS Kernel extensions | A new scheduling model to support trustworthy mixed-criticality real-time systems. | UNSW | In progress. Main API stable and available. Note: smaller API changes while verification is in progress. |
| seL4 Microkit | A simple operating systems framework for building systems on seL4. | UNSW | Ongoing research & development. Available for use. Detailed roadmap available here. |
| seL4 Device Driver Framework | A high-performance and secure driver framework for seL4. | UNSW | Ongoing research & development. Available for use. Find out more here. |
| LionsOS | A secure, fast, and adaptable OS based on the seL4 Microkit. | UNSW | Ongoing research & development. An initial release containing a non-trivial example system has been made. Find out more here. |
Verification
| Feature | Description | Assigned | Status |
|---|---|---|---|
| MCS Kernel extensions | Functional correctness proofs for a new scheduling model to support trustworthy mixed-criticality real-time systems. | Proofcraft | C verification ongoing |
| AArch64 port | Functional correctness proofs for the AArch64 port of seL4 completed. Integrity (access control) ongoing. | Proofcraft | Integrity verification to complete Q1/25 |
Adding to the Roadmap
The roadmap is not only for seL4 kernel development or verification itself. If you are working on a larger feature or addition to the the wider seL4 ecosystem, and are confident enough to commit to a timeline, you can request this plan to be added to the roadmap on this page.
If you are contracted to deliver a major user-level component, framework, or feature in the seL4 ecosystem with a delivery date, and ideally an approved RFC to go with it, your contribution would be an ideal addition to the roadmap.
A new feature can become a part of the official seL4 roadmap by decision of the Technical Steering Committee (TSC) of the seL4 Foundation. To submit a request to the TSC for putting a planned feature on the roadmap, send an email to any TSC member with a description of the contribution, the planned timeline, and level of confidence for achieving it, e.g. by pointing to any related RFC. The TSC will discuss the proposal and either request more information or vote on it.