7 ms·

Ironclad – formally verified, real-time capable, Unix-like OS kernel

375 points by vitalnodo 10mo ago

joshuakelly 10mo ago
Building new operating systems seems so ambitious to me. Radiant Computer (https://radiant.computer/ https://radiant.computer/) was also recently posted. What other exciting projects like these exist?
- ivanjermakov 10mo ago
  https://serenityos.org/ https://serenityos.org/
  - aloisdg 10mo ago
    [flagged]
    - coolKid721 10mo ago
      [flagged]
  - sharts 10mo ago
    This looks perfect. Just wonder how the hardware /software support goes
    - deleted 10mo ago
      [deleted]
- attila-lendvai 10mo ago
  it seems to be little more than a mission statement... no?
- lifty 10mo ago
  https://asterinas.github.io/ https://asterinas.github.io/ (Linux compatible Kernel) and https://redox-os.org/ https://redox-os.org/ are two promising ones.
  - oguz-ismail 10mo ago
    [dead]
  - criticalfault 10mo ago
    I wonder why all of these do not use gpl2?
    - floam 10mo ago
      I wouldn’t kneecap a OS project I wish to be adopted by licensing it GPL. Look at glibc which basically can’t practically support static linking. You make any of your OS standard libraries GPL and they need to suck to use and can’t statically link your code without being forced to also be licensed GPL. That viral property some people find desirable.
      - criticalfault 10mo ago
        Isn't this what made Linux successful? Being able to sell it closed and not releasing the source would make closing the android ecosystem 'good old times', no? We would only get a bunch of closed outdated company controlled binaries, but now for everything, not only drivers?
      - heavyset_go 10mo ago
        WRT kneecapping, history has shown that companies will bleed the commons dry and they need to be legally strong-armed into contributing back to the free software projects they make their fortunes off of. Virality might suit the ego, but it doesn't make for a healthy project when its primary users are parasitic.
        bigstrat2003 10mo ago
        > history has shown that companies will bleed the commons dry and they need to be legally strong-armed into contributing back to the free software projects they make their fortunes off of. Software is not a scarce good. Let companies use free software without contributing back as much as they wish; it doesn't affect others in the least. There is no bleeding of the commons here, because even if companies take as much as they can without giving back, it doesn't reduce the resources available for others.
- chrsw 10mo ago
  Not new, but alternative https://www.haiku-os.org/ https://www.haiku-os.org/
- zzo38computer 10mo ago
  I have ideas as well, and wrote about some of them (including some partial specifications), although I do not have a name for my own, so due to this, there is not a repository or anything like that yet. Note that, there are multiple parts, and different projects will have a different set of these parts: hardware, kernel, user/application programs; my ideas involve all three (there may be other parts, and different ways to divide them, too).
- Iwan-Zotow 10mo ago
  There is always Plan9
- accrual 10mo ago
  ReactOS continues to move forward! I know it's based on something extant and not net new, but it's still a new OS in my eyes. https://reactos.org/blogs/ https://reactos.org/blogs/
- snvzz 10mo ago
  The most important effort is seL4[0], the fastest OS kernel out there which also happens to be the most formally verified. LionsOS[1] is its static scenario building framework, with some dynamic scenario support. Genode[2] is an independent OS construction kit that can also use the seL4 kernel. Their general purpose OS, Sculpt, just had a very interesting multi-kernel release[3]. The systems group at ETHZürich is building Kirsch[4], an effort with seL4 and CHERI. Managarm[5] is also building something of interesting architecture with some Linux software compatibility. 0, https://sel4.systems/ https://sel4.systems/ 1. https://trustworthy.systems/projects/LionsOS/ https://trustworthy.systems/projects/LionsOS/ 2. https://genode.org/ https://genode.org/ 3. https://genodians.org/alex-ab/2025-11-02-sculpt-multi-kernel https://genodians.org/alex-ab/2025-11-02-sculpt-multi-kernel 4. https://sockeye.ethz.ch/kirsch/ https://sockeye.ethz.ch/kirsch/ 5. https://managarm.org/ https://managarm.org/
  - vacuity 10mo ago
    Note: IPC performance isn't the only factor in overall OS performance. Especially for a "traditional microkernel", where programs are split up into separate processes liberally, performance degrades due to the sheer number of cross-boundary interactions. A whole system is performant if the design of the whole system, not just the design of the kernel, is aligned with performance. This is not to put down seL4; on the other hand, it continues the trend of L4 microkernels demonstrating the viability of stricter designs. But keep in mind that more time and effort is necessary to implement larger systems well.
    - snvzz 10mo ago
      Do not miss the latest seL4 summit's state of seL4 talk by Gernot Heiser[0], which besides providing an update on the work done this year, goes into performance[1]. This is real world throughput and latency seL4 is crushing Linux on, not some synthetic IPC benchmark. 0. https://www.youtube.com/watch?v=wP48V34lDhk https://www.youtube.com/watch?v=wP48V34lDhk 1. https://youtu.be/wP48V34lDhk?t=1199 https://youtu.be/wP48V34lDhk?t=1199
      - vacuity 10mo ago
notepad0x90 10mo ago
There is an NDA related company called ironclad as well. Beware the trademark/copyright terrorists. That said, I am huge fan of works like this. But in practice, the security layer that betrays all of this tends to be the firmware layer. My dream is to have something like the Framework computer use verifiably secure EFI firmware, as well as similarly verified and audited firmware for every hardware component.
- F3nd0 10mo ago
  You might want to check out MNT Research if you haven’t yet. They make repairable laptops, too, but they also release their work as free software and open hardware. https://mnt.re/ https://mnt.re/
  - notepad0x90 10mo ago
    The MNT is too small for my usage, but it's a great effort. I think their goal is to make open hardware right now, not necessarily a verifiable one.
- indolering 10mo ago
  You need a different kernel for firmware verification. But it should be regulated at this point.
- scoot 10mo ago
  That isn't how trademarks work. There can be multiple business with the same name, as long as they operate in a different field. Case in point, Apple Computer had to pay for the rights to The Beatles label Apple Music only when they entered the music industry (not that they didn't try to contest it!) Copyright is something different entirely! https://xkcd.com/386/ https://xkcd.com/386/
  - notepad0x90 10mo ago
    That make sense. I'd still be weary though, you can win in court, but the cost of getting sued isn't small. Nintendo's lawsuits come to mind.
