esbmc-verification

ESBMC Verification Skill

ESBMC (Efficient SMT-based Context-Bounded Model Checker) detects bugs or proves their absence in C, C++, CUDA, CHERI-C, Python, Solidity, Java, and Kotlin programs.

Prerequisites Check

Before running any ESBMC command, verify that ESBMC is installed by running which esbmc or esbmc --version. If ESBMC is not found, inform the user and provide installation instructions:

• Pre-built binaries: Download from ESBMC releases
• Build from source: Clone https://github.com/esbmc/esbmc and follow the build instructions in its README
• After installing, ensure esbmc is in the PATH: export PATH=$PATH:/path/to/esbmc/bin

Do not proceed with verification commands until ESBMC is confirmed available.

Verification Pipeline

Source Code → Frontend Parser → GOTO Program → Symbolic Execution (SSA) → SMT Formula → Solver → Result

Quick Start

# C file with default checks
esbmc file.c

# C++ file
esbmc file.cpp

# Python (requires type annotations)
esbmc file.py

# Solidity contract
esbmc --sol contract.sol --contract ContractName

# Common safety checks
esbmc file.c --memory-leak-check --overflow-check --unwind 10 --timeout 60s

# Concurrency verification
esbmc file.c --deadlock-check --data-races-check --context-bound 2

Supported Languages

Language	Command	Notes
C	esbmc file.c	Default, Clang frontend
C++	esbmc file.cpp	C++11-20 via --std
Python	esbmc file.py	Requires type annotations, Python 3.10+
Solidity	esbmc --sol file.sol --contract Name	Smart contracts
CUDA	esbmc file.cu	GPU kernel verification
Java/Kotlin	esbmc file.jimple	Requires Soot conversion from .class

For language-specific options and examples, see references/language-specific.md.

Safety Properties

Default Checks (Always On)

• Array bounds: Out-of-bounds array access
• Division by zero: Integer and floating-point
• Pointer safety: Null dereference, invalid pointer arithmetic
• Assertions: User-defined assert() statements

Optional Checks (Enable Explicitly)

• --overflow-check / --unsigned-overflow-check: Integer overflow
• --memory-leak-check: Memory leaks
• --deadlock-check / --data-races-check: Concurrency safety
• --nan-check: Floating-point NaN
• --ub-shift-check: Undefined shift behavior
• --is-instance-check: Enable runtime isinstance assertions for annotated Python code

Disable Specific Checks

--no-bounds-check, --no-pointer-check, --no-div-by-zero-check, --no-assertions

For the full CLI reference, see references/cli-options.md.

Loop Invariants and Function Contracts

These features extend ESBMC beyond the reach of plain BMC — use them when BMC hits its scaling limits, not as a general replacement. Both are under active development; encourage users to try them.

When to recommend each

Situation	Recommend
Loop with small or known bound	--unwind N — simpler, counterexamples are confirmed bugs
Loop bound large / unbounded, BMC times out	--loop-invariant --ir
Function called once or twice	Plain BMC / k-induction
Function called many times, BMC times out	--enforce-contract + --replace-call-with-contract

What to tell the user before they start

• These are over-approximations — a verification failure may mean the abstraction needs refinement, not that the program has a real bug.
• Iteration is expected and normal. Guide the user through the refinement cycle rather than treating the first failure as a dead end.
• VERIFICATION SUCCESSFUL with a correct abstraction is a sound, trustworthy result.

For the refinement workflow, see references/loop-invariants.md and references/function-contracts.md.

Loop Handling

K-induction is an alternative strategy that bypasses loop discovery entirely — see the Strategy Selection section below. If you are using BMC instead, always start by discovering loops before choosing an unwind strategy. Never guess a bound with --unwind N.

# Step 1: discover all loops and their IDs
esbmc file.c --show-loops

Decision tree based on the output:

• No loops → no unwind flag needed; run without any unwind option
• Loops with apparent bounds (e.g., for (i = 0; i < N; i++)) → use per-loop bounds derived from the source:

  esbmc file.c --unwindset L1:N,L2:M
  

• Loops with unknown or dynamic bounds → use incremental BMC:

  esbmc file.c --incremental-bmc
  

Strategy Selection

Choose a high-level path before running any checks:

Path A — k-Induction (try first for proving correctness)

• No loop discovery needed.
• Detect CPU count: nproc on Linux, sysctl -n hw.ncpu on macOS.

• 4 CPUs → use --k-induction-parallel

• ≤4 CPUs → use --k-induction
• If k-induction succeeds → property is proved (unbounded result).
• If k-induction times out or returns UNKNOWN → fall back to Path B.

Path B — BMC (bounded, loop-aware)

• Run --show-loops, then choose --unwindset or --incremental-bmc per the Loop Handling decision tree above.

Verification Strategies

