Dear Andrew You can find a lot of infomation about seL4 on the website ( https://sel4.systems/), especially the white paper. (Mathematically Verified Software Kernels: Raising the Bar for High Assurance Implementations) The seL4 came form NICTA and now it joins Data61, so you also find a lot of paper on the website. (https://ts.data61.csiro.au/projects/seL4/) For the formal verification, I think the following reference is useful. [1] http://proofcraft.org/blog/proof-engineer-reading.html [2] https://frap.csail.mit.edu/main In 21st, I think it exists three different design principles of kernel style. 1. monolithic kernel, e.g. Linux, FreeBSD 2. microkernel, e.g. seL4, more example : http://www.microkernel.info/ 3. unikernel, example: http://unikernel.org/projects/ Thanks Gapry 2016-08-22 4:16 GMT+08:00 Andrew Mine :

Hi

I have just started looking at seL4 and I was wondering where can I find some documentation explaining the features and difference between seL4 and other kernels. I have gone through the manual and tutorial documents but nothing majorly explains how seL4 is different and its features. Any guidance towards any documentation will be helpful.

Thanks Andrew

_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel