Barrelfish: microkernel(?) + capabilities + distributed heterogeneous cores + formal proofs + Haskell

Since no one else has mentioned it yet, let me present, The Barrelfish  
Operating System:

http://barrelfish.org/

As described in this paper:

http://barrelfish.org/barrelfish_sosp09.pdf

    "We investigate a new OS structure, the multikernel, that treats  
the machine as a
network of independent cores, assumes no inter-core sharing at the
lowest level, and moves traditional OS functionality to a distributed
system of processes that communicate via message-passing."

This paper describes the use of DSLs and DSL -> C compilers written in  
Haskell to generate low-level kernel code:

http://www.barrelfish.org/fof_plos09.pdf

The aim is to be able to build provably correct DSLs and compilers  
fast enough that you would actually prefer to use them as part of the  
development process instead of just doing the low-level C code by hand.

- jeremy