I have smart teachers

How about proving the correctness of the L4 microkernel? Turns out my current algorithms teacher was/is(?) the program leader of the group doing this work. "Logic of knowledge" anyone? Smart guy.

L4 verified
Open Kernel Labs
NICTA

In other news, my OO professor last session gets props I suppose for hitting the blog headlines for a paper he wrote with my tutor last session. Validity Invariants and Effects. "Design by contract" takes on a whole new meaning.