SBV: SMT Based Verification in Haskell

Express properties about Haskell programs and automatically prove them using SMT solvers.

Hackage | Release Notes | Documentation

SBV provides symbolic versions of Haskell types. Programs written with these types can be automatically verified, checked for satisfiability, optimized, or compiled to C — all via SMT solvers.

SBV in 5 Minutes

Fire up GHCi with SBV:

$ cabal repl --build-depends sbv

For unbounded integers, x + 1 .> x is always true:

ghci> :m Data.SBV
ghci> prove $ \x -> x + 1 .> (x :: SInteger)
Q.E.D.

But with machine arithmetic, overflow lurks:

ghci> prove $ \x -> x + 1 .> (x :: SInt8)
Falsifiable. Counter-example:
  s0 = 127 :: Int8

IEEE-754 floats break reflexivity of equality:

ghci> prove $ \x -> (x :: SFloat) .== x
Falsifiable. Counter-example:
  s0 = NaN :: Float

What's the multiplicative inverse of 3 modulo 256?

ghci> sat $ \x -> x * 3 .== (1 :: SWord8)
Satisfiable. Model:
  s0 = 171 :: Word8

Use quantifiers for named results:

ghci> sat $ skolemize $ \(Exists @"x" x) (Exists @"y" y) -> x * y .== (96::SInteger) .&& x + y .== 28
Satisfiable. Model:
  x = 24 :: Integer
  y =  4 :: Integer

Optimize a cost function subject to constraints:

ghci> :{
optimize Lexicographic $ do x <- sInteger "x"
                            y <- sInteger "y"
                            constrain $ x + y .== 20
                            constrain $ x .>= 5
                            constrain $ y .>= 5
                            minimize "cost" $ x * y
:}
Optimal in an extension field:
  x    =  5 :: Integer
  y    = 15 :: Integer
  cost = 75 :: Integer

For inductive proofs and equational reasoning, SBV includes a theorem prover:

revApp :: forall a. SymVal a => TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool))
revApp = induct "revApp"
                 (\(Forall xs) (Forall ys) -> reverse (xs ++ ys) .== reverse ys ++ reverse xs) $
                 \ih (x, xs) ys -> [] |- reverse ((x .: xs) ++ ys)
                                      =: reverse (x .: (xs ++ ys))
                                      =: reverse (xs ++ ys) ++ [x]
                                      ?? ih
                                      =: (reverse ys ++ reverse xs) ++ [x]
                                      =: reverse ys ++ (reverse xs ++ [x])
                                      =: reverse ys ++ reverse (x .: xs)
                                      =: qed

ghci> runTP $ revApp @Integer
Inductive lemma: revApp
  Step: Base                            Q.E.D.
  Step: 1                               Q.E.D.
  Step: 2                               Q.E.D.
  Step: 3                               Q.E.D.
  Step: 4                               Q.E.D.
  Step: 5                               Q.E.D.
  Result:                               Q.E.D.
Functions proven terminating: sbv.reverse
[Proven] revApp :: Ɐxs ∷ [Integer] → Ɐys ∷ [Integer] → Bool

Features

Symbolic types — Booleans, signed/unsigned integers (8/16/32/64-bit and arbitrary-width), unbounded integers, reals, rationals, IEEE-754 floats, characters, strings, lists, tuples, sums, optionals, sets, enumerations, algebraic data types, and uninterpreted sorts.

Verification — prove/sat/allSat for property checking and model finding, safe/sAssert for assertion verification, dsat/dprove for delta-satisfiability, and QuickCheck integration.

Optimization — Minimize/maximize cost functions subject to constraints via optimize/maximize/minimize, with support for lexicographic, independent, and Pareto objectives.

Quantifiers and functions — Universal and existential quantifiers (including alternating), with skolemization for named bindings. Define SMT-level functions directly from Haskell via smtFunction, including recursive and mutually recursive definitions with automatic termination checking.

Theorem proving (TP) — Semi-automated inductive proofs (including strong induction) with equational reasoning chains. Includes termination checking, recursive and mutually recursive definitions, productive (co-recursive) functions, and user-defined measures.

