For model checking concurrent and distributed imperative programs, there's the Promela language, and the Spin model checker ( http://spinroot.com ) than can explore/enumerate a finite state space of a system and decide validity of LTL formulae. Is there something similar for Haskell models of concurrency? Ideally, some subset of Haskell (containing enough of Control.Concurrent.*) as an alternative for Promela. It should even be possible to put the model checking in an alternative implementation of respective monad (STM, IO for MVars) so the whole thing is an embedded DSL. somewhat related: this project is about a verified model checker: https://cava.in.tum.de/ (ML code generated from Isabelle) but my interest is in model-checking concurrent programs in functional notation. - J.W.