sbv: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

[ bit-vectors, bsd3, formal-methods, library, math, smt, symbolic-computation, theorem-provers ] [ Propose Tags ]
Versions 0.9, 0.9.1, 0.9.2, 0.9.3, 0.9.4, 0.9.5, 0.9.6, 0.9.7, 0.9.8, 0.9.9, 0.9.10, 0.9.11, 0.9.12, 0.9.13, 0.9.14, 0.9.15, 0.9.16, 0.9.17, 0.9.18, 0.9.19, 0.9.20, 0.9.21, 0.9.22, 0.9.23, 0.9.24, 1.0, 1.1, 1.2, 1.3, 1.4, 2.0, 2.1, 2.2, 2.3, 2.4, 2.5, 2.6, 2.7, 2.8, 2.9, 2.10, 3.0, 3.1, 3.2, 3.3, 3.4, 3.5, 4.0, 4.1, 4.2, 4.3, 4.4, 5.0, 5.1, 5.2, 5.3, 5.4, 5.5, 5.6, 5.7, 5.8, 5.9, 5.10, 5.11, 5.12, 5.13, 5.14, 5.15, 6.0, 6.1, 7.0, 7.1, 7.2, 7.3, 7.4, 7.5, 7.6 (info)
Change log
Dependencies array, base (==4.*), containers, deepseq, directory, filepath, HUnit, mtl, old‑time, pretty, process, QuickCheck, random, sbv, syb [details]
License BSD-3-Clause
Copyright Levent Erkok, 2010-2013
Author Levent Erkok
Maintainer Levent Erkok (
Category Formal Methods, Theorem Provers, Bit vectors, Symbolic Computation, Math, SMT
Home page
Bug tracker
Source repo head: git clone git://
Uploaded by LeventErkok at Fri Mar 22 04:25:22 UTC 2013
Distributions Arch:7.6, Debian:5.9, LTSHaskell:7.5, NixOS:7.5, openSUSE:7.4
Executables SBVUnitTests
Downloads 24171 total (292 in the last 30 days)
Rating 2.5 (votes: 5) [estimated by rule of succession]
Your Rating
  • λ
  • λ
  • λ
Status Docs uploaded by user
Build status unknown [no reports yet]
Hackage Matrix CI

Express properties about Haskell programs and automatically prove them using SMT (Satisfiability Modulo Theories) solvers. Automatically generate C programs from Haskell functions. The SBV library adds support for symbolic bit vectors and other symbolic types, allowing formal models of Haskell programs to be created.

  $ ghci -XScopedTypeVariables
  Prelude> :m Data.SBV
  Prelude Data.SBV> prove $ \(x::SWord8) -> x `shiftL` 2 .== 4*x
  Prelude Data.SBV> prove $ forAll ["x"] $ \(x::SWord8) -> x `shiftL` 2 .== x
  Falsifiable. Counter-example:
    x = 128 :: SWord8

You can pick the SMT solver you want to use by importing the appropriate module. The SBV library currently works with the the following SMT solvers:

import Data.SBV
Picks the default solver, which is currently set to be Z3. (Might change in the future!)
import Data.SBV.Bridge.Z3
Picks Z3 from Microsoft (
import Data.SBV.Bridge.Yices
Picks Yices from SRI (
import Data.SBV.Bridge.CVC4
Picks CVC4 from New York University and the University of Iowa (
import Data.SBV.Bridge.Boolector
Picks Boolector from Johannes Kepler University at (

SBV introduces the following types and concepts:

Functions built out of these types can be:

Predicates can have both existential and universal variables. Use of alternating quantifiers provides considerable expressive power. Furthermore, existential variables allow synthesis via model generation.

The SBV library can also compile Haskell functions that manipulate symbolic values directly to C, rendering them as straight-line C programs.

In addition to the library, the installation will create the executable SBVUnitTests. You should run it once the installation is complete, to make sure the unit tests are run and all is well.

SBV is hosted at GitHub: Comments, bug reports, and patches are always welcome.

The following people reported bugs, provided comments/feedback, or contributed to the development of SBV in various ways: Ian Blumenfeld, Ian Calvert, Iavor Diatchki, John Erickson, Tom Hawkins, Lee Pike, Austin Seipp, Don Stewart, Josef Svenningsson, and Nis Wegmann.

Release notes can be seen at:

[Skip to Readme]




Maintainer's Corner

For package maintainers and hackage trustees

Readme for sbv-2.10

[back to package description]

SBV: SMT Based Verification in Haskell

Please see: