A model checker that somehow cleverly handles external input and statespace.

Lacking that, haskell's type system :D