Capabilities. Like fine grain locks, these are very powerful and very hard to get right. That's the lesson from Hydra, the 432, .... No, it's not a hard mechanism for the microkernel to get right; it's a hard policy for the application programmer to get right. However, that's probably more of an opportunity rather than meant as a criticism. Our tools are massively more evolved than they were in the 70s. It'll be interesting to see what happens with capabilities.
C++. Oh lord. Why are you writing a microkernel in C++? If there was anything they learned from L4 (Xen, Linux, ...) it is that C is sufficient. Why do you want to implement something small with something that is large? This one is a real head scratcher.
Provably secure. They did this with the SEL4 microkernel so this is a doable thing. If they're going to hang their hat on security (capabilities, microkernel, ...) there's no excuse for not having done this already and delivered a provably secure microkernel out of the box.