seL4 is really cool; I was just looking at and the other L4 family / derivatives for µkernel ideas and trends. More links: - https://en.wikipedia.org/wiki/L4

seL4 is really cool; I was just looking at and the other L4 family / derivatives for µkernel ideas and trends. More links: - https://en.wikipedia.org/wiki/L4_microkernel_family#High_assurance:_seL4 https://en.wikipedia.org/wiki/L4_microkernel_family#High_ass... - seL4: Formal Verification of an OS Kernel (2009) [pdf paper] http://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf http://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf - l4v (seL4 proofs git repo) https://github.com/seL4/l4v https://github.com/seL4/l4v