News
Development Update: Late October 2026
The early-October update ended at the v8.6 release. Since then, 515 commits from 509 pull requests landed on master between 13 and 27 October; about three in five fix the Python front end. This update starts with the wrong verdicts in the verification engine, then covers Python, NumPy, C and C++, the operational models and the smaller front ends, and ends with a table of the new options. Wrong verdicts in the verification engine False proofs in the default configuration. A GNU case range, case lo ... hi:, matched only lo, so a value inside the range went to default. ESBMC missed bugs inside the range and raised false alarms on fallthrough. This program verified:
October 27, 2026
Development Update: Early October 2026
Following the late-September update, 222 commits (219 pull requests) landed on master between 1 and 13 October, ending with the v8.6 release. As before, most of the user-visible ones fix a wrong verdict, so this update starts there; the Python, C/C++, operational model and Ladder Diagram changes follow. Wrong verdicts in the verification engine False proofs under --k-induction. The inductive step havocked only the named variables a loop assigns, so storage the loop writes through a pointer — *p, p->f, a callee, memcpy — kept its pre-loop value, and the step proved properties that fail later in the loop:
October 13, 2026
Development Update: Late September 2026
Following the mid-September update, 145 commits landed on master between 20 September and 1 October. Most of the user-visible ones fix a wrong verdict, so this update starts there; the Python, C/C++ and Ladder Diagram front ends follow. Wrong verdicts in the verification engine False proofs in the default configuration. Three fixes this fortnight concern runs with no options at all. Interval-based guard pruning, which symbolic execution performs by default (--no-interval-symex-guard turns it off), tracked only assignments, assumes, declarations and DEAD; the writes symex performs itself — binding a call’s result or a callee’s parameters, returning into the caller’s left-hand side, a body-less call storing through a pointer, a recursive callee overwriting its caller’s locals — left stale intervals behind, and a loop guard was pruned as false. The issue’s program verified:
October 1, 2026
Development Update: Mid-September 2026
Following the early-September update, 231 commits landed on master between 4 and 20 September. Here are the changes a user will notice. The C++ standard-library headers ESBMC could not include. Because ESBMC compiles C++ with -nostdinc++, a header with no operational model is a PARSING ERROR on the #include alone, whether or not the program uses anything from it. Twenty headers closed that way this fortnight: <numbers> (#7638), <concepts> (#7639), <version> (#7647), <charconv> (#7649), <cfenv>, <cinttypes>, <cwctype> and six more C wrappers (#7799), <ratio> (#7804), <execution>, <codecvt> and <scoped_allocator> (#7909), <latch>, <semaphore> and <stop_token> (#7912), <flat_map>, <flat_set> and <syncstream> (#7914), and <regex> and <mdspan> (#7915). <ranges>, <format>, <print>, <coroutine>, <generator>, <barrier> and <stdfloat> are what remain.
September 20, 2026
Development Update: Early September 2026
Following the end-of-August update, about 120 pull requests landed on master between 26 August and 4 September. ESBMC is now at v8.5 (#7379). Here are the changes a user will notice. A Linux ARM64 release asset. #7229 adds esbmc-linux-armv8.zip as a fourth canonical release asset, built statically against LLVM 22, so it runs on any aarch64 Linux userspace. An armv8 leg now runs per PR as well. Four features are unavailable on that build — --32, Solidity, CVC5 and --goto-contractor — and interval analysis differs from x86_64; the Setup page lists each with its tracking issue.
September 4, 2026
Development Update: End of August 2026
A short follow-up to the late-August update: roughly 80 pull requests landed on master between 22 and 26 August. Here are the ones a user will notice. Bitwuzla now uses its native floating-point theory. #7022 implements the SMT floating-point theory on the Bitwuzla backend — the default solver — so floats are encoded with fp.add and friends instead of ESBMC’s own bit-vector lowering. On symbolic-input FP queries it measured 1.2–13× faster, and 303 FP-touching regression tests agree on every verdict. --fp2bv opts back into the old encoding; fmod/remainder keep a bit-vector round-trip because fp.rem is two orders of magnitude slower on the solver side. One known gap: the theory cannot represent the sign of a NaN (#7021).
August 26, 2026
Development Update: Late August 2026
A follow-up to the previous update: another 175 or so pull requests landed on master between 13 and 22 August. Here are the highlights. Every run names every property. #7064 prints the per-property ** Results: block on every run, not only under --multi-property, and --result-only no longer suppresses it — so esbmc --result-only file.c now names what it checked. Properties a single-property run never separated are reported NOT CHECKED rather than PASSED, since a run that stops at the first violation cannot decide the rest.
August 22, 2026
Development Update: August 2026
Development on ESBMC has been moving fast: around 80 pull requests were merged into master in the first two weeks of August alone. Here are the highlights. A user-facing esbmc.h header. #6932 ships include/esbmc.h, installed alongside the binary, which exposes the verification intrinsics under unprefixed names — ESBMC_assume, ESBMC_assert, ESBMC_nondet_int, and friends. Including the header under any other compiler is a hard error, so verification harnesses cannot silently compile to no-ops.
August 13, 2026
Docs Page Improvement
📚 We have given the ESBMC documentation a thorough cleanup. When the docs moved to this site, much of the content was carried over verbatim from the old wiki: one enormous documentation page that mixed every topic together, duplicated other pages, and was hard to navigate. We have reorganized it into something far easier to read. Build guide, by platform. The build guide is now a set of per-OS tabs — Ubuntu/Debian, Fedora, macOS, FreeBSD and Windows — where each tab is a self-contained sequence of steps with the optional bits tucked into collapsible sections. The duplicate Linux and Windows build pages that used to confuse contributors are gone.
June 6, 2026
New Website Announcement
🚀 Exciting News! We are pleased to announce our new ESBMC website. ESBMC 🔍 is a mature, permissively licensed open-source SMT-based bounded model checker for C, C++, Python, Rust, and Solidity programs, verifying both single and multi-threaded software and detecting bugs such as division by zero, pointer safety, overflow, memory leaks, and more. Before this update, the documentation and news was fragmented across several websites: ssvlab.github.io/esbmc github.com/esbmc/esbmc/wiki esbmc.github.io/esbmc The new site consolidates all documentation, tutorials, news, and downloads into a single, up-to-date location 📚🔗. We aim to keep this website as up-to-date as possible!
December 7, 2025