I think it's a great idea actually. Build a small kernel with very few responsibilities so it's easier to prove safety That already exists and was just open so

I think it's a great idea actually. Build a small kernel with very few responsibilities so it's easier to prove safety That already exists and was just open sourced! See seL4: http://en.wikipedia.org/wiki/L4_microkernel_family#High_assurance:_seL4 http://en.wikipedia.org/wiki/L4_microkernel_family#High_assu...