Nice submission. Didn’t know about this. Here’s the descriptions for version 4 and version 5. There is a ton of complexity in these. They can’t be trusted any more than other hardened Linuxes. Running it in user-mode on secure kernels or hypervisors is still safest solution since all the complexity is contained in deprivileged space.
For some reason, the French are still behind on that. Unless, they aren’t but answer is in a French language resource I haven’t read. They certainly have the talent and tooling to pull it off. While INTEGRITY-178B shot for EAL6+ High Robustness, the best I saw in response from France was PolyXene at EAL5+. That was it for years. Then, Prove & Run did ProvenCore for ARM claiming it was all formally verified (i.e. EAL7-ish). I see no evaluation, though.
Since these are all proprietary, we can’t evaluate their real security. The EAL’s represent effort put into specific components. seL4 (EAL7+-ish) took a few years whereas they’re said to put 10+ years into PolyXene and who knows what for CLIP OS which isn’t securable at all. U.S. (INTEGRITY-178B, LynxSecure, VxWorks MILS), Australia (OKL4, seL4), and Germany (Perseus and Genode Architectures) are playing it smarter with tiny TCB’s. Even Qubes (Poland) is safer despite its weak TCB due to also isolating most of the complexity.