Ironclad: A formally verified, hard real-time capable kernel in Ada

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

Would be very interesting so see how it compares against RTEMS.

From my basic understanding of RTEMS, they are similar on the surface, but Ironclad has a wholly different set of aims.

While RTEMS aims to provide an extremely lightweight and easily embeddedable system (and thus it forgoes things like per-process address spaces, which increase footprint and needed hardware), Ironclad puts a really strong focus on security, with things like mandatory access control, full user support, capabilities, and other goodies, sometimes at the expense of those things. Its more of a QNX and RTLinux than an RTEMS.

I hope this OS becomes main stream