Ironclad OS project popping out Unix-like kernel in a unique mix of languages
(2025/11/10)
- Reference: 1762794909
- News link: https://www.theregister.co.uk/2025/11/10/ironclad_os_unix_like_kernel/
- Source link:
If you're looking for a Unix-like, POSIX-compatible, real-time kernel, there's no shortage of projects trying to build one. Ironclad stands out for using the Ada programming language and its formally verifiable SPARK subset.
The [1]Ironclad OS project is writing a new Unix-like OS kernel, aimed at small-footprint and embedded systems, and planning to be realtime-capable. For stronger security, it supports Mandatory Access Control (MAC), which is a [2]big-organization style sort of system, as the US National Institute of Standards and Technology [3]describes .
There are quite a few such projects out there. When we searched GitHub for a [4]Unix-like kernel we got 222 results across 23 pages. What is a little different about Ironclad is that it's not in C, nor in C++ [5]like Serenity OS , nor in Rust [6]like Redox OS . It's not even in one of the other modern C-like languages, such as Drew DeVault's project in his [7]Hare language , which he calls [8]Bunnix .
[9]
Instead, Ironclad is built in the granddaddy of safe systems-programming languages, Ada, and its design-by-contract dialect SPARK, at which The Register [10]took a look back in 2006 . The team is working on formal verification for the Ironclad kernel, although this isn't complete yet. The only other formally verified kernel we're aware of is the [11]seL4 microkernel , as The Reg [12]covered in 2014 , so that would be quite a coup.
[13]
[14]
Because just a kernel isn't much use or very interesting on its own, the project has also got a more complete OS that runs on top of the Ironclad kernel, called [15]Gloire , after France's pioneering ocean-going ironclad of 1859. Gloire is built using GNU tools, which means more traditional Unix compatibility – to the extent that the team is [16]porting the MATE desktop to Gloire . Gloire's C standard library, [17]mlibc , comes from the [18]Managarm project that we [19]described back in September .
[20]52-year-old data tape could contain only known copy of UNIX V4
[21]The elusive goal of Unix – or Linux – simplicity
[22]The Unix Epochalypse might be sooner than you think
[23]Beta of Unix version 2 restored to life
Possibly thanks to riding on Rust's coat-tails, Ada seems to have been getting more attention recently. Earlier this year, [24]AdaCore excitedly reported that it was back in the TIOBE top 20, and it [25]still is as we write. As we [26]mentioned back in 2023 , we ascribe some of this to there being a FOSS toolchain: the [27]GNU Ada compiler GNAT .
Although the [28]late great Niklaus "Bucky" Wirth wasn't directly involved, Ada's syntax – and its strong typing - are visibly inspired by Pascal. It's very different from the C family of languages, but it's not the first Unix-like OS to be written in a Pascal-family language.
Back in the early 1980s, there was a profusion of such projects. The University of Toronto developed [29]TUNIS in [30]Concurrent Euclid , but there have been several others besides. Apollo's AEGIS OS was implemented in Pascal; in 1988, Apollo added both System V and BSD UNIX compatibility environments and renamed it Domain/OS. The company was later purchased by Hewlett-Packard. [31]Elxsi 's proprietary workstations ran EMBOS, a very early microkernel-style design implemented in Pascal. An [32]offshoot is still trading, but core Elxsi people went on to work to invent digital certificates, work on Internet Explorer and the Intel Itanium, and found the NexGen that was [33]later acquired by AMD . DEC's experimental [34]Topaz microkernel [PDF] was written in Modula-2+, and the University of Washington's [35]SPIN operating system in Modula-3. The [36]original Chorus microkernel OS [PDF] from INRIA was first developed in Pascal. Chorus later ended up at Oracle and [37]went open source , and its kernel was used in Sun's [38]long canceled JavaOS .
[39]
In other words, there's a surprisingly long history of using Pascal and Pascal-like languages in Unix-like OSes, especially in microkernels – Chorus even predates Mach, now the basis of Apple's macOS. Ironclad development only reaches back to 2022, but although it sounds surprising and unexpected, Ironclad is just the newest entry in a long and varied tradition. ®
Get our [40]Tech Resources
[1] https://ironclad-os.org/
[2] https://www.theregister.com/2006/04/27/linux_mac_pilot/
[3] https://csrc.nist.gov/glossary/term/mandatory_access_control
[4] https://github.com/search?q=unix+like+kernel&type=repositories
[5] https://www.theregister.com/2022/03/31/serenityos/
[6] https://www.theregister.com/2022/11/29/redox_os_version_08/
[7] https://harelang.org/
[8] https://drewdevault.com/2024/05/24/2024-05-24-Bunnix.html
[9] https://pubads.g.doubleclick.net/gampad/jump?co=1&iu=/6978/reg_software/oses&sz=300x50%7C300x100%7C300x250%7C300x251%7C300x252%7C300x600%7C300x601&tile=2&c=2aRJuh1MPZ8BoBRDdM-uL7wAAAQk&t=ct%3Dns%26unitnum%3D2%26raptor%3Dcondor%26pos%3Dtop%26test%3D0
[10] https://www.theregister.com/2006/09/20/high_integrity_software/
[11] https://sel4.systems/
[12] https://www.theregister.com/2014/07/28/aussie_droneprotecting_hackerdetecting_kernel_goes_open_source/
[13] https://pubads.g.doubleclick.net/gampad/jump?co=1&iu=/6978/reg_software/oses&sz=300x50%7C300x100%7C300x250%7C300x251%7C300x252%7C300x600%7C300x601&tile=4&c=44aRJuh1MPZ8BoBRDdM-uL7wAAAQk&t=ct%3Dns%26unitnum%3D4%26raptor%3Dfalcon%26pos%3Dmid%26test%3D0
[14] https://pubads.g.doubleclick.net/gampad/jump?co=1&iu=/6978/reg_software/oses&sz=300x50%7C300x100%7C300x250%7C300x251%7C300x252%7C300x600%7C300x601&tile=3&c=33aRJuh1MPZ8BoBRDdM-uL7wAAAQk&t=ct%3Dns%26unitnum%3D3%26raptor%3Deagle%26pos%3Dmid%26test%3D0
[15] https://codeberg.org/Ironclad/Gloire
[16] https://blog.ironclad-os.org/adding-modern-desktop-environment-options-to-gloire/
[17] https://github.com/managarm/mlibc
[18] https://managarm.org/
[19] https://www.theregister.com/2025/09/12/three_new_microkernels/
[20] https://www.theregister.com/2025/11/07/unix_fourth_edition_tape_rediscovered/
[21] https://www.theregister.com/2025/05/27/elusive_goal_of_simplicity/
[22] https://www.theregister.com/2025/08/23/the_unix_epochalypse_might_be/
[23] https://www.theregister.com/2025/02/24/beta_unix_2_restored/
[24] https://blog.adacore.com/ada-is-back-in-the-tiobe-index-top-20
[25] https://www.tiobe.com/tiobe-index/
[26] https://www.theregister.com/2023/03/28/nostalgic_for_basic/
[27] https://www.theregister.com/2023/03/28/nostalgic_for_basic/
[28] https://www.theregister.com/2024/01/04/niklaus_wirth_obituary/
[29] https://en.wikipedia.org/wiki/TUNIS
[30] https://en.wikipedia.org/wiki/Concurrent_Euclid
[31] https://en.wikipedia.org/wiki/Elxsi
[32] https://www.tataelxsi.com/
[33] https://www.theregister.com/2000/08/08/intel_engineers_amds_success_dham/
[34] https://www.mcjones.org/paul/wwospos.pdf
[35] https://www-spin.cs.washington.edu/
[36] https://ics.uci.edu/~cs230/reading/chorus.pdf
[37] https://docs.oracle.com/cd/E19048-01/chorus5/index.html
[38] https://www.theregister.com/1999/08/24/sun_ibm_pull_plugs/
[39] https://pubads.g.doubleclick.net/gampad/jump?co=1&iu=/6978/reg_software/oses&sz=300x50%7C300x100%7C300x250%7C300x251%7C300x252%7C300x600%7C300x601&tile=4&c=44aRJuh1MPZ8BoBRDdM-uL7wAAAQk&t=ct%3Dns%26unitnum%3D4%26raptor%3Dfalcon%26pos%3Dmid%26test%3D0
[40] https://whitepapers.theregister.com/
The [1]Ironclad OS project is writing a new Unix-like OS kernel, aimed at small-footprint and embedded systems, and planning to be realtime-capable. For stronger security, it supports Mandatory Access Control (MAC), which is a [2]big-organization style sort of system, as the US National Institute of Standards and Technology [3]describes .
There are quite a few such projects out there. When we searched GitHub for a [4]Unix-like kernel we got 222 results across 23 pages. What is a little different about Ironclad is that it's not in C, nor in C++ [5]like Serenity OS , nor in Rust [6]like Redox OS . It's not even in one of the other modern C-like languages, such as Drew DeVault's project in his [7]Hare language , which he calls [8]Bunnix .
[9]
Instead, Ironclad is built in the granddaddy of safe systems-programming languages, Ada, and its design-by-contract dialect SPARK, at which The Register [10]took a look back in 2006 . The team is working on formal verification for the Ironclad kernel, although this isn't complete yet. The only other formally verified kernel we're aware of is the [11]seL4 microkernel , as The Reg [12]covered in 2014 , so that would be quite a coup.
[13]
[14]
Because just a kernel isn't much use or very interesting on its own, the project has also got a more complete OS that runs on top of the Ironclad kernel, called [15]Gloire , after France's pioneering ocean-going ironclad of 1859. Gloire is built using GNU tools, which means more traditional Unix compatibility – to the extent that the team is [16]porting the MATE desktop to Gloire . Gloire's C standard library, [17]mlibc , comes from the [18]Managarm project that we [19]described back in September .
[20]52-year-old data tape could contain only known copy of UNIX V4
[21]The elusive goal of Unix – or Linux – simplicity
[22]The Unix Epochalypse might be sooner than you think
[23]Beta of Unix version 2 restored to life
Possibly thanks to riding on Rust's coat-tails, Ada seems to have been getting more attention recently. Earlier this year, [24]AdaCore excitedly reported that it was back in the TIOBE top 20, and it [25]still is as we write. As we [26]mentioned back in 2023 , we ascribe some of this to there being a FOSS toolchain: the [27]GNU Ada compiler GNAT .
Although the [28]late great Niklaus "Bucky" Wirth wasn't directly involved, Ada's syntax – and its strong typing - are visibly inspired by Pascal. It's very different from the C family of languages, but it's not the first Unix-like OS to be written in a Pascal-family language.
Back in the early 1980s, there was a profusion of such projects. The University of Toronto developed [29]TUNIS in [30]Concurrent Euclid , but there have been several others besides. Apollo's AEGIS OS was implemented in Pascal; in 1988, Apollo added both System V and BSD UNIX compatibility environments and renamed it Domain/OS. The company was later purchased by Hewlett-Packard. [31]Elxsi 's proprietary workstations ran EMBOS, a very early microkernel-style design implemented in Pascal. An [32]offshoot is still trading, but core Elxsi people went on to work to invent digital certificates, work on Internet Explorer and the Intel Itanium, and found the NexGen that was [33]later acquired by AMD . DEC's experimental [34]Topaz microkernel [PDF] was written in Modula-2+, and the University of Washington's [35]SPIN operating system in Modula-3. The [36]original Chorus microkernel OS [PDF] from INRIA was first developed in Pascal. Chorus later ended up at Oracle and [37]went open source , and its kernel was used in Sun's [38]long canceled JavaOS .
[39]
In other words, there's a surprisingly long history of using Pascal and Pascal-like languages in Unix-like OSes, especially in microkernels – Chorus even predates Mach, now the basis of Apple's macOS. Ironclad development only reaches back to 2022, but although it sounds surprising and unexpected, Ironclad is just the newest entry in a long and varied tradition. ®
Get our [40]Tech Resources
[1] https://ironclad-os.org/
[2] https://www.theregister.com/2006/04/27/linux_mac_pilot/
[3] https://csrc.nist.gov/glossary/term/mandatory_access_control
[4] https://github.com/search?q=unix+like+kernel&type=repositories
[5] https://www.theregister.com/2022/03/31/serenityos/
[6] https://www.theregister.com/2022/11/29/redox_os_version_08/
[7] https://harelang.org/
[8] https://drewdevault.com/2024/05/24/2024-05-24-Bunnix.html
[9] https://pubads.g.doubleclick.net/gampad/jump?co=1&iu=/6978/reg_software/oses&sz=300x50%7C300x100%7C300x250%7C300x251%7C300x252%7C300x600%7C300x601&tile=2&c=2aRJuh1MPZ8BoBRDdM-uL7wAAAQk&t=ct%3Dns%26unitnum%3D2%26raptor%3Dcondor%26pos%3Dtop%26test%3D0
[10] https://www.theregister.com/2006/09/20/high_integrity_software/
[11] https://sel4.systems/
[12] https://www.theregister.com/2014/07/28/aussie_droneprotecting_hackerdetecting_kernel_goes_open_source/
[13] https://pubads.g.doubleclick.net/gampad/jump?co=1&iu=/6978/reg_software/oses&sz=300x50%7C300x100%7C300x250%7C300x251%7C300x252%7C300x600%7C300x601&tile=4&c=44aRJuh1MPZ8BoBRDdM-uL7wAAAQk&t=ct%3Dns%26unitnum%3D4%26raptor%3Dfalcon%26pos%3Dmid%26test%3D0
[14] https://pubads.g.doubleclick.net/gampad/jump?co=1&iu=/6978/reg_software/oses&sz=300x50%7C300x100%7C300x250%7C300x251%7C300x252%7C300x600%7C300x601&tile=3&c=33aRJuh1MPZ8BoBRDdM-uL7wAAAQk&t=ct%3Dns%26unitnum%3D3%26raptor%3Deagle%26pos%3Dmid%26test%3D0
[15] https://codeberg.org/Ironclad/Gloire
[16] https://blog.ironclad-os.org/adding-modern-desktop-environment-options-to-gloire/
[17] https://github.com/managarm/mlibc
[18] https://managarm.org/
[19] https://www.theregister.com/2025/09/12/three_new_microkernels/
[20] https://www.theregister.com/2025/11/07/unix_fourth_edition_tape_rediscovered/
[21] https://www.theregister.com/2025/05/27/elusive_goal_of_simplicity/
[22] https://www.theregister.com/2025/08/23/the_unix_epochalypse_might_be/
[23] https://www.theregister.com/2025/02/24/beta_unix_2_restored/
[24] https://blog.adacore.com/ada-is-back-in-the-tiobe-index-top-20
[25] https://www.tiobe.com/tiobe-index/
[26] https://www.theregister.com/2023/03/28/nostalgic_for_basic/
[27] https://www.theregister.com/2023/03/28/nostalgic_for_basic/
[28] https://www.theregister.com/2024/01/04/niklaus_wirth_obituary/
[29] https://en.wikipedia.org/wiki/TUNIS
[30] https://en.wikipedia.org/wiki/Concurrent_Euclid
[31] https://en.wikipedia.org/wiki/Elxsi
[32] https://www.tataelxsi.com/
[33] https://www.theregister.com/2000/08/08/intel_engineers_amds_success_dham/
[34] https://www.mcjones.org/paul/wwospos.pdf
[35] https://www-spin.cs.washington.edu/
[36] https://ics.uci.edu/~cs230/reading/chorus.pdf
[37] https://docs.oracle.com/cd/E19048-01/chorus5/index.html
[38] https://www.theregister.com/1999/08/24/sun_ibm_pull_plugs/
[39] https://pubads.g.doubleclick.net/gampad/jump?co=1&iu=/6978/reg_software/oses&sz=300x50%7C300x100%7C300x250%7C300x251%7C300x252%7C300x600%7C300x601&tile=4&c=44aRJuh1MPZ8BoBRDdM-uL7wAAAQk&t=ct%3Dns%26unitnum%3D4%26raptor%3Dfalcon%26pos%3Dmid%26test%3D0
[40] https://whitepapers.theregister.com/
Re: Oh, goody! I can put Ada back on my resume.
Anonymous Coward
With Github telling us how Typescript is surging, because of how it's strong typing is better for AI, my first thought was: "Typescript good. Ada better"
I propose leaning into this with AI extensions and a new language AIDA.
(You may send grateful donations in the meme-coin of your choice)
PERQ / Accent / Mach
Alan J. Wylie
Back around 1980, I briefly evaluated an ICL PERQ workstation, running PNX (yes, really!). It could run several other operating systems, including Accent, which was a predecessor of Mach.
Wikipedia articles: [1]PERQ , [2]Accent
[1] https://en.wikipedia.org/wiki/PERQ
[2] https://en.wikipedia.org/wiki/Accent_kernel
Doctor Syntax
Not at all Unix-like but the UCSD pSystem (the original Apple Pascal) was written in Pascal. The OS, application and P-code interpreter all had to live in a small address space, enabling it to run on a 6502 or Z80. (As a L1 cache any self-respecting modern core would turn its nose up at the size of the memory available on the box I had it running on.)
Why does this
DS999
Read like a DoD project to me? Their home page doesn't look like it, but the implementation of MAC and especially use of Ada sure do!
Other than Apple using seL4 as the kernel in the Secure Element, is there any use of formal verification in any mass market products? Who will use this if the defense industry doesn't?
Oh, goody! I can put Ada back on my resume.
I think I remember intentionally removing it since it made me look old (which wasn't really necessary), and since hiring types would get a befuddled look on their faces when encountering that word.
Never really got to use Ada in a real production environment. Some difficult coding exercises around handling communication buffers, etc. Gov't mandated Ada for new IT projects but it really wasn't ready at the time. One fall-back was to use JOVIAL (which also doesn't show up on my resume.)