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.