Hi, ImProve [1] is a little imperative DSL that compiles to C code. Intended for high assurance embedded applications, ImProve is also an infinite state, unbounded model checker. Meaning ImProve can verify assertions in a program will always be true. Here's an example: module Main where import Language.ImProve launchControl :: Stmt () launchControl = do presidentialAuthority <- input bool "presidentialAuthority" buttonPressed <- input bool "buttonPressed" launchMissiles <- bool' "launchMissiles" $ (presidentialAuthority ||. buttonPressed) assert "conditionsToLaunch" $ launchMissiles ==. (presidentialAuthority &&. buttonPressed) main :: IO () main = verify "yices" 20 launchControl Running this program yields: verifying conditionsToLaunch FAILED: disproved basis in k = 1 (see trace) On verification failures, ImProve will emit a counter example showing the violation, which is essentially a program trace showing how things could go wrong. In this case, the trace looks like this: initialize launchMissiles := false cycle 0 input presidentialAuthority <== true input buttonPressed <== false launchMissiles <== true assertion FAILED: conditionsToLaunch This basically means Barack was somehow able to launch on his own. (Man! I even voted for the guy!) Under the hood, ImProve uses Yices [2] for SMT solving, and a method of unbounded model checking known as k-induction. Don't expect too much from ImProve; it's a very restrictive language. It's basically three data types (bool, int, float), variables assignments, and 'if' statements. No procedures, no loops, no arrays, no pointers, etc. However, it can still do interesting things -- especially with Haskell combinators in play. Hope you find it useful. And as always, questions, comments, and feedback welcome. -Tom [1] http://hackage.haskell.org/package/improve [2] http://yices.csl.sri.com/