https://www.linux.org.ru/forum/developm ... d=17544801
Muen is an Open Source separation kernel (SK) for the Intel x86/64 architecture that has been formally proven to contain no runtime errors at the source code level.
https://muen.codelabs.ch/
Мне не интересно, но Вы вроде проявляли интерес ко всяким ядрам.