Ironclad – formally verified, real-time capable, Unix-like OS kernel
14 days ago
- #formal-verification
- #operating-system
- #open-source
- Ironclad is a formally verified, UNIX-like OS kernel for general-purpose and embedded uses.
- Written in SPARK and Ada, it is 100% free software with a POSIX-compatible interface.
- Features include preemptive multitasking, Mandatory Access Control (MAC), and hard real-time scheduling.
- Fully open source under GPLv3, with no firmware blobs required.
- Uses SPARK's formal verification for error-free cryptography, MAC, and user-facing facilities.
- Portable to multiple platforms, with easy cross-compilation via GNU toolchain.
- Relies on donations and grants, funded by NGI Zero Core and supported by NLnet and the European Commission.