L4.sec implementation and formal verification

William DUCK guillaume.fortaine at wanadoo.fr
Sat Aug 26 04:05:11 CEST 2006

 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 :

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

More information about the l4-hackers mailing list