AlotOfReading 10mo ago
Interesting project. I'm curious about the limits of formal verification of worst case execution time. There are other formally verified kernels like seL4 and atmosphere, as well as layers you can stack on top to get a mostly compatible posix-ish layer like genode. You can also go out and find completely compatible kernels with enough maturity that (full) formal verification isn't a major value-add, like QNX or VxWorks. I'm not aware of much that combines WCET + formal verification + POSIX compatibility though. The verification page here is mostly at stone level, which from my understanding of SPARK terminology just means it passes validation, but might have runtime errors where most of Ada's WCET nondeterminism comes from. I'm skeptical that this is actually production usable for the hard real-time use cases all over their documentation at the current stage, but nothing on the website gives any clue as to the actual maturity short of reading the code myself.
- indolering 10mo ago
  Any government can get RCE on any OS with the change in their couch. Formal verification of process isolation is REALLY important when lives depend on it. That's a huge value add! My main concern is speed and the lack of capability based security. seL4 is faster than Linux by a mile and I'm guessing that this is much slower. You can put a POSIX layer on seL4 but POSIX is inherently flawed too. MAC separates privileges from code and is too clunky to use in practice (see seLinux).
  - SahAssar 10mo ago
    > Any government can get RCE on any OS with the change in their couch. Do you really believe that? That seems extremely implausible based on just simple observations like all governments using COTS OS for military/intelligence work or standard OS:es being used for critical infrastructure like power/water/finance/transportation. If your statement was even remotely true then why is this not used in conflicts to devastating effect?
    - numpy-thagoras 10mo ago
      Yes, I believe that. > If your statement was even remotely true then why is this not used in conflicts to devastating effect? It has been, it continues to be. Where have you been?
alberth 10mo ago
> It is written in SPARK and Ada, and is comprised of 100% free software. I thought SPARK was a paid (not free) license. Am I mistaken? Very cool project btw.
- misswaterfairy 10mo ago
  > I thought SPARK was a paid (not free) license. Am I mistaken? Similar model to Qt: permissive licensed open source version, with a commercial 'Pro' offering. https://en.wikipedia.org/wiki/SPARK_(programming_language) https://en.wikipedia.org/wiki/SPARK_(programming_language) https://alire.ada.dev/transition_from_gnat_community.html https://alire.ada.dev/transition_from_gnat_community.html
liamkinne 10mo ago
Is there a technical reason it only supports x86_64, riscv64, and not arm64?
- rurban 10mo ago
  There were a bunch of ports, like arm64, but with several bugs. So the maintainer removed all but x86_64, and then another group added risc64. From there arm64 can be tried again
