Xmonad from Coq: Programming a Window Manager with a Proof Assistant (2012) [pdf] (staff.science.uu.nl)

The point of this exercise wasn't really to have a formally verified window manager, it was to document what it's like to make formally verified software. As a modestly complex program and one of the most well-known Haskell programs, xmonad was a good choice.

And while I agree that a formally verified X window manager seems a bit silly, a formally verified Wayland compositor would be a great idea given their broad scope of responsibilities.

True, but the number of times I have to restart because Gnome has borked and is no longer recognising mouse clicks, makes me think it has a place.

If you do it right, you only need to verify a few key components with interface conditions on how the rest should use them. This approach was taken in high-assurance security to build window managers that prevented leaks between apps or login spoofing. Nitpicker GUI is a modern example of that at least architecturally.