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:

| Solver | From | | Solver | From | |--------|------|-|--------|------| | ABC | Berkeley | | DReal | CMU | | Bitwuzla | Stanford | | MathSAT | FBK / Trento | | Boolector | JKU | | OpenSMT | USI | | CVC4 | Stanford / Iowa | | Yices | SRI | | CVC5 | Stanford / Iowa | | Z3 | Microsoft |

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:

| Example | Description | |---------|-------------| | Sudoku | Solve Sudoku puzzles using SMT constraints | | N-Queens | Solve the N-Queens placement puzzle | | SEND + MORE = MONEY | The classic cryptarithmetic puzzle | | Fish/Zebra | Einstein's logic puzzle | | SQL Injection | Find inputs that cause SQL injection vulnerabilities | | Regex Crossword | Solve regex crossword puzzles | | BitTricks | Verify bit-manipulation tricks from Stanford's bithacks collection | | Legato multiplier | Correctness proof of Legato's 8-bit multiplier | | Prefix sum | Ladner-Fischer prefix-sum implementation proof | | AES | AES encryption with C code generation | | CRC | Symbolic CRC computation with C code generation | | Sqrt2 irrational | Prove that the square root of 2 is irrational | | Sorting | Prove insertion sort, merge sort, and quick sort correct | | Kadane | Prove Kadane's maximum segment-sum algorithm correct | | McCarthy91 | Prove McCarthy's 91 function meets its specification | | [Binary search](http://hackage.haskell.org