First off, congratulations on being the new primary microkernel of choice for the Genode Operating System Framework! I'm very excited.

Now to my questions - how does the formal verification of seL4 compare with the Integrity-178B security guarantees? Also, how do two structurally compare with each other in terms of design principles and implementation?