deleted 10mo ago
[deleted]
anta40 10mo ago
For typical end users, kernel on its own is useless. So this an example of OS which uses Ironclad kernel: https://codeberg.org/Ironclad/Gloire https://codeberg.org/Ironclad/Gloire
lovidico 10mo ago
From their verification roadmap, it sure seems generous to refer to this as “formally verified”. They don’t prove anything important about the kernel clearly at all. Seems very disingenuous to describe it as they do since it lacks any of the merits of other formally verified kernels like seL4 and Tock.
wiradikusuma 10mo ago
Can we use Rust / Go / Java (GraalVM Native) or Flutter Linux to build an executable that runs on an OS with an Ironclad kernel? Or is there special treatment that makes it incompatible with "plain" Linux exe?
- Rochus 10mo ago
  Ironclad has a POSIX API, so yes, in principle it should be possible. There is an OS on top of Ironclad (https://github.com/Ironclad-Project/Gloire https://github.com/Ironclad-Project/Gloire) which uses GNU tools.
rurban 10mo ago
The MAC's are good: https://ironclad-os.org/manual/Mandatory-access-control-_0028MAC_0029.html https://ironclad-os.org/manual/Mandatory-access-control-_002...
Mockapapella 10mo ago
OK can someone smarter than me educate me? A couple weeks ago I was curious what the strictest programming language was. ChatGPT listed a couple, and it kicked off a short discussion where I began asking it about the capabilities of stricter programming languages at low levels. Funny enough at the end it mentioned that SPARK/Ada was the strictest you could get at the lowest levels, same as Ironclad. At one point while asking it about drivers, it said "ACL2’s logic is [...] side‑effect‑free definitions with termination proofs when admitted to the logic. That is misaligned with effectful, interrupt‑driven kernel code. I'm not an OS or kernel dev, most of my work has been in Web Dev, ML, and a little bit of embedded. How accurate is the information that was presented to me? Here is the link to the discussion: https://chatgpt.com/share/691012a7-a06c-800f-9cc9-54a7c2c8b640 https://chatgpt.com/share/691012a7-a06c-800f-9cc9-54a7c2c8b6... I don't know SPARK or Ada, but it just bothers me to think that we can't...I guess...prove everything about our software before we run it (yes yes, I'm familiar with halting problem shenanigans, but other than that).
- AlotOfReading 10mo ago
  There's a lot to unpack here. You can always make a stricter programming language by having your compiler error on everything. Lisps are perfectly usable for system level code as well. There was an entire lineage of Lisp Machines where virtually all OS code was written in lisp. Those probably could have used ACL2 had it existed. There's an X-Y component to your questions though. The strictness of the programming language just isn't the main goal for OS formal verification. It just makes certain things easier. What's important is having executable semantics of the programming language, having a machine model, and a behavioral specification. All of these are typically written in proof languages, and the kernel code is proven to implement the behavior spec according to the machine and language semantics. SPARK gives you executable semantics, but so do C (specifically the Clight subset), most of the Lisps, Rust, and many others. You're benefiting from certain errors being impossible in SPARK, but it's not a fundamentally different process.
tombert 10mo ago
I haven’t fully given up on the hope that a fully verified kernel eventually catches on. It would be basically impossible to verify all of Linux at this point, but I could see seL4 eventually getting traction in something like the smartphone market. A guy can dream, at least.
- meling 10mo ago
  It has been used for a while in the Secure Enclave operating system: https://en.wikipedia.org/wiki/L4_microkernel_family#:~:text=Apple%20A%20series,at%20310%20million https://en.wikipedia.org/wiki/L4_microkernel_family#:~:text=... But to my knowledge, not for the more general user facing OSes.
  - tombert 10mo ago
    Yeah that's what I was getting at. I know seL4 is used in a bunch of places, but outside of a few hobbyist projects I have never heard of anyone using is at a "full" OS. It would be nearly impossible to have the support for the extremely diverse set of hardware that desktop Linux has while staying formally verified, but for something a bit more constrained like a smartphone, I think something like seL4 could work as a base and the manufacturer could write their own drivers for whatever hardware is needed. I mean, how cool would it be if every single part of the stack that is even possible to verify was fully verified. I know about the halting problem, I know there are things that would be basically impossible to verify fully, but I still think it would be cool to live in a world where software engineers actually had a little assurance what they were doing actually worked before unleashing into the world.
    - AlotOfReading 10mo ago
      I know at least one autonomous vehicle company is using it as their base OS in the autonomy stack, with efforts at extending some form of verification up to the high level code.
      - tombert 10mo ago
nacozarina 10mo ago
SPARK’s “ask about pricing” stickers indicate this is “free” software that’s a different kind of free.
- monerozcash 10mo ago
  What about all the github links above that "ask about pricing"? Commercial support is not free, and the pricing for that is almost always something you have to ask for. Hard to see how this is piece of free software stands out.
- pjmlp 10mo ago
  That guy in Nebraska needs to buy food and shelter.
JoeDohn 10mo ago
"Formally verified" what does that means? As far as I know formal verification is another testing method and as as such it's is as good as the quality and the extent of the "verification" (aka tests). Best way to verify that I know of is Fuzzing + testing.
- curtisf 10mo ago
  Formal verification is explicitly NOT testing. It is a method where a computer verifies a proof that the program adheres to its specification for _all_ inputs (subject to whatever limitations the particular method has). Types are the simplest kind of formal verification, and with sufficiently advanced dependent type-systems, can be used to prove that programs obey arbitrarily complex specifications. However, this can be extremely laborious and requires significantly different skills than normal programming, so it is very rarely done in industry
shevy-java 10mo ago
Yay! Take that, Minix and GNU Hurd! \o/
- Rochus 10mo ago
  Ironclad isn't a microkernel, is it? At least the device drivers, file system and network stack seem to run in kernel space. I didn't find any strong architectural hints pointing to microkernel design in the implementation so far.
Rochus 10mo ago
Here is the deepwiki documentation: https://deepwiki.com/Ironclad-Project/Ironclad https://deepwiki.com/Ironclad-Project/Ironclad
- ptx 10mo ago
  Is that an AI-generated page pretending to be a wiki?
  - Rochus 10mo ago
    Don't tell me you don't know this service. It's extremely useful to get to know the code and architecture of a project. You can even ask questions about the code and get the relevant references to the corresponding sections in the source files.
    - debugnik 10mo ago
      Okay but that's not a wiki. Wiki implies pages can be collaboratively edited and linked. Otherwise it's not a wiki, it's just a website. The only collaboration here is to bait people into becoming maintainers and fix the hallucinated content. More than one maintainer has shown frustration at that site making up wrong documentation already.
      - shadowgovt 10mo ago
        Open collaborative editing is a useful feature enabled by wiki software, but I've never actually heard anyone claim it is core to the definition; it's more that it's the killer app enabled by the quick editing model embraced by WikiBase and the systems that ran on WikiBase after Cunningham made it available. You can definitely have a wiki of one user. And it's extremely common for organizations to have a wiki of only authorized users. Although in a high trust circumstance, there's really a good reason to lock users who can read the wiki out from editing the wiki as long as edits are audited. (Regardless of all of that, I'm fairly certain the deepwiki output is editable?)
      - Rochus 10mo ago
