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

esbmc-verification