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 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 big-organization style sort of system, as the US National Institute of Standards and Technology describes.

There are quite a few such projects out there. When we searched GitHub for a 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++ like Serenity OS, nor in Rust like Redox OS. It’s not even in one of the other modern C-like languages, such as Drew DeVault’s project in his Hare language, which he calls Bunnix.

Instead, Ironclad is built in the granddaddy of safe systems-programming languages, Ada, and its design-by-contract dialect SPARK, at which The Register 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 seL4 microkernel, as The Reg covered in 2014, so that would be quite a coup.

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 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 porting the MATE desktop to Gloire. Gloire’s C standard library, mlibc, comes from the Managarm project that we described back in September.

• 52-year-old data tape could contain only known copy of UNIX V4
• The elusive goal of Unix – or Linux – simplicity
• The Unix Epochalypse might be sooner than you think
• 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, AdaCore excitedly reported that it was back in the TIOBE top 20, and it still is as we write. As we mentioned back in 2023, we ascribe some of this to there being a FOSS toolchain: the GNU Ada compiler GNAT.

Although the 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 TUNIS in 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. Elxsi’s proprietary workstations ran EMBOS, a very early microkernel-style design implemented in Pascal. An 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 later acquired by AMD. DEC’s experimental Topaz microkernel [PDF] was written in Modula-2+, and the University of Washington’s SPIN operating system in Modula-3. The original Chorus microkernel OS [PDF] from INRIA was first developed in Pascal. Chorus later ended up at Oracle and went open source, and its kernel was used in Sun’s long canceled JavaOS.

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