Commercial Support
The seL4 Foundation has endorsed several service providers to help with development with seL4. These providers have been recognised for their expertise in various seL4-related systems or verification areas. To receive an endorsement, providers must have one or more in-house experts who have already contributed in the area they are endorsed for.

DornerWorks Ltd
Innovative companies are building products on a trusted software base with the guidance of DornerWorks engineers. As a founding member of the seL4 Foundation, DornerWorks can accelerate the integration of seL4 as the trusted software base for your products.
DornerWorks Ltd is an Endorsed Service Provider for:
- systems: kernel platform port
- systems: user-level OS (VM)
- systems: application
Further details available on seL4 Microkernel Engineering Services.
Kry10 Limited
Kry10 offers support to enable seL4-based secure projects to be affordable, maintainable, and remotely manageable. Kry10 offers a full-featured operating system on top of the seL4 kernel, along with tooling, services, key management and more. The Kry10 Platform is a fast and easy way to build highly secure, next-generation cyber-physical devices. We leverage the verification of seL4 to bring you a secure, self-healing, truly dynamic system with minimal downtime, even during upgrades. Whether you are working on national assets, vehicles or sensors on a wall, you require deep confidence and easy to use tools. Come talk to us.
Kry10 is an Endorsed Service Provider for:
- systems: kernel
- systems: kernel platform port
- systems: user-level OS (Kry10 OS, CAmkES)
- systems: applications
- verification: kernel
- verification: user-level OS
- verification: applications
Proofcraft Pty Ltd
Proofcraft offers commercial support, verification projects, and consulting on formal verification in general, and involving seL4 specifically.
Formal verification is what makes seL4 unique. With increasing uptake and adoption, seL4 is evolving, supporting more platforms, architectures, configurations, and features. An increasing number of high assurance systems are built with seL4 as a trustworthy foundation.
As seL4 code evolves, so must its formal proofs. As more systems are built on seL4, there is an increased need to ensure correct configuration and initialisation, and correctness of critical components.
Founded by the seL4 verification leaders, Proofcraft is here to help. By applying mathematical machine-checked software verification, Proofcraft increases critical software systems' reliability, safety and security, for a verified future.
Proofcraft is an Endorsed Service Provider for:
- verification: kernel
- verification: user-level OS
- verification: applications
- systems: kernel
- systems: kernel platform port
For further information, visit Proofcraft or email contact@proofcraft.systems.
UNSW Sydney
The Trustworthy Systems (TS) team is the creator of seL4 and the seL4 Foundation, and for a long time was the sole source of support. With the seL4 Foundation now in place, and at its new home at UNSW, TS is now focusing on seL4-related research and driving development, leaving engineering mostly to other ecosystem players. However, TS is happy to take on research and consultancy contracts, as well as providing engineering (systems and verification) services when no commercial player is available.
Trustworthy Systems is an Endorsed Service provider for:
- systems: kernel
- systems: kernel platform port
- systems: user-level OS
- verification: user-level OS (microkit)
For more information, see services, Trustworthy Systems and UNSW.
If you are a member of the seL4 Foundation interested in being endorsed, check out the endorsement scheme.