ESBMC (the Efficient SMT-based Context-Bounded Model Checker) is a mature, permissively licensed open-source context-bounded model checker that automatically detects or proves the absence of runtime errors in single- and multi-threaded C, C++, CUDA, CHERI, Kotlin, Python, and Solidity programs. It can automatically verify predefined safety properties (e.g., bounds check, pointer safety, overflow) and user-defined program assertions.
ESBMC supports: The Clang compiler as its C/C++/CHERI/CUDA frontend; The Soot framework via Jimple as its Java/Kotlin frontend; The ast and ast2json modules as its Python frontend; Implements the Solidity grammar production rules as its Solidity frontend; Supports IEEE floating-point arithmetic for various SMT solvers. ESBMC also implements state-of-the-art incremental BMC and k-induction proof-rule algorithms based on Satisfiability Modulo Theories (SMT) and Constraint Programming (CP) solvers.