Hello all, I'm happy to announce the first public release of sbvPlugin, a new GHC-core plugin based on the SBV library: http://hackage.haskell.org/package/sbvPlugin The plugin can be used to prove (or refute!) theorems in your Haskell code, using the SBV library as its backend. Here's a most simple example: {-# OPTIONS_GHC -fplugin=Data.SBV.Plugin #-} module Test where import Data.SBV.Plugin {-# ANN test theorem #-} test :: Integer -> Integer -> Bool test x y = x + y >= x - y When compiled (or loaded into ghci), you'll see that the plugin will attempt to prove the given theorem, and will produce a counter-example since it is not valid! (This assumes, you've installed an SBV-supported SMT solver. Z3 from Microsoft is a good choice: http://github.com/Z3Prover/z3) http://github.com/Z3Prover/z3 The plugin is still in its early days and the examples are rather sparse. But see the following for one worked out instance: (Thanks to Anthony Cowley for the original idea.) http://hackage.haskell.org/package/sbvPlugin/docs/Data-SBV-Plugin-Examples-M... The sbvPlugin takes advantage of the SBV library ( http://hackage.haskell.org/package/sbv) to directly reason about Haskell programs at GHC's core level. However, the plugin is *not* a replacement for SBV. It only exposes a few features of SBV directly at the Haskell level; which hopefully makes it useful and more friendly than SBV; but it is neither intended nor possible for it to replace the SBV library itself. In particular, the plugin is limited to certain types (mostly numeric), and a few composite ones (lists and tuples.) If the plugin does not "understand" a Haskell type/expression, it'll use a technique called "uninterpretation" to black-box it. In those cases, the counter-examples produced might be bogus, though proofs will still be valid. Note that any definitions that are outside of the module being compiled will also go uninterpreted, including all the Prelude functions. The plugin is still in its early days, and there are a number of rough edges. Any feedback is most welcome! Happy hacking, -Levent.