Formal verification is the difficult but necessary next step for security-intensive applications.
Also, any new kernel should only be written in a memory-safe language. Rust would be the best, since it is also safe from data races, outside of unsafe blocks.
The proof evidence is very hard to extend meaningfully for new platforms, and you're limited to environments which have a sufficient MMU.
We're starting with seL4 and building a whole Rust-based userland around it, and creating a whole pile of compile-time assurances along the way to make sure we're not inadvertently doing something dangerous or stupid with the rope seL4 gives you.
It's worth it for us. However, it is a colossal pain in the ass. That said, in the coming months we're likely to open source some of our progress in making it easier and more reliable to work with, integrate with, and otherwise leverage seL4 for certain use cases.
As an aside, I wonder just how much async/await in Rust will obviate the need for small kernels in deeply embedded applications. If I can do blocking IO with my peripherals and use the async state machines to do "task" switching, well... who needs tasks and capabilities? It'd land somewhere on the "language OS" side of an embedded OS almost.
When we open source things in the coming weeks & months they'll all land on GitHub, https://github.com/auxoncorp, so that's probably the lowest touch way of observing what we're up to as things mature.
While Rust seems to be promising here, I'm not sure whether the current async/await implementation will really allow for this. I experimented a bit with it, and found lots of issues where async/await lead to severe memory bloat (composing 3 async functions that do not a lot things requiring a 20kB task allocation). The compatibility with Futures and the requirement to move async fns to compose them before using them (which requires extra stack - which again ends up as extra heap/task memory) plays a bit against it. But these things are also worked on, so let's seee how it works out.
Waiting directly on the resource like that would require exclusive access quite often though?
You should read [1] to understand how Rust achieves this.
A data race has Undefined Behavior, and is therefore impossible to perform in Safe Rust.
...
However Rust does not prevent general race conditions.
This is pretty fundamentally impossible, and probably honestly undesirable. Your hardware is racy, your OS is racy, the other programs on your computer are racy, and the world this all runs in is racy. Any system that could genuinely claim to prevent all race conditions would be pretty awful to use, if not just incorrect.
Maybe you should read a bit more on its docs [1]. I quote:
However Rust does not prevent general race conditions.