HNHacker News
TopNewBestAskShowJobs

azoriousrange

12 karma · joined January 8, 2024

submissionscomments
azoriousrange··on Ironclad: A formally verified, hard real-time capable kernel in Ada
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.

azoriousrange··on 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