If you find this interesting you may want to read about this more current research: http://www.openmirage.org/

To quote from the vision paper http://anil.recoil.org/papers/2010-bcs-visions.pdf

  Mirage is written in the spirit of vertical operating 
  systems such as Nemesis [17] or Exokernel [10], but
  differs in certain aspects: (i) apart from a small runtime,
  the operating system and support code (e.g., threading)
  is entirely written in OCaml; and (ii) is statically
  specialised at compile-time by assembling only required
  components (e.g., a read-only file system which fits
  into memory will be directly linked in as an immutable
  data structure). These features mean that it provides
  a stronger basis for the practical application of formal
  methods such as model checking; and the removal of
  redundant safety system checks greatly improves the
  energy efficiency of the system.