L4.sec implementation and formal verification

 Hello Misters, As you are microkernel experts, I am  asking your help.  I am attempting to build up a team.  I believe it's time for a full-fledge verified OS. If somebody is interested in functional programming and in formal methods to help to implement the L4.sec kernel , he is welcome :) Here is an example of a protocol formalisation : network stack : http://www.cl.cam.ac.uk/~pes20/Netsem/ If you want to contact me, my mail is guillaume_dot_fortaine_at_wanadoo_dot_fr I will set up a mailing-list, a web server, a wiki and an IRC Best Regards,                           Guillaume FORTAINE