alexnewman 10mo ago
So if I find a bug or security bug does this speak to the usefulness of the formal verification claim?
lproven 10mo ago
Interesting. Ada is in the greater Wirthian family (it's Pascal-like), and until now, the only Unix-like kernel I was aware of in a Wirthian language was TUNIS: https://en.wikipedia.org/wiki/TUNIS https://en.wikipedia.org/wiki/TUNIS It was implemented in Concurrent Euclid. https://en.wikipedia.org/wiki/Concurrent_Euclid https://en.wikipedia.org/wiki/Concurrent_Euclid
- Rochus 10mo ago
  > the only Unix-like kernel I was aware of in a Wirthian language was TUNIS SPIN developed at the University of Washington in the nineties was written in Modula-3; it was a microkernel-based system and supported the Digital UNIX system call interface, allowing Unix applications to run. There was also Sol implemented at INRIA in a Pascal dialect in the eighties which offered a Unix-compatible environment; it was followed by Chorus (initially written in Pascal), also a microkernel-based system, compatible with Unix APIs.
  - lproven 10mo ago
    Fascinating! Thank you!
beanjuiceII 10mo ago
(partially) formally verified says right on the page https://ironclad-os.org/formalverification.html https://ironclad-os.org/formalverification.html
jonjacky 10mo ago
CuBit is another operating system in SPARK/Ada. 1. https://blog.adacore.com/cubit-a-general-purpose-operating-system-in-spark-ada https://blog.adacore.com/cubit-a-general-purpose-operating-s... 2. https://github.com/docandrew/CuBit https://github.com/docandrew/CuBit
ajdude 10mo ago
What I like most about ironclad is that it is fully posix-compliant, meaning that you can run a lot of UNIX programs on it already, like what "Gloire" does: https://github.com/Ironclad-Project/Gloire https://github.com/Ironclad-Project/Gloire
hulitu 10mo ago
> Ironclad – formally verified, real-time capable, Unix-like OS kernel What filesystems are supported ?

375 points by vitalnodo 10mo ago

Building new operating systems seems so ambitious to me. Radiant Computer (https://radiant.computer/ https://radiant.computer/) was also recently posted. What other exciting projects like these exist?

ivanjermakov 10mo ago
https://serenityos.org/ https://serenityos.org/
- aloisdg 10mo ago
  [flagged]
  - coolKid721 10mo ago
    [flagged]
- sharts 10mo ago
  This looks perfect. Just wonder how the hardware /software support goes
  - deleted 10mo ago
    [deleted]
attila-lendvai 10mo ago
it seems to be little more than a mission statement... no?
lifty 10mo ago
https://asterinas.github.io/ https://asterinas.github.io/ (Linux compatible Kernel) and https://redox-os.org/ https://redox-os.org/ are two promising ones.
- oguz-ismail 10mo ago
  [dead]
- criticalfault 10mo ago
  I wonder why all of these do not use gpl2?
  - floam 10mo ago
    I wouldn’t kneecap a OS project I wish to be adopted by licensing it GPL. Look at glibc which basically can’t practically support static linking. You make any of your OS standard libraries GPL and they need to suck to use and can’t statically link your code without being forced to also be licensed GPL. That viral property some people find desirable.
    - criticalfault 10mo ago
      Isn't this what made Linux successful? Being able to sell it closed and not releasing the source would make closing the android ecosystem 'good old times', no? We would only get a bunch of closed outdated company controlled binaries, but now for everything, not only drivers?
    - heavyset_go 10mo ago
      WRT kneecapping, history has shown that companies will bleed the commons dry and they need to be legally strong-armed into contributing back to the free software projects they make their fortunes off of. Virality might suit the ego, but it doesn't make for a healthy project when its primary users are parasitic.
      - bigstrat2003 10mo ago
        > history has shown that companies will bleed the commons dry and they need to be legally strong-armed into contributing back to the free software projects they make their fortunes off of. Software is not a scarce good. Let companies use free software without contributing back as much as they wish; it doesn't affect others in the least. There is no bleeding of the commons here, because even if companies take as much as they can without giving back, it doesn't reduce the resources available for others.
chrsw 10mo ago
Not new, but alternative https://www.haiku-os.org/ https://www.haiku-os.org/
zzo38computer 10mo ago
I have ideas as well, and wrote about some of them (including some partial specifications), although I do not have a name for my own, so due to this, there is not a repository or anything like that yet. Note that, there are multiple parts, and different projects will have a different set of these parts: hardware, kernel, user/application programs; my ideas involve all three (there may be other parts, and different ways to divide them, too).
Iwan-Zotow 10mo ago
There is always Plan9
accrual 10mo ago
ReactOS continues to move forward! I know it's based on something extant and not net new, but it's still a new OS in my eyes. https://reactos.org/blogs/ https://reactos.org/blogs/
snvzz 10mo ago
The most important effort is seL4[0], the fastest OS kernel out there which also happens to be the most formally verified. LionsOS[1] is its static scenario building framework, with some dynamic scenario support. Genode[2] is an independent OS construction kit that can also use the seL4 kernel. Their general purpose OS, Sculpt, just had a very interesting multi-kernel release[3]. The systems group at ETHZürich is building Kirsch[4], an effort with seL4 and CHERI. Managarm[5] is also building something of interesting architecture with some Linux software compatibility. 0, https://sel4.systems/ https://sel4.systems/ 1. https://trustworthy.systems/projects/LionsOS/ https://trustworthy.systems/projects/LionsOS/ 2. https://genode.org/ https://genode.org/ 3. https://genodians.org/alex-ab/2025-11-02-sculpt-multi-kernel https://genodians.org/alex-ab/2025-11-02-sculpt-multi-kernel 4. https://sockeye.ethz.ch/kirsch/ https://sockeye.ethz.ch/kirsch/ 5. https://managarm.org/ https://managarm.org/
- vacuity 10mo ago
  Note: IPC performance isn't the only factor in overall OS performance. Especially for a "traditional microkernel", where programs are split up into separate processes liberally, performance degrades due to the sheer number of cross-boundary interactions. A whole system is performant if the design of the whole system, not just the design of the kernel, is aligned with performance. This is not to put down seL4; on the other hand, it continues the trend of L4 microkernels demonstrating the viability of stricter designs. But keep in mind that more time and effort is necessary to implement larger systems well.
  - snvzz 10mo ago
    Do not miss the latest seL4 summit's state of seL4 talk by Gernot Heiser[0], which besides providing an update on the work done this year, goes into performance[1]. This is real world throughput and latency seL4 is crushing Linux on, not some synthetic IPC benchmark. 0. https://www.youtube.com/watch?v=wP48V34lDhk https://www.youtube.com/watch?v=wP48V34lDhk 1. https://youtu.be/wP48V34lDhk?t=1199 https://youtu.be/wP48V34lDhk?t=1199
    - vacuity 10mo ago

notepad0x90 10mo ago

There is an NDA related company called ironclad as well. Beware the trademark/copyright terrorists. That said, I am huge fan of works like this. But in practice, the security layer that betrays all of this tends to be the firmware layer. My dream is to have something like the Framework computer use verifiably secure EFI firmware, as well as similarly verified and audited firmware for every hardware component.

F3nd0 10mo ago
You might want to check out MNT Research if you haven’t yet. They make repairable laptops, too, but they also release their work as free software and open hardware. https://mnt.re/ https://mnt.re/
- notepad0x90 10mo ago
  The MNT is too small for my usage, but it's a great effort. I think their goal is to make open hardware right now, not necessarily a verifiable one.
indolering 10mo ago
You need a different kernel for firmware verification. But it should be regulated at this point.
scoot 10mo ago
That isn't how trademarks work. There can be multiple business with the same name, as long as they operate in a different field. Case in point, Apple Computer had to pay for the rights to The Beatles label Apple Music only when they entered the music industry (not that they didn't try to contest it!) Copyright is something different entirely! https://xkcd.com/386/ https://xkcd.com/386/
- notepad0x90 10mo ago
  That make sense. I'd still be weary though, you can win in court, but the cost of getting sued isn't small. Nintendo's lawsuits come to mind.

AlotOfReading 10mo ago

Interesting project. I'm curious about the limits of formal verification of worst case execution time. There are other formally verified kernels like seL4 and atmosphere, as well as layers you can stack on top to get a mostly compatible posix-ish layer like genode. You can also go out and find completely compatible kernels with enough maturity that (full) formal verification isn't a major value-add, like QNX or VxWorks. I'm not aware of much that combines WCET + formal verification + POSIX compatibility though. The verification page here is mostly at stone level, which from my understanding of SPARK terminology just means it passes validation, but might have runtime errors where most of Ada's WCET nondeterminism comes from. I'm skeptical that this is actually production usable for the hard real-time use cases all over their documentation at the current stage, but nothing on the website gives any clue as to the actual maturity short of reading the code myself.

indolering 10mo ago
Any government can get RCE on any OS with the change in their couch. Formal verification of process isolation is REALLY important when lives depend on it. That's a huge value add! My main concern is speed and the lack of capability based security. seL4 is faster than Linux by a mile and I'm guessing that this is much slower. You can put a POSIX layer on seL4 but POSIX is inherently flawed too. MAC separates privileges from code and is too clunky to use in practice (see seLinux).
- SahAssar 10mo ago
  > Any government can get RCE on any OS with the change in their couch. Do you really believe that? That seems extremely implausible based on just simple observations like all governments using COTS OS for military/intelligence work or standard OS:es being used for critical infrastructure like power/water/finance/transportation. If your statement was even remotely true then why is this not used in conflicts to devastating effect?
  - numpy-thagoras 10mo ago
    Yes, I believe that. > If your statement was even remotely true then why is this not used in conflicts to devastating effect? It has been, it continues to be. Where have you been?

alberth 10mo ago

> It is written in SPARK and Ada, and is comprised of 100% free software. I thought SPARK was a paid (not free) license. Am I mistaken? Very cool project btw.

misswaterfairy 10mo ago
> I thought SPARK was a paid (not free) license. Am I mistaken? Similar model to Qt: permissive licensed open source version, with a commercial 'Pro' offering. https://en.wikipedia.org/wiki/SPARK_(programming_language) https://en.wikipedia.org/wiki/SPARK_(programming_language) https://alire.ada.dev/transition_from_gnat_community.html https://alire.ada.dev/transition_from_gnat_community.html

liamkinne 10mo ago

Is there a technical reason it only supports x86_64, riscv64, and not arm64?

rurban 10mo ago
There were a bunch of ports, like arm64, but with several bugs. So the maintainer removed all but x86_64, and then another group added risc64. From there arm64 can be tried again

deleted 10mo ago

[deleted]

anta40 10mo ago

For typical end users, kernel on its own is useless. So this an example of OS which uses Ironclad kernel: https://codeberg.org/Ironclad/Gloire https://codeberg.org/Ironclad/Gloire

lovidico 10mo ago

From their verification roadmap, it sure seems generous to refer to this as “formally verified”. They don’t prove anything important about the kernel clearly at all. Seems very disingenuous to describe it as they do since it lacks any of the merits of other formally verified kernels like seL4 and Tock.

wiradikusuma 10mo ago

Can we use Rust / Go / Java (GraalVM Native) or Flutter Linux to build an executable that runs on an OS with an Ironclad kernel? Or is there special treatment that makes it incompatible with "plain" Linux exe?

Rochus 10mo ago
Ironclad has a POSIX API, so yes, in principle it should be possible. There is an OS on top of Ironclad (https://github.com/Ironclad-Project/Gloire https://github.com/Ironclad-Project/Gloire) which uses GNU tools.

rurban 10mo ago

The MAC's are good: https://ironclad-os.org/manual/Mandatory-access-control-_0028MAC_0029.html https://ironclad-os.org/manual/Mandatory-access-control-_002...

Mockapapella 10mo ago

OK can someone smarter than me educate me? A couple weeks ago I was curious what the strictest programming language was. ChatGPT listed a couple, and it kicked off a short discussion where I began asking it about the capabilities of stricter programming languages at low levels. Funny enough at the end it mentioned that SPARK/Ada was the strictest you could get at the lowest levels, same as Ironclad. At one point while asking it about drivers, it said "ACL2’s logic is [...] side‑effect‑free definitions with termination proofs when admitted to the logic. That is misaligned with effectful, interrupt‑driven kernel code. I'm not an OS or kernel dev, most of my work has been in Web Dev, ML, and a little bit of embedded. How accurate is the information that was presented to me? Here is the link to the discussion: https://chatgpt.com/share/691012a7-a06c-800f-9cc9-54a7c2c8b640 https://chatgpt.com/share/691012a7-a06c-800f-9cc9-54a7c2c8b6... I don't know SPARK or Ada, but it just bothers me to think that we can't...I guess...prove everything about our software before we run it (yes yes, I'm familiar with halting problem shenanigans, but other than that).

AlotOfReading 10mo ago
There's a lot to unpack here. You can always make a stricter programming language by having your compiler error on everything. Lisps are perfectly usable for system level code as well. There was an entire lineage of Lisp Machines where virtually all OS code was written in lisp. Those probably could have used ACL2 had it existed. There's an X-Y component to your questions though. The strictness of the programming language just isn't the main goal for OS formal verification. It just makes certain things easier. What's important is having executable semantics of the programming language, having a machine model, and a behavioral specification. All of these are typically written in proof languages, and the kernel code is proven to implement the behavior spec according to the machine and language semantics. SPARK gives you executable semantics, but so do C (specifically the Clight subset), most of the Lisps, Rust, and many others. You're benefiting from certain errors being impossible in SPARK, but it's not a fundamentally different process.

tombert 10mo ago

I haven’t fully given up on the hope that a fully verified kernel eventually catches on. It would be basically impossible to verify all of Linux at this point, but I could see seL4 eventually getting traction in something like the smartphone market. A guy can dream, at least.

meling 10mo ago
It has been used for a while in the Secure Enclave operating system: https://en.wikipedia.org/wiki/L4_microkernel_family#:~:text=Apple%20A%20series,at%20310%20million https://en.wikipedia.org/wiki/L4_microkernel_family#:~:text=... But to my knowledge, not for the more general user facing OSes.
- tombert 10mo ago
  Yeah that's what I was getting at. I know seL4 is used in a bunch of places, but outside of a few hobbyist projects I have never heard of anyone using is at a "full" OS. It would be nearly impossible to have the support for the extremely diverse set of hardware that desktop Linux has while staying formally verified, but for something a bit more constrained like a smartphone, I think something like seL4 could work as a base and the manufacturer could write their own drivers for whatever hardware is needed. I mean, how cool would it be if every single part of the stack that is even possible to verify was fully verified. I know about the halting problem, I know there are things that would be basically impossible to verify fully, but I still think it would be cool to live in a world where software engineers actually had a little assurance what they were doing actually worked before unleashing into the world.
  - AlotOfReading 10mo ago
    I know at least one autonomous vehicle company is using it as their base OS in the autonomy stack, with efforts at extending some form of verification up to the high level code.
    - tombert 10mo ago

nacozarina 10mo ago

SPARK’s “ask about pricing” stickers indicate this is “free” software that’s a different kind of free.

monerozcash 10mo ago
What about all the github links above that "ask about pricing"? Commercial support is not free, and the pricing for that is almost always something you have to ask for. Hard to see how this is piece of free software stands out.
pjmlp 10mo ago
That guy in Nebraska needs to buy food and shelter.

JoeDohn 10mo ago

"Formally verified" what does that means? As far as I know formal verification is another testing method and as as such it's is as good as the quality and the extent of the "verification" (aka tests). Best way to verify that I know of is Fuzzing + testing.

curtisf 10mo ago
Formal verification is explicitly NOT testing. It is a method where a computer verifies a proof that the program adheres to its specification for _all_ inputs (subject to whatever limitations the particular method has). Types are the simplest kind of formal verification, and with sufficiently advanced dependent type-systems, can be used to prove that programs obey arbitrarily complex specifications. However, this can be extremely laborious and requires significantly different skills than normal programming, so it is very rarely done in industry

shevy-java 10mo ago

Yay! Take that, Minix and GNU Hurd! \o/

Rochus 10mo ago
Ironclad isn't a microkernel, is it? At least the device drivers, file system and network stack seem to run in kernel space. I didn't find any strong architectural hints pointing to microkernel design in the implementation so far.

Rochus 10mo ago

Here is the deepwiki documentation: https://deepwiki.com/Ironclad-Project/Ironclad https://deepwiki.com/Ironclad-Project/Ironclad

ptx 10mo ago
Is that an AI-generated page pretending to be a wiki?
- Rochus 10mo ago
  Don't tell me you don't know this service. It's extremely useful to get to know the code and architecture of a project. You can even ask questions about the code and get the relevant references to the corresponding sections in the source files.
  - debugnik 10mo ago
    Okay but that's not a wiki. Wiki implies pages can be collaboratively edited and linked. Otherwise it's not a wiki, it's just a website. The only collaboration here is to bait people into becoming maintainers and fix the hallucinated content. More than one maintainer has shown frustration at that site making up wrong documentation already.
    - shadowgovt 10mo ago
      Open collaborative editing is a useful feature enabled by wiki software, but I've never actually heard anyone claim it is core to the definition; it's more that it's the killer app enabled by the quick editing model embraced by WikiBase and the systems that ran on WikiBase after Cunningham made it available. You can definitely have a wiki of one user. And it's extremely common for organizations to have a wiki of only authorized users. Although in a high trust circumstance, there's really a good reason to lock users who can read the wiki out from editing the wiki as long as edits are audited. (Regardless of all of that, I'm fairly certain the deepwiki output is editable?)
    - Rochus 10mo ago

alexnewman 10mo ago

So if I find a bug or security bug does this speak to the usefulness of the formal verification claim?

lproven 10mo ago

Interesting. Ada is in the greater Wirthian family (it's Pascal-like), and until now, the only Unix-like kernel I was aware of in a Wirthian language was TUNIS: https://en.wikipedia.org/wiki/TUNIS https://en.wikipedia.org/wiki/TUNIS It was implemented in Concurrent Euclid. https://en.wikipedia.org/wiki/Concurrent_Euclid https://en.wikipedia.org/wiki/Concurrent_Euclid

Rochus 10mo ago
> the only Unix-like kernel I was aware of in a Wirthian language was TUNIS SPIN developed at the University of Washington in the nineties was written in Modula-3; it was a microkernel-based system and supported the Digital UNIX system call interface, allowing Unix applications to run. There was also Sol implemented at INRIA in a Pascal dialect in the eighties which offered a Unix-compatible environment; it was followed by Chorus (initially written in Pascal), also a microkernel-based system, compatible with Unix APIs.
- lproven 10mo ago
  Fascinating! Thank you!

beanjuiceII 10mo ago

(partially) formally verified says right on the page https://ironclad-os.org/formalverification.html https://ironclad-os.org/formalverification.html

jonjacky 10mo ago

CuBit is another operating system in SPARK/Ada. 1. https://blog.adacore.com/cubit-a-general-purpose-operating-system-in-spark-ada https://blog.adacore.com/cubit-a-general-purpose-operating-s... 2. https://github.com/docandrew/CuBit https://github.com/docandrew/CuBit

ajdude 10mo ago

What I like most about ironclad is that it is fully posix-compliant, meaning that you can run a lot of UNIX programs on it already, like what "Gloire" does: https://github.com/Ironclad-Project/Gloire https://github.com/Ironclad-Project/Gloire

hulitu 10mo ago

> Ironclad – formally verified, real-time capable, Unix-like OS kernel What filesystems are supported ?