News
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
Old News
02/09/2022 ESBMC v7.0 released for all platforms. 30/12/2020 ESBMC v6.7 for all platforms. 30/12/2020 ESBMC v6.6 for Linux and MacOS released. 30/12/2020 ESBMC has successfully participated at the 10th Intl. Competition on Software Verification held at TACAS 2021 in Luxembourg. ESBMC won first place in the ReachSafety-XCSP subcategory. Second place in the SoftwareSystems-AWS-C-Common-ReachSafety, ReachSafety-ECA, and ReachSafety-Arrays subcategories. Fourth place in the ReachSafety category. Fifth place in the SoftwareSystems category. Overall, the sixth place among 25 state-of-the-art software verifiers at SV-COMP 2021!
December 7, 2025