｢ 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. Ironclad features a familiar POSIX-compatible interface, true simultaneous preemptive multitasking, Mandatory Access Control (MAC), and support for hard real-time scheduling ｣