QED Prover Experiments writing a proof system, particularly designed to prove properties about Haskell code, such as the HLint rewrite rules. Tom Ellis described the approach as "coinduction on the execution".