I’m glad you asked!
Formal verification is an automatic checking methodology that catches many common design errors and can uncover ambiguities in the design. It is an exhaustive methodology that covers all input scenarios and also detects corner case bugs.
One of the most futuristic companies I know of is Runtime Verification that uses formal Methods in industry. They have a list of accomplishments that seem like vaporware including a semantic babel fish called the K framework that can translate between languages based on formal, semantic definitions of each.
It’s not important unless Xmonad was being used for some kind of task where human lives are at risk if a mistake was made. In my case here (and indeed much of the Haskell world) it’s just fun to surround myself with software of that kind of code quality/reliability.