I thought commingling classification/user clearance levels on the same hardware fell out of favor a while ago, because of side channels (with speculative execution being the final nail in the coffin.)

Isn't seL4 more used for things like data diodes, cryptographic equipment and military hardware? Stuff that you need to keep from getting hacked or malfunctioning, but not time-shared with untrusted users.

Nah, multilevel security fell out of favor because no large commercial vendor could do it. They retracted the requirements over a decade ago because it prevented Microsoft and IBM from bidding on government contracts to “secure” their infrastructure.

Well, Microsoft made some half-assed runs at Orange Book compliance (e.g. Windows NT without floppies/CDs...or networking), but Trusted AIX was a real thing with real users. Having been involved in a couple of MLS Unix implementations, IMO it didn't fall out of favour because no vendor could do it, it fell out of favour because no one could effectively run it in production. The admin overhead of a 'real' TCSEC validate system is formidable, and at some point someone decided 'useable with admins with 6 months of training (e.g. privates and corporals)' was more important than 'checks all the boxes', and the boxes that needed to be checked changed.