The engine
ESBMC
The Efficient SMT-based Context-Bounded Model Checker — a production-grade formal verification tool with 50+ international competition awards (SV-COMP & Test-Comp, 2012–2026) and published industrial case studies at Intel, Arm, AWS, and the Ethereum Foundation.
Research provenance
An open-source tool, built in the open since 2008
ESBMC began in 2008 as part of Lucas Cordeiro's PhD research at the University of Southampton, and has been continuously developed since by an open community of contributors at Southampton, the Federal University of Amazonas, and — since 2018 — the University of Manchester. The tool is publicly available as open-source software on GitHub, and Cyber-Reasoning Consultancy (CRC)'s consultancy services are built around the same public ESBMC release used by the broader research community. CRC does not own ESBMC and does not claim exclusive rights to it; we contribute to and consult around an openly licensed tool.
Foundations
What is formal verification?
A structural engineer does not certify a bridge by driving one lorry across it. They apply mathematical analysis to reason about the bridge's behaviour under all loads. Formal software verification applies the same principle to code.
Traditional testing checks a finite set of scenarios. Formal verification uses mathematical logic to reason about every possible execution of a program — every input, every thread interleaving, every edge case — and either proves safety properties hold or produces a concrete counterexample showing exactly how they can fail.
ESBMC implements bounded model checking (BMC) and k-induction, encoding your program as a set of logical constraints and handing them to an SMT solver. The solver either confirms the constraints are satisfiable (finding a bug, with a counterexample trace) or proves them unsatisfiable — a formal correctness guarantee within the verification bound, extended to unbounded proofs via k-induction where applicable.
Parse source code
ESBMC parses C, C++, Rust, Python, and other supported languages into an internal GOTO intermediate representation.
Encode as SMT constraints
The program is unwound up to a configurable bound and encoded as Satisfiability Modulo Theories (SMT) formulae.
Hand to an SMT solver
An industrial SMT solver (Z3, Bitwuzla, etc.) determines whether a counterexample exists.
Report: proof or bug
ESBMC returns a formal safety certificate, or a concrete counterexample trace showing exactly how the bug is triggered.
Coverage
Supported languages
C / C++
Core target — full MISRA, AUTOSAR support
Python
ESBMC-Python: first SMT-based BMC for Python
Rust
Via GOTO Transcoder; runs in the verify-rust-std project CI
Solidity
Smart contract verification
CUDA
GPU kernel correctness
Kotlin / Java
Via Soot framework
CHERI C
Memory-safe hardware platform verification (research support)
Detection
Error classes detected
Backends
SMT solver support
ESBMC supports multiple industrial-grade SMT solvers, allowing it to select the best backend for each verification task. This flexibility is key to its performance on large codebases — as demonstrated by the Intel Core Power Management firmware (190,000 LOC) verified in under 8 hours.
Recognition
Awards & recognition
Distinguished Paper Award
ASE'24
Most Influential Paper Award
ASE'23
50+ category awards
SV-COMP & Test-Comp
See ESBMC in action
Read how ESBMC identified 23 additional property violations in Arm's RMM firmware on top of those already detected by CBMC, or explore our other industrial case studies.