Code generation — Compile symbolic programs to C as straight-line programs or libraries (compileToC, compileToCLib), and generate test vectors (genTest).

SMT interaction — Incremental mode via runSMT/query for programmatic solver interaction with a high-level typed API. Run multiple solvers simultaneously with proveWithAny/proveWithAll.

Algebraic Data Types

User-defined algebraic data types — including enumerations, recursive, and parametric types — are supported via mkSymbolic, with pattern matching via sCase (and its proof counterpart pCase):

{-# LANGUAGE QuasiQuotes     #-}
{-# LANGUAGE TemplateHaskell #-}

import Data.SBV

data Expr a = Val a
            | Add (Expr a) (Expr a)
            | Mul (Expr a) (Expr a)
            deriving Show

-- Make Expr symbolically available, named SExpr
mkSymbolic [''Expr]

eval :: SymVal a => (SBV a -> SBV a -> SBV a) -> (SBV a -> SBV a -> SBV a) -> SBV (Expr a) -> SBV a
eval add mul = smtFunction "eval" $ \e ->
    [sCase| e of
       Val v   -> v
       Add x y -> eval add mul x `add` eval add mul y
       Mul x y -> eval add mul x `mul` eval add mul y
    |]

The sCase construct supports nested pattern matching, as-patterns, guards, and wildcards, making programming with algebraic data types natural. Plain case expressions inside sCase are automatically treated as symbolic case-splits. The pCase variant provides the same features for proof case-splits in the theorem proving context.

Supported SMT Solvers

SBV communicates with solvers via the standard SMT-Lib interface:

Z3 is the default solver. Use proveWith, satWith, etc. to select a different one (e.g., proveWith cvc5). See tested versions for details. Other SMT-Lib compatible solvers can be hooked up with minimal effort — get in touch if you'd like to use one not listed here.

A Selection of Examples

SBV ships with many worked examples. Here are some highlights:

Browse the full collection in Documentation.SBV.Examples on Hackage.

License

SBV is distributed under the BSD3 license. See COPYRIGHT and LICENSE for details.

Please report bugs and feature requests at the GitHub issue tracker.

Thanks

The following people made major contributions to SBV, by developing new features and contributing to the design in significant ways: Joel Burget, Brian Huffman, Brian Schroeder, and Jeffrey Young.

The following people reported bugs, provided comments/feedback, or contributed to the development of SBV in various ways: Andreas Abel, Ara Adkins, Andrew Anderson, Kanishka Azimi, Markus Barenhoff, Reid Barton, Ben Blaxill, Ian Blumenfeld, Guillaume Bouchard, Martin Brain, Ian Calvert, Oliver Charles, Christian Conkle, Matthew Danish, Iavor Diatchki, Alex Dixon, Robert Dockins, Thomas DuBuisson, Trevor Elliott, Gergő Érdi, John Erickson, Richard Fergie, Adam Foltzer, Joshua Gancher, Remy Goldschmidt, Jan Grant, Brad Hardy, Tom Hawkins, Greg Horn, Jan Hrcek, Georges-Axel Jaloyan, Anders Kaseorg, Tom Sydney Kerckhove, Lars Kuhtz, Piërre van de Laar, Pablo Lamela, Ken Friis Larsen, Andrew Lelechenko, Joe Leslie-Hurd, Nick Lewchenko, Brett Letner, Sirui Lu, Georgy Lukyanov, Martin Lundfall, Daniel Matichuk, John Matthews, Curran McConnell, Philipp Meyer, Fabian Mitterwallner, Joshua Moerman, Matt Parker, Jan Path, Matt Peddie, Lucas Peña, Matthew Pickering, Lee Pike, Gleb Popov, Rohit Ramesh, Geoffrey Ramseyer, Blake C. Rawlings, Jaro Reinders, Stephan Renatus, Dan Rosén, Ryan Scott, Eric Seidel, Austin Seipp, Andrés Sicard-Ramírez, Don Stewart, Greg Sullivan, Josef Svenningsson, George Thomas, May Torrence, Daniel Wagner, Sean Weaver, Robin Webbers, Eddy Westbrook, Nis Wegmann, Jared Ziegler, and Marco Zocca.

Thanks!