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.