Потому что
1. seL4 верифицирована и настолько маленькая что. тысячи глаз могут ее просмотреть
2. в ней используются ну очень строгие параметры компиляции
   - Code should compile without warnings, with -Wall.
   - When using integral types (char, int, long, etc.), qualify them explicitly as unsigned except where negative values are meaningful and must be handled.
   - запрещены ++x и --y
   - используют automatic formatting of C code
Просто сравни это с распространеными опенсорс проектами.

И второе "потому что":
лицензия этого ядра позволяет использовать для "всего что не в нем" нормальные пермиссивные. И писать на любом языке который можно с Си соединить.
А это немаловажный плюс - твой код не заражается раковой ГПЛей.

И третье, последнее но немаловажное:
ГНУтики поработали - чего их трудом не воспользоваться)