https://ironclad-os.org/

Ironclad
[documentat]Documentation[d]
User manual Formal verification Supported hardware Changelog
Trademark and logo use Code licensing
[community]Community[d]
Community channels Organisational structure Code of Conduct
[contributi]Contributing[d]
Contributing to Ironclad Report a bug[e] Report a security
vulnerability[e] Donate to the project
[languages]English
English Deutsch Espanol Francais Italiano Portugues
[blog]Blog[e] [repositori]Repositories[e]

The Ironclad Operating System Kernel

Ironclad is a (partially) 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.

Download a distribution Download an Ironclad tarball
[screenshot]

Why Choose Ironclad?

[fos]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.

[for]Formal verification

SPARK's state of the art formal verification is employed for ensuring
absence of errors and correctness of big portions of Ironclad, like
cryptography, MAC, and user-facing facilities.

[por]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.

[eco]Distributions and ecosystem

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.

Who 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.

Donate

Thanks to

NLNet

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:

AdaCore Limine Free Software Foundation
[ironclad]

Useful Links

Community User manual

Legal

Code licensing Trademark and logo use

Development

Project Organization Repository of this website

Copyright (c) 2025 The Ironclad Project. Made with [?] for seals and
good Ada code.