Vu à travers le Distrowatch weekly de cette semaine, il y a d'autres sources d'infos: le micro-kernel formellement vérifié et temps réel dur seL4 est devenu disponible sous GPLv2 il y a quelques jours à http://sel4.systems/
C'est un des descendants améliorés du L4 d'origine d'il y a 20 ans. Un de ses prédécesseurs est utilisé 24/7 comme RTOS dans les SoC modem GSM de Qualcomm, autrement dit dans quelques milliards de téléphones portables; on peut également l'utiliser comme hyperviseur, par exemple pour Linux.
La portabilité est limitée: x86 32 bits sur les PCs modernes, ARM sur plusieurs boards récentes. Pas de vérification formelle pour la version expérimentale multi-coeurs...

On verra ce qui se passe, mais le fait d'ouvrir le code a de grandes chances d'augmenter sa popularité et sa portabilité.