Hi guys, For a while I've been looking into formalizing parts of xmonad in the Coq proof assistant. After a bit of work, I've written a Coq module that, when you extract Haskell code from it, produces a drop-in replacement for xmonad's StackSet module. The generated Haskell code is clearly not hand-written and triggers plenty of ghc warnings, but passes the QuickCheck testsuite. I've put everything online here: https://bitbucket.org/wouterswierstra/xmonad It require one or two very modest patches to xmonad to build, but nothing controversial. See the readme for more technical details. I've managed to prove a handful of QuickCheck properties in Coq, but I just don't have the time to see this project through. If anyone is interested in contributing, I'd be very happy to advise them on how to proceed. I think it would make quite a nice exercise for anyone interested in learning more about formal verification using Coq -- but it's certainly not for the faint hearted! All the best, Wouter