how does Muen relate to seL4?
e.g. it claims to be the first verified microkernel.
That has always been pretty dodgy marketing. It claims to be the first *open source* verified microkernel. The first part of which is technically true, since seL4 became open source slightly later, but seL4 was of course verified much before Muen. The
second part I would actually contest, because they themselves (correctly, as far as I can see ) call it a separation kernel in the rest of the docs, not a general-purpose microkernel. seL4 can be configured as a separation kernel, but that is just one of many
ways of using it.
Muen as far as I can tell doesn’t really compare in feature set or depth of verification. It shows absence runtime errors only, which 10 years ago would have been cool, but is a bit behind the times. seL4 had full functional correctness in 2009 already
(which includes absence of runtime errors), and by now also binary correctness, security theorems, etc.
Doesn’t mean it’s a bad project, It’s probably fine for the limited application area it is aimed at, but the verification is comparatively shallow.
Cheers,
Gerwin