I came across a new project out of Dresdin University, called VFiasco (Verified Fiasco). VFiasco is an attempt to produce a verifiably correct microkernel. It is based on a previous DU microkernel project called Fiasco, which is an L4 compatible microkernel licensed under the GPL. I thought this might be just the sort of thing that would interest the TUNES folks. http://os.inf.tu-dresden.de/vfiasco/ -Jason