Verification of Haskell Code

Niki Vazou

(University of Maryland)

LiquidHaskell: Verification of Haskell Code

Motivation: Why verification?

Software bugs are Everywhere

“Airbus A400M crashed due to a software bug.”

— May 2015


Software bugs are Everywhere

Heartbleed: a security bug in the OpenSSL cryptography library.”

— April 2014

The Heartbleed Bug.

Goal: Make Bugs Difficult to Express

Using Modern Programming Languages (e.g., Haskell, Scala, Ocaml, F#).

Because of Strong Types & Lambda Calculus.

Via compile-time sanity checks

Lambda Man.

Fact Check: Haskell VS. Heartbleed

Haskell vs Heartbleed

How The Heartbleed Bug Works

How The Heartbleed Bug Works

The Heartbleed Bug in Haskell

λ> :m +Data.Text Data.Text.Unsafe
λ> let text = pack "HAT"
λ> :t takeWord16
    takeWord16 :: Int -> Text -> Text

True is a bad argument

λ> takeWord16 True text

    Couldn't match expected type ‘Int’ with actual type ‘Bool’
    In the first argument of ‘takeWord16’, namely ‘True’
    In the expression: takeWord16 True text

But, 10 is a good argument

Reveal 6 extra characters...
λ>  takeWord16 10 text

More Bugs: Partial Functions

λ> :t head
head :: [a] -> a

λ> head "Hawai'i"

λ> head []
*** Exception: Prelude.head: empty list

More Bugs: Termination

λ> fib 4
λ> fib 42

Goal: Extend Type System

  • To prevent wider class of errors

  • To enforce program specific properties


  1. Refinements Types
  2. Data Types
  3. Termination


  1. Refinements: Types + Predicates
  2. Subtyping: SMT Implication
  3. Measures: Specify Properties of Data
  4. Termination: Use Logic to Prove Termination


  • Diverse Code Bases

  • 20KLoc

  • Memory Safety, Termination, Functional Correctness, Program Equivalence

  • Specifications: 1 / 10 LOC


Liquid Types: Automated Verification via SMT

Properties: Predicates + Types
Proofs: SMT Solvers + Subtyping

Thank You!

online demo @