I will start of briefly summarising the concept of a microkernel, and the core principles which characterise the L4 microkernel family. I will then introduce the core concepts of seL4, and what distinguishes it functionally from other L4 kernels.

What makes seL4 really special is its formal verification. I will explain what this is, and what exactly we have proved about seL4, and discuss what this means in practice, especially as far as security, safety and reliability are concerned. I will also indicate where we are planning to take seL4, i.e. a high-level summary of our on-going research and development projects.

Having covered the technical aspects, I will discuss the development process of the seL4 ecosystem, both past and present. I will specifically discuss the licensing status of various bits of this ecosystem, and how it is likely to develop. In particular I will indicate suggest the best way for the community to contribute to this ecosystem, and help develop it to the benefit of us all.

NOTE: Lecture will be provided via Skype