esbmc-linter

Pre-commit hooks for ESBMC, the Efficient SMT-based Context-Bounded Model Checker.

ESBMC automatically detects runtime errors in C, C++, Python, and Solidity programs using formal verification. It can find buffer overflows, null-pointer dereferences, memory leaks, arithmetic overflows, deadlocks, data races, and more -- or prove their absence within a bounded execution depth.

Prerequisites

ESBMC must be installed and available on your PATH. Install it via one of:

Ubuntu (PPA):

sudo add-apt-repository ppa:esbmc/esbmc
sudo apt update
sudo apt install esbmc

Pre-built binaries:

Download from the ESBMC releases page.

Build from source:

See the ESBMC build instructions.

Verify your installation:

esbmc --version

Quick Start

Add to your .pre-commit-config.yaml:

repos:
  - repo: https://github.com/esbmc/esbmc-linter
    rev: v0.1.0
    hooks:
      - id: esbmc

Then install and run:

pre-commit install
pre-commit run --all-files

Available Hooks

Hook ID	Description	File Types	Extra Checks
esbmc	General safety verification	C, C++	Default checks (bounds, pointer, div-by-zero, alignment, UB-shift)
esbmc-memory	Memory safety	C, C++	Default + memory leak detection
esbmc-overflow	Arithmetic overflow	C, C++	Default + signed overflow/underflow
esbmc-python	Python verification	Python	Default checks
esbmc-solidity	Smart contract verification	Solidity (.sol)	Default checks

All hooks apply these defaults (unless you override them):

• --incremental-bmc -- efficient bounded model checking strategy
• --unwind 5 -- unwind loops up to 5 iterations
• --timeout 60 -- 60-second timeout per file

ESBMC's built-in default checks are always active unless explicitly disabled: array bounds, pointer safety, division by zero, pointer alignment, scanf overflow, VLA size overflow, and undefined-behavior shift operations.

Configuration

Custom flags

Pass any ESBMC flag via args. These are forwarded directly to the esbmc binary:

hooks:
  - id: esbmc
    args: [--unwind, "10", --overflow-check, --memory-leak-check]

Solver selection

ESBMC supports multiple SMT solvers. Select one with:

hooks:
  - id: esbmc
    args: [--z3]

Available solvers: --z3, --boolector, --bitwuzla, --mathsat, --cvc4, --cvc5, --yices.

Deeper analysis

Increase the unwind bound and timeout for more thorough (but slower) verification:

hooks:
  - id: esbmc
    args: [--unwind, "20", --timeout, "300"]

Multiple hooks

Combine hooks for layered checking:

hooks:
  - id: esbmc
  - id: esbmc-memory
  - id: esbmc-overflow

Restrict to specific directories

hooks:
  - id: esbmc
    files: ^src/safety_critical/

Disable specific default checks

hooks:
  - id: esbmc
    args: [--no-bounds-check, --no-pointer-check]

Or disable all default checks and enable only what you need:

hooks:
  - id: esbmc
    args: [--no-standard-checks, --overflow-check]

k-induction (unbounded verification)

For proving properties without a bound:

hooks:
  - id: esbmc
    args: [--k-induction, --max-k-step, "50"]

Concurrency checks

For multi-threaded C/C++ programs using pthreads:

hooks:
  - id: esbmc
    args: [--deadlock-check, --data-races-check]

Environment Variables

Variable	Description
ESBMC_PATH	Explicit path to the esbmc binary (overrides PATH lookup)
ESBMC_CONFIG_FILE	Path to an ESBMC TOML config file (set to empty string to disable)
ESBMC_OPTS	Additional ESBMC options (lowest priority, parsed as shell tokens)

ESBMC also reads ~/.config/esbmc.toml by default for persistent configuration.

Hook-Specific Options

The wrapper accepts these options (separate from ESBMC flags):

Option	Description
--version	Print esbmc-linter and esbmc versions
--esbmc-path PATH	Explicit path to the esbmc binary

ESBMC Property Reference

Enabled by default

Flag to disable	Property
--no-bounds-check	Array bounds
--no-pointer-check	Pointer safety (null, dangling, double-free)
--no-div-by-zero-check	Division by zero
--no-align-check	Pointer alignment
--no-ub-shift-check	Undefined behavior on shifts
--no-unlimited-scanf-check	scanf/fscanf buffer overflow
--no-vla-size-check	VLA size overflow

Opt-in

Flag to enable	Property
--overflow-check	Signed arithmetic overflow
--unsigned-overflow-check	Unsigned arithmetic overflow
--memory-leak-check	Memory leaks
--nan-check	Floating-point NaN
--deadlock-check	Deadlocks
--data-races-check	Data races
--lock-order-check	Lock ordering
--atomicity-check	Atomicity violations
--struct-fields-check	Over-sized struct field reads

Troubleshooting

"esbmc not found on PATH"

ESBMC must be installed separately. See Prerequisites.

Verification takes too long / hangs

Reduce the unwind bound or timeout:

args: [--unwind, "3", --timeout, "30"]

False positives on malloc

If your code assumes malloc never fails:

args: [--force-malloc-success]

Need more verbose output

args: [--verbosity, "6"]

License

Apache License 2.0 -- same as ESBMC.