Hello Misters, As you are iin functional programming, I am asking your help. I am attempting to build up a team. I believe it's time for a full-fledge verified OS. http://www.ertos.nicta.com.au/publications/papers/Tuch_KH_05.pdf Here are my guidelines : http://www.cse.ogi.edu/~hallgren/House/ *OS-design : http://www.ertos.nicta.com.au/publications/papers/Leslie_06.pdf ( for transition ) http://www.marcus-brinkmann.org/hurd-ng.pdf http://www.eecg.toronto.edu/~tornado/ ( scalability / hot swapping ) *kernel : http://os.inf.tu-dresden.de/L4/L4.Sec/ http://www.doclsf.de/papers/vstte06.pdf#search=%22formalising%20high%20perfo... *network stack : http://www.cl.cam.ac.uk/~pes20/Netsem/ *programming : http://fling-l.seas.upenn.edu/~plclub/cgi-bin/poplmark/index.php?title=The_P... http://www.informatik.uni-bonn.de/~loeh/GFP.html http://maude.cs.uiuc.edu/tools/scc/ *proving environment : http://isabelle.in.tum.de/ http://www.cl.cam.ac.uk/Research/HVG/HOL/ *compiler : http://pauillac.inria.fr/~xleroy/compcert-backend/ http://www.score.is.tsukuba.ac.jp/~okuma/vc/ Any suggestions ? Thank you for your answer, 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, Best Regards,                           Guillaume FORTAINE