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.
POSIX compatibility makes software porting and development easy. The project features distributions ready for download and use for all the available architectures and boards, the most prominent FOSS one is Gloire .
Ported to several platforms and boards, and designed to be easily portable to many more. Dependency on only the GNU toolchain allows for easy cross-compilation.
SPARK 's state of the art formal verification is employed for ensuring absence of errors and correctness of huge swathes of Ironclad, like cryptography, MAC , and user-facing facilities.
Ironclad is fully open source and distributed under the GPLv3 , ensuring it remains free. No firmware blobs are needed or shipped with the kernel. Every piece of the stack is open source.
Ironclad will always be free for use, study, and modification , so, to support the project, we rely on the use of donations and grants. Every contribution makes a difference and allows us to do more.
Thanks to
This project is funded through NGI Zero Core, a fund established by NLnet with financial support from the European Commission's Next Generation Internet program. Learn more at the NLnet project page.
Additionally, we would like to thank the following organizations: