The main problem now is that there isn't a platform that has the tooling or infrastructure to prove, including through formal methods, that they are correct and free from bugs in the spirit of the seL4 project.