Seeing the interest for OSes submitted recently with rust and safety as a main concern, what about this little formally verified Ada/SPARK kernel? It also has a distribution called Gloire at https://github.com/streaksu/Gloire