I mean, LionOS appears to (with the exception of sel4 itself) be mainly written in unverified C without heavy static analysis. So LionOS and Genode appear to b

I mean, LionOS appears to (with the exception of sel4 itself) be mainly written in unverified C without heavy static analysis. So LionOS and Genode appear to be about equal in that regard.