On 7 Sep 2019, at 13:32, Gergely Buday <gbuday@gmail.commailto:gbuday@gmail.com> wrote:

how does Muen relate to seL4?

https://muen.codelabs.ch/

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