Ironclad is a formally verified, real-time capable, UNIX-like operating system kernel for general-purpose and embedded uses. It is written in SPARK and Ada, and is comprised of 100% free software.
OS built with the Ironclad kernel and using GNU tools for the userland, along with some original applications like util-ironclad. Gloire is capable of running Xorg-based desktop environments, games...