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.
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).
Looking forward to it. A formally verified OS is a great step towards better security.
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.
Copyright is something different entirely!
What other exciting projects like these exist?
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.
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?
I thought SPARK was a paid (not free) license. Am I mistaken?
Very cool project btw.
Similar model to Qt: permissive licensed open source version, with a commercial 'Pro' offering.