4 ms·
What I like about seL4 (although not a complete embedded dev platform) is formally-verification. QNX might have EAL4 in some configurations, but like most every
by banish-m4 2y ago
What I like about seL4 (although not a complete embedded dev platform) is formally-verification. QNX might have EAL4 in some configurations, but like most every other operating system on the planet, they haven't bothered to up their game by formally verifying it for correctness. This is a shame and entirely preventable with greater attention to testing and verification.
- kragen 2y agowhat sel4 shows is that it's entirely preventable with a rewrite from scratch by a team of formal-methods ph.d.s over many years, if they invent a design that allows the kernel to only be a few thousand lines of code so that the titanic effort of formal verification becomes feasible, barely. it's not something you can do with a codebase of millions of lines of code or a codebase that wasn't written from scratch with formal verification in mind. yet, anyway