Signed up just to comment on this. I've been wanting to do something similar for a while now (although, an exokernel).<p>You should update your source to use the new 2014 tools. The verifications become part of the syntax.
For embedded/industrial applications the future is in domain-specific operating systems that are JEOS by virtue of not compling unneeded syscalls. OSes like Linux have way too many ABIs and internal machinery that just aren't necessary for headless systems and merely opens a huge attack surface by default... Even with make menuconfig stripped .config, there's still a ton of extra bells and whistles.<p>In a positive direction, it would be nice to be able to be able to strip out more functionality and still produce a functional kernel. Unfortunately, I don't think this is scalable with autotools or any configuration management setups without having more #ifdefs than code. Haskell could be a good candidate for such a kernel framework, but I'm sure there are other functional and imperative languages that have better complex configuration mgmt support with formal verification.
Honest question: who has a use-case for which a Raspberry wasn't powerful enough, but a Banana would have been?<p>Given that the Banana is about twice as expensive, here's a subsidiary question: who has a use-case for which TWO Raspberries wouldn't have been powerful enough, but a Banana would have been?
> The Muen Separation Kernel is the world’s first Open Source microkernel that has been formally proven to contain no runtime errors at the source code level.<p>I had the impression seL4 was the first microkernel formally proven to be secure.
Hmmm, one problem I see with this, at least for us open source mortals, is that all this rigor sits atop a festering pile of C, that is, the GCC (the GNAT Ada compiler in it)....<p>At least as these people are using SPARK/Ada.<p>Then again, maybe I should return to looking at Intel CPU and chipset errata....<p>On the third hand, these guys aren't using systems with ECC.... (<a href="http://ark.intel.com/products/64893/intel-core-i7-3520m-processor-4m-cache-up-to-3_60-ghz" rel="nofollow">http://ark.intel.com/products/64893/intel-core-i7-3520m-proc...</a>).