Interesting. I have already seen the approach "Lets design this in haskell and write production code in C" for http://cryptol.net/ http://cryptol.net/, but due

Interesting. I have already seen the approach "Lets design this in haskell and write production code in C" for http://cryptol.net/ http://cryptol.net/, but due to limited scope (mostly functions of several hundered bits input and output as customary in crypto-primitives), they were able to check that the implementation adheres to specification automatically. The aim was to allways know that the c code does what it is supposed to, so that programmer can focus on mitigating side-channel attacks :) I wonder if something similar would be applicable to writing the micro-kernell.