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/

Ironclad OS project popping out Unix-like kernel in a unique mix of languages

: There's more to safer systems languages than Rust

The Register

@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!

Ironclad

Ironclad is a free software formally verified kernel written in SPARK/Ada