Savannah site
Git development repository
Mailing lists

Development information
User support and bug reporting
Conduct and communication guidelines

Ironclad is a partially formally verified kernel with a small footprint for general-purpose and embedded OSes, written in SPARK and Ada. It is made to be 100% free software, free in the sense that it respects the user's freedom.

Some of the supported features are:


2023-Sep-1: New domain:

I've acquired, my intention with that domain is to use it as the main website of the project, with mirrors for the project's repos and other tools, and maybe a mail server, imitating

Those services will be rolled out slowly, as I am not the best with web stuff, I will learn that slowly, for now, it will be a redirect to with cool email stuff.

When linking people to the project, please use instead of from now on, thank you!

2023-Aug-31: Ironclad 0.4.0 released!

This release brings a lot of improvements on almost all subsystems of the kernel.

This is a non-exhaustive list of the big changes included in this release:

Tarballs for this release are available here:

Please contact me directly regarding questions or comments about this release at

All news

Further news can be read here.


Ironclad uses semantic versioning. Support thru major versions, porting bug fixes, will be done in a case-by-case basis time period, but for no shorter than 6 months since release.

All releases and their signatures can be found at the main repository. Here's a table of the latest releases:

Version Released End of life Downloads Documentation
0.4.0 2023-Aug-31 Not stable [.tar.gz] [.sig] [html] [pdf]
0.3.0 2023-Apr-02 Not stable [.tar.gz] [.sig]
0.2.0 2022-Nov-16 Not stable [.tar.gz] [.sig]

All releases are signed using PGP, please check the signatures before using the downloaded tarballs. The release keyring can be found here.

Who uses Ironclad?

Some distributions use Ironclad as its kernel, for example, visit Gloire, a general purpose desktop OS using Ironclad along GNU userland tools.

Thanks to

GNU Savannah Limine Free Software Foundation AdaCore Managarm