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.
Why Choose Ironclad?
Free as in freedom
Free as in freedom
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.
Formal verification
Formal verification
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.
Portable
Portable
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.
Distributions and ecosystemWho pays for Ironclad?
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.
About the Author
