[el_pollo_diablo]

> seL4 is the only microkernel that has a proof of correctness

ProvenCore (https://provenrun.com/provencore/) has a proof that covers correctness (memory safety, and more generally absence of UB, termination, etc.), functional properties (e.g. the fork() system call is a refinement of an abstract "clone" operation of abstract machines), and security properties (memory isolation).