Describir: seL4: Formal Verification of an Operating-System Kernel.