Testing

Property Verification Techniques: Beyond Unit Tests to Formal Guarantees

HelpMeTest

20 Aug 2026 — 6 min read

Unit tests verify specific behaviors on specific inputs. Property verification asks a different question: does this code satisfy a mathematical property for all inputs in a domain? The gap between these two approaches is the gap between "it worked on what I tested" and "it is correct."

This post covers the techniques that sit between unit testing and full theorem proving: invariants, contracts, abstract interpretation, symbolic execution, and SMT-based verification. These techniques scale to real codebases and catch classes of bugs that no amount of test coverage will find.

What Is a Property?

A property is a predicate over program states that should always hold. Unlike a test (which checks one specific case), a property holds universally:

Invariant: 0 <= account.balance — always true regardless of operations applied
Pre/postcondition: sorted(sort(list)) == true for all lists
Safety property: "the lock is never held by two threads simultaneously"
Liveness property: "every request eventually receives a response"

The verification technique you use depends on what kind of property you want to verify and how much time you're willing to spend.

Invariants: Enforced by Type Systems and Contracts

The cheapest form of property verification is encoding invariants in the type system.

Newtype Pattern

// Without invariant: any number is a valid percentage
function applyDiscount(price: number, discount: number): number {
    return price * (1 - discount);  // Bug: discount could be 1.5
}

// With invariant: enforce at boundary
type Percentage = number & { readonly __brand: "Percentage" };

function makePercentage(n: number): Percentage {
    if (n < 0 || n > 1) throw new Error(`Invalid percentage: ${n}`);
    return n as Percentage;
}

function applyDiscount(price: number, discount: Percentage): number {
    return price * (1 - discount);  // Discount is guaranteed 0-1
}

This is property verification by construction — you make invalid states unrepresentable.

Dependent Types for Stronger Invariants

Languages with dependent types (Idris, Agda, Lean) can express more:

-- A vector with length encoded in the type
data Vect : Nat -> Type -> Type where
  Nil  : Vect Z a
  (::) : a -> Vect n a -> Vect (S n) a

-- zip is only defined for same-length vectors
zip : Vect n a -> Vect n b -> Vect n (a, b)
zip Nil       Nil       = Nil
zip (x :: xs) (y :: ys) = (x, y) :: zip xs ys
-- Mismatched lengths are a compile error, not a runtime error

The type checker enforces the length property at compile time, eliminating an entire class of runtime errors.

Design by Contract: Pre/Postconditions

Design by Contract (DbC) attaches preconditions, postconditions, and invariants to functions:

Python with icontract

from icontract import require, ensure, invariant

@require(lambda x: x >= 0, "x must be non-negative")
@require(lambda n: n >= 1, "n must be at least 1")
@ensure(lambda result, x: result * result <= x + 0.0001)
@ensure(lambda result, x: result >= 0)
def integer_sqrt(x: float, n: int = 10) -> float:
    """Newton's method integer square root."""
    z = x / 2
    for _ in range(n):
        z = z - (z * z - x) / (2 * z)
    return z

Violations raise ViolationError at runtime with the failing condition and variable values.

Eiffel-style Invariants

@invariant(lambda self: self.balance >= 0, "Balance cannot go negative")
@invariant(lambda self: self.limit > 0, "Limit must be positive")
class BankAccount:
    def __init__(self, initial_balance: float, limit: float):
        self.balance = initial_balance
        self.limit = limit
    
    @require(lambda amount: amount > 0, "Amount must be positive")
    @ensure(lambda self, amount, OLD: self.balance == OLD.balance - amount)
    def withdraw(self, amount: float) -> None:
        if amount > self.balance:
            raise InsufficientFunds(f"Cannot withdraw {amount}, balance is {self.balance}")
        self.balance -= amount

Invariants are checked before and after every method call. If withdraw is buggy and doesn't maintain balance >= 0, you find out immediately.

Abstract Interpretation

Abstract interpretation analyzes program behavior by computing over abstract domains instead of concrete values. Instead of asking "what is the value of x?", it asks "what set of values can x take?"

Example: Interval Analysis

# Concrete execution
x = 3
y = x + 5   # y = 8

# Abstract execution (interval domain)
# x ∈ [0, 10]
# y = x + 5, so y ∈ [5, 15]

Static analyzers like Facebook's Infer and Microsoft's IKOS use abstract interpretation to find null pointer dereferences, buffer overflows, and integer overflows without running the code.

Running Infer on Java

# Install Infer
brew install infer  # macOS
# Or: https://fbinfer.com/docs/getting-started/

# Analyze a Java project
infer run -- javac MyClass.java

# Or with Gradle
infer run -- gradle build

Example output:

INFER_RESULTS:
./PaymentService.java:47: error: NULL_DEREFERENCE
  null dereference of `customer`
  47 |     return customer.getAccount().getBalance();
  
  Null is assigned at line 44:
  44 |     Customer customer = db.findCustomer(id);  // returns null if not found

Infer found a null pointer dereference without you writing a test — it statically analyzed all paths through findCustomer.

Running Infer on C/C++

# Capture build
infer capture -- make

# Analyze
infer analyze

# Check for memory leaks and null dereferences
infer report --issues-tests

Infer's separation logic engine can track heap ownership and detect use-after-free, double-free, and memory leaks.

