Looking back on 10 years of the verified seL4 microkernel: https://microkerneldude.wordpress.com/2019/08/06/10-years-sel4-still-the-best-still-getting-better/ Includes some interesting design notes and comments on avoiding a kernel heap entirely.