Goal	Strategy	Command
Loops with known bounds	BMC with unwindset	--unwindset L1:N,...
Unknown loop bounds	Incremental BMC	--incremental-bmc
Prove correctness (≤4 CPUs)	k-Induction	--k-induction
Prove correctness (>4 CPUs)	k-Induction parallel	--k-induction-parallel
All violations	Multi-property	--multi-property
Large programs	Incremental SMT	--smt-during-symex
Concurrent code	Context-bounded	--context-bound 3

For detailed descriptions of the strategies and their configurations, see references/verification-strategies.md.

Solver Selection

Always detect available solvers via --list-solvers rather than assuming one is present. Use the best available solver by priority: Boolector → Bitwuzla → Z3.

esbmc --list-solvers      # Detect available solvers
esbmc file.c --boolector  # Boolector (highest priority)
esbmc file.c --bitwuzla   # Bitwuzla (second priority)
esbmc file.c --z3         # Z3 (fallback)

If none of these solvers are available, ESBMC was built without solver support and verification cannot proceed.

ESBMC Intrinsics

Use these in the source code to guide verification.

Quick Reference

Purpose	C/C++	Python
Symbolic int	__ESBMC_nondet_int()	nondet_int()
Symbolic uint	__ESBMC_nondet_uint()	N/A
Symbolic bool	__ESBMC_nondet_bool()	nondet_bool()
Symbolic float	__ESBMC_nondet_float()	nondet_float()
Symbolic string	N/A	nondet_str()
Symbolic list	N/A	nondet_list()
Symbolic dictionary	N/A	nondet_dict()
Assumption	__ESBMC_assume(cond)	assume(cond)
Assertion	__ESBMC_assert(cond, msg)	esbmc_assert(cond, msg)
Atomic section	__ESBMC_atomic_begin/end()	N/A

Basic Usage

int x = __ESBMC_nondet_int();       // Symbolic input
__ESBMC_assume(x > 0 && x < 100);   // Constrain input
__ESBMC_assert(result >= 0, "msg");  // Verify property

x: int = nondet_int()
__ESBMC_assume(x > 0 and x < 100)
assert result >= 0, "msg"

For the step-by-step process of adding intrinsics to code, see references/adding-intrinsics.md. For the full intrinsics API, see references/intrinsics.md.

Output and Debugging

esbmc file.c                          # Counterexample shown on failure
esbmc file.c --witness-output w.graphml # Generate witness file
esbmc file.c --show-vcc               # Show verification conditions
esbmc file.c --generate-testcase      # Generate test from counterexample
esbmc file.py --generate-pytest-testcase            # Generate pytest

Resource Limits

esbmc file.c --timeout 300s   # Time limit
esbmc file.c --memlimit 4g    # Memory limit

Common Workflows

Bug Hunting

# Step 1: discover loops
esbmc file.c --show-loops
# Step 2a: known bounds
esbmc file.c --boolector --unwindset L1:N --timeout 60s
# Step 2b: unknown bounds
esbmc file.c --boolector --incremental-bmc --timeout 120s

Proving Correctness

# Step 1: detect CPUs
nproc   # Linux; use `sysctl -n hw.ncpu` on macOS

# Step 2a: >4 CPUs
esbmc file.c --boolector --k-induction-parallel --overflow-check

# Step 2b: ≤4 CPUs
esbmc file.c --boolector --k-induction --overflow-check

# Step 3: if k-induction times out or returns UNKNOWN, fall back to BMC
esbmc file.c --show-loops   # then use --unwindset or --incremental-bmc

Memory Safety Audit

esbmc file.c --boolector --unwindset L1:N --memory-leak-check

Concurrency Verification

esbmc threaded.c --boolector --deadlock-check --data-races-check --context-bound 2

For guidance on fixing verification failures, see references/fixing-failures.md.

Additional Resources

Reference Files

• references/cli-options.md — Complete CLI reference
• references/verification-strategies.md — Detailed strategy guide
• references/language-specific.md — Language-specific features and options
• references/intrinsics.md — Full ESBMC intrinsics API
• references/adding-intrinsics.md — Step-by-step guide for annotating code
• references/fixing-failures.md — Diagnosing and fixing verification failures
• references/loop-invariants.md — Loop invariant syntax, CLI flag, design guidelines, and debugging
• references/function-contracts.md — Function contract clauses, enforce/replace modes, when to use each, and examples

Example Files

• examples/memory-check.c — Memory safety verification (C)
• examples/overflow-check.c — Integer overflow detection (C)
• examples/concurrent.c — Concurrency verification (C)
• examples/cpp-verify.cpp — C++ verification (classes, STL, RAII)
• examples/python-verify.py — Python verification

Scripts

• scripts/quick-verify.sh — Quick verification wrapper
• scripts/full-audit.sh — Comprehensive security audit