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.
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.
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).
> 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?
The publicly available exploit prices put a browser zero day at $200k-$500k. That's the same cost as firing a few Javalin missiles. OS RCE runs into $1-$2 million. Much less than a cheap Russian tank. [1]
The cost of internally developed exploits is probably much lower. They aren't one shot assets either, they can be used until someone plugs the hole.
There are private companies selling devices to law enforcement that can extract information from locked phones [2]. Availability of that sort of access to anyone's phone by local law enforcement is absurdly cheap.
it is used here n there but unlike bullets the attacks if they remain unknown have no armer to defend against them, but are single use.
since the 2010s atleast more than 140 countries spend over 10 mil a year on purly offensive cyber. most of those countries spend astronomical amounts more than that. that includes purchase of attack tools and exploits
That really depends on what formal verification means in context. I don't see any interesting specifications in the repo, just basic stuff like this MD5 spec [0] that doesn't verify whether the MD5 implementation is correct. This is one of the areas where formal verification is listed as completed/gold level.
It's common for the interesting OS proofs to take more code than the kernel itself. Take a look at the seL4 proofs [1], or those for CertiKOS as examples.
If you're actually interested in alternative OSes in memory safe languages, you might like TockOS, which is more production-ready at this point. Formal verification work of the isolation model is still ongoing, because it's difficult work.
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.
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.
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!)
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.
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.
seL4 is being used in many places that we know about[0] and then there's those we don't or are still in the future, where we can only guess based on e.g. seL4 membership[1].
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.
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.
> 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.
Software is rarely finished, and development has real costs.
When that development gets silo'ed away in proprietary systems, that is potential development lost upstream. If that happens enough, upstream becomes starved and anemic, and with forks only living on in silos.
Apple, for example, has made trillions of dollars off of FreeBSD. To this day, FreeBSD still does not have a modern WiFi or Bluetooth stack.
Meanwhile, AMD, Intel, Microsoft, and even Apple, etc have full-time engineering roles and teams dedicated to upstreaming their improvements to Linux. And there are paid engineers at these companies that ensure WiFi and Bluetooth work on Linux.
Rust's technical choices seem to make releasing GPL software with it cumbersome and unattractive. Also the implied goal of a lot of Rust projects is to replace GPL'ed programs with permissive ones.
Which technical choices are thinking of here? My best guess is the crates ecosystem and the oft discussed ‘dependency hell’ that pervasive package manager usage seems to engender. Is there something else I’m missing contributing to the (maybe purposeful) reluctance to push GPL code?
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).
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.
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.
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
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-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).
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.
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?
"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.
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.
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).
> 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?
The publicly available exploit prices put a browser zero day at $200k-$500k. That's the same cost as firing a few Javalin missiles. OS RCE runs into $1-$2 million. Much less than a cheap Russian tank. [1]
The cost of internally developed exploits is probably much lower. They aren't one shot assets either, they can be used until someone plugs the hole.
There are private companies selling devices to law enforcement that can extract information from locked phones [2]. Availability of that sort of access to anyone's phone by local law enforcement is absurdly cheap.
[1]: https://opzero.ru/en/prices/
[2]: https://arstechnica.com/gadgets/2025/10/leaker-reveals-which...
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?
it is used here n there but unlike bullets the attacks if they remain unknown have no armer to defend against them, but are single use.
since the 2010s atleast more than 140 countries spend over 10 mil a year on purly offensive cyber. most of those countries spend astronomical amounts more than that. that includes purchase of attack tools and exploits
1) Those things are being hardened right now
2) You haven’t seen a hot conflict yet
It does not have to remain at stone level, and it can get legit certifications, too.
Looking forward to it. A formally verified OS is a great step towards better security.
That really depends on what formal verification means in context. I don't see any interesting specifications in the repo, just basic stuff like this MD5 spec [0] that doesn't verify whether the MD5 implementation is correct. This is one of the areas where formal verification is listed as completed/gold level.
It's common for the interesting OS proofs to take more code than the kernel itself. Take a look at the seL4 proofs [1], or those for CertiKOS as examples.
If you're actually interested in alternative OSes in memory safe languages, you might like TockOS, which is more production-ready at this point. Formal verification work of the isolation model is still ongoing, because it's difficult work.
[0] https://codeberg.org/Ironclad/Ironclad/src/branch/main/sourc...
[1] https://github.com/seL4/l4v
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.
Ironclad is also the name of the chief cryptographic library for Common Lisp: https://github.com/sharplispers/ironclad/
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/
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.
You need a different kernel for firmware verification. But it should be regulated at this point.
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/
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.
SPARK’s “ask about pricing” stickers indicate this is “free” software that’s a different kind of free.
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.
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.
It has been used for a while in the Secure Enclave operating system: https://en.wikipedia.org/wiki/L4_microkernel_family#:~:text=...
But to my knowledge, not for the more general user facing OSes.
seL4 is being used in many places that we know about[0] and then there's those we don't or are still in the future, where we can only guess based on e.g. seL4 membership[1].
0. https://sel4.systems/use.html
1. https://sel4.systems/Foundation/Membership/
Building new operating systems seems so ambitious to me. Radiant Computer (https://radiant.computer/) was also recently posted.
What other exciting projects like these exist?
https://asterinas.github.io/ (Linux compatible Kernel) and https://redox-os.org/ are two promising ones.
Asterinas looks cool, but they literally are involved with sustech, what a name for an organization!
I wonder why all of these do not use gpl2?
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.
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.
> 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.
Software is rarely finished, and development has real costs.
When that development gets silo'ed away in proprietary systems, that is potential development lost upstream. If that happens enough, upstream becomes starved and anemic, and with forks only living on in silos.
Apple, for example, has made trillions of dollars off of FreeBSD. To this day, FreeBSD still does not have a modern WiFi or Bluetooth stack.
Meanwhile, AMD, Intel, Microsoft, and even Apple, etc have full-time engineering roles and teams dedicated to upstreaming their improvements to Linux. And there are paid engineers at these companies that ensure WiFi and Bluetooth work on Linux.
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?
Rust's technical choices seem to make releasing GPL software with it cumbersome and unattractive. Also the implied goal of a lot of Rust projects is to replace GPL'ed programs with permissive ones.
Which technical choices are thinking of here? My best guess is the crates ecosystem and the oft discussed ‘dependency hell’ that pervasive package manager usage seems to engender. Is there something else I’m missing contributing to the (maybe purposeful) reluctance to push GPL code?
> Also the implied goal of a lot of Rust projects is to replace GPL'ed programs with permissive ones.
People really got to stop with crazy nonsense.
https://serenityos.org/
This looks perfect. Just wonder how the hardware /software support goes
Not new, but alternative https://www.haiku-os.org/
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/
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).
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/
1. https://trustworthy.systems/projects/LionsOS/
2. https://genode.org/
3. https://genodians.org/alex-ab/2025-11-02-sculpt-multi-kernel
4. https://sockeye.ethz.ch/kirsch/
5. https://managarm.org/
it seems to be little more than a mission statement... no?
There is always Plan9
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.
The MAC's are good: https://ironclad-os.org/manual/Mandatory-access-control-_002...
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
> 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.
> 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://alire.ada.dev/transition_from_gnat_community.html
Is there a technical reason it only supports x86_64, riscv64, and not arm64?
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
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-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).
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.
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?