Formally verified Unix-y kernel written in Ada is /not/ something I had on my Bingo card.
“Ironclad OS crafts Unix-like kernel in Ada and SPARK”
https://www.theregister.com/2025/11/10/ironclad_os_unix_like_kernel/
Formally verified Unix-y kernel written in Ada is /not/ something I had on my Bingo card.
“Ironclad OS crafts Unix-like kernel in Ada and SPARK”
https://www.theregister.com/2025/11/10/ironclad_os_unix_like_kernel/
@justkwin Interesting! And it's #GPL licenced and #EU funded, both of which make it even more interesting. #IroncladOS
More details here: https://ironclad-os.org/
There's even a full distro, #Gloire, with the GNU userspace stack, available here:
https://codeberg.org/Ironclad/Gloire
I'm very tempted to give it a try!