LionsOS is currently undergoing active research and development, it does not have a concrete verification story yet. It is not expected for LionsOS to be stable at this time, but it is available for others to experiment with.
LionsOS is an operating system based on the seL4 microkernel with the goal of making the achievements of seL4 accessible. That is, to provide performance, security, and reliability.
LionsOS is being developed by the Trustworthy Systems research group at UNSW Sydney in Australia.
It is not a conventional operating system, but contains composable components for creating custom operating systems that are specific to a particular task. Components are joined together using the Microkit tool.
The principles on which a LionsOS system is built are laid out fully in the sDDF design document; but in brief they are:
Components are connected by lock-free queues using an efficient model-checked signalling mechanism.
As far as is practical, operating systems components do a single thing. Drivers for instance exist solely to convert between a hardware interface and a set of queues to talk to the rest of the system.
Components called virtualisers handle multiplexing and control, and conversion between virtual and IO addresses for drivers.
Information is shared only where necessary, via the queues, or via published information pages.
The system is static: it does not adapt to changing hardware, and does not load components at runtime. There is a mechanism for swapping components of the same type at runtime, to implement policy changes, or to reboot a virtual machine with a new Linux kernel.
To be successful, many more components are needed. Pull requests to the various repositories are welcome. See the page on contributing for more details.