Formalized laws for the mtl library Laws for mtl classes Verified implementations for the common monad transformers Code to be as close to mtl and transformers as possible, rather than practical in Coq. Future work Merge with coq-ext-lib Laws compatible with applicative