seL4 is awesome for its formal engineering. One of the main gotchas though with purer (less hybrid) microkernel architectures is the coordination of transaction

seL4 is awesome for its formal engineering. One of the main gotchas though with purer (less hybrid) microkernel architectures is the coordination of transactions that touch multiple services, i.e., a system call or event that touches multiple hardware areas and must execute rollback code should any one of them fail.