Writing static checks to an unsuspecting library with Liquid Haskell

Link: Writing static checks to an unsuspecting library with Liquid Haskell

The author uses Liquid Haskell, a version of Haskell with refinement types, to prove that a diffing algorithm is correct.