A mix of Coq proofs and Haskell code about Unicode Grapheme Clusters as specified in UAX29. The idea is to automatically derive a regular expression from the rules given in UAX29 and identify degenerate cases (since UAX29 doesn't list all degenerate cases).
Use Stack.