Symbolic Execution

Symbolic execution runs programs with symbolic inputs rather than concrete values. Instead of x = 5, it uses x = α (any value). The execution engine tracks constraints on α and explores all paths.

KLEE: Symbolic Execution for C

#include <klee/klee.h>

int buggy_function(int x, int y) {
    int result = 0;
    if (x > 0) {
        result = 100 / y;  // potential division by zero
    }
    if (y == 0 && x > 0) {
        result = -1;  // dead code?
    }
    return result;
}

int main() {
    int x, y;
    klee_make_symbolic(&x, sizeof(x), "x");
    klee_make_symbolic(&y, sizeof(y), "y");
    
    buggy_function(x, y);
    return 0;
}

# Compile with KLEE instrumentation
clang -I /usr/include/klee -emit-llvm -c -g buggy.c -o buggy.bc

# Run symbolic execution
klee buggy.bc

KLEE explores all paths through buggy_function and finds that when x > 0 && y == 0, you hit a division by zero at 100 / y. It generates a concrete test case that triggers the bug.

Java Pathfinder (JPF)

import gov.nasa.jpf.annotation.*;

public class TransferService {
    
    @StateTracked
    public static void transfer(Account from, Account to, int amount) {
        // JPF explores all thread interleavings
        from.balance -= amount;
        to.balance += amount;
        
        // JPF will find the race condition here:
        // Thread 1: from.balance -= 100 (reads 500, writes 400)
        // Thread 2: from.balance -= 100 (reads 500, writes 400)  <- uses stale read
        // Result: balance should be 300 but is 400
    }
}

JPF's scheduling choice generator explores every possible thread interleaving, finding data races that would take millions of test runs to reproduce.

SMT Solvers for Property Verification

SMT (Satisfiability Modulo Theories) solvers check whether a logical formula can be satisfied. Z3 and CVC5 are the most popular. You can use them directly for property verification:

Z3 Python API

from z3 import *

# Verify: for all non-negative x, sqrt(x^2) == x
x = Real('x')
solver = Solver()

# Add negation of property (if UNSAT, property holds)
solver.add(x >= 0)
solver.add(Sqrt(x * x) != x)

result = solver.check()
if result == unsat:
    print("Property verified: sqrt(x^2) == x for all x >= 0")
elif result == sat:
    print("Counterexample found:", solver.model())

Verifying Array Properties

from z3 import *

# Verify that a simple bubble sort implementation is correct
def bubble_sort_spec(arr, n):
    """Specification: result is sorted"""
    result = [Int(f'r{i}') for i in range(n)]
    
    solver = Solver()
    
    # Assert result is sorted
    for i in range(n - 1):
        solver.add(result[i] <= result[i + 1])
    
    # Assert result is a permutation of input
    # (simplified: same multiset)
    for v in arr:
        count_in  = Sum([If(arr[j] == v, 1, 0) for j in range(n)])
        count_out = Sum([If(result[j] == v, 1, 0) for j in range(n)])
        solver.add(count_in == count_out)
    
    return solver.check() == sat  # Check that such a result exists

# Verify properties about integer overflow
n = 32  # 32-bit integers
a, b = BitVecs('a b', n)
solver = Solver()

# Check: does a + b ever overflow when both are positive?
solver.add(a > 0, b > 0)
solver.add(a + b < 0)  # addition overflowed

if solver.check() == sat:
    m = solver.model()
    print(f"Overflow: a={m[a]}, b={m[b]}, sum={m.eval(a+b)}")

Integration with Test Suites

Use Z3 to generate test cases covering edge cases automatically:

from z3 import *

def generate_edge_cases(function_constraints):
    """Generate test inputs that cover boundary conditions"""
    x = Int('x')
    cases = []
    
    # Get example satisfying each boundary
    for constraint, label in function_constraints:
        s = Solver()
        s.add(constraint(x))
        if s.check() == sat:
            cases.append((s.model()[x].as_long(), label))
    
    return cases

cases = generate_edge_cases([
    (lambda x: x < 0,       "negative"),
    (lambda x: x == 0,      "zero"),
    (lambda x: And(x > 0, x < 100),  "small positive"),
    (lambda x: x >= 100,    "large positive"),
])

for value, label in cases:
    print(f"Test case ({label}): {value}")

Choosing Your Verification Technique

Technique	Effort	Coverage	Best for
Type system invariants	Low	Compile-time	Data validity, state machines
Design by contract	Low-medium	Runtime	Function pre/postconditions
Property-based testing	Medium	Sampled	Algorithmic correctness
Abstract interpretation	Low (tooling)	Static	Null dereferences, overflows
Symbolic execution	Medium	Path-complete	Security-critical code
Model checking (SPIN/NuSMV)	High	State-complete	Protocols, concurrency
Theorem proving (Coq/Lean)	Very high	Mathematically complete	Critical algorithms

Start with type system invariants — they're free. Add contracts for critical functions. Use Infer for null dereference analysis in CI. Reach for SPIN or Z3 when you have a concurrency bug that tests can't reliably reproduce.

The goal isn't to apply every technique to every codebase. It's to match the verification method to the risk level. A bug in a billing service has different consequences than a bug in a loading spinner. Calibrate accordingly.