[Haskell-cafe] model checking for (subset of) concurrent Haskell?

[Johannes Waldmann]

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.