Proven in production

Case Studies

ESBMC has been applied to firmware, blockchain infrastructure, and systems software at some of the world's leading technology organisations. Here's what we found, and what it meant.

Intel

2021–2025

1,500%

verification speedup

Semiconductor · Firmware

Scalable Formal Verification of Firmware

On a representative Intel firmware code pattern, our VO-GCSE optimisation cut ESBMC verification time from 105 seconds to under 7 seconds; interval analysis then made Intel's 190,000-LOC Core Power Management firmware verifiable in 8 hours (versus a 3-day timeout).

Read full case study

Arm

2022–2024

additional property violations found

Hardware · Confidential Computing

Securing the Arm Confidential Computing Architecture

In a SAS 2024 collaboration with engineers from Arm, ESBMC identified 23 additional property violations in the Realm Management Monitor firmware on top of those already detected by CBMC, strengthening the assurance baseline of the published RMM implementation.

Read full case study

Ethereum Foundation

2023–2024

PR #3600

fix merged upstream

Blockchain · Python

Reporting an integer_squareroot Bug in the Ethereum Consensus Specification

Using ESBMC-Python, the first BMC-based Python code verifier, we identified a division-by-zero in the integer_squareroot helper of the Ethereum consensus specification. The fix was merged upstream as ethereum/consensus-specs PR #3600. Published at ACM SIGSOFT ISSTA 2024.

Read full case study

verify-rust-std project

2024–2026

1 of 4

verification tools listed in the verify-rust-std book

Open-source ecosystem · Rust

ESBMC in the verify-rust-std Project

We won the Tool Applications track of the AWS-sponsored Rust standard library verification contest. ESBMC (via the GOTO Transcoder) is now one of four verification tools listed in the model-checking/verify-rust-std book, alongside Kani, VeriFast and Flux, and runs in the project's CI workflow.

Read full case study

NVIDIA OpenSMA

2026

F-1

OOB write confirmed and fixed upstream by NVIDIA

Data-centre firmware · C++23

Verifying NVIDIA OpenSMA Firmware with ESBMC

In a PoC verifying ~30 production C++23 modules of NVIDIA's open-source MCXN556S System Management Agent firmware, ESBMC identified 17 distinct findings, including a Tier-A out-of-bounds write in the MCTP validator that NVIDIA's OpenSMA team confirmed and fixed upstream on 2026-05-11. 22+ ESBMC frontend issues were merged in the course of the work.

Read full case study

AWS Neuron (NKI)

2026

new nki-samples division-by-zero bugs filed by the PoC and fixed by AWS

AI accelerators · Python kernels

Verifying AWS Neuron NKI Kernels with ESBMC

A reproducible PoC showing that AWS Neuron Kernel Interface (NKI) kernels for Trainium and Inferentia can be statically verified by ESBMC's Python frontend without Neuron hardware. 19 kernels port to a single ~865-LoC stub library, 11 of 13 symbolic targets carry k-induction completeness certificates, and the PoC filed two new division-by-zero bugs that AWS confirmed and fixed upstream (nki-samples PR #126 and commit bb513ac), on top of rediscovering the PR #74 matmul shape bug in ~2 seconds.

Read full case study

vLLM

2026

6 of 7

CLI-reachable findings fixed upstream in vLLM (PR #43794, PR #44070)

LLM inference · Python

Verifying vLLM Configuration Arithmetic with ESBMC

A reproducible PoC applying ESBMC's Python frontend to vLLM's integer and index arithmetic, the high-throughput LLM inference engine. Across 31 tiered targets (~4 min end-to-end), ESBMC surfaced seven CLI-reachable defects; six have been confirmed and fixed upstream, three division-by-zero crashes (--block-size 0, --hash-block-size 0, --max-model-len 0) in PR #43794 and two silent-acceptance defects in PR #44070, leaving one gap open. A further programmatic-only finding was fixed in PR #44207.

Read full case study

Chromium Dashboard

2026

of 7 issues filed on Google's tracker fixed upstream (PR #6451, PR #6452, PR #6656)

Developer infrastructure · Python

Verifying Google's Chromium Dashboard with ESBMC

A reproducible PoC applying ESBMC's Python frontend to chromium-dashboard, the Google App Engine backend behind Chrome Platform Status. Across 48 targets in five tiers (under 30s end-to-end), ESBMC confirmed ten live API-validation findings and formally proved two security invariants sound; seven findings were filed as issues on Google's public tracker and the chromium-dashboard maintainers fixed three of those upstream in PR #6451, PR #6452 and PR #6656.

Read full case study

AWS SDK for C++ · Base64

2026

2 CVEs

memory-safety issues fixed by AWS (CVE-2026-19642, CVE-2026-19643)

Cloud SDK · C++

Two Base64 Memory-Safety CVEs in the AWS SDK for C++

We verified the hand-written Base64 decoder in the AWS SDK for C++ with ESBMC, driving it with symbolic inputs rather than individual test strings. The analysis uncovered out-of-bounds behaviour in the decoder's length arithmetic, reachable from a class of well-formed inputs. AWS published security bulletin 2026-080 for CVE-2026-19642 (out-of-bounds write) and CVE-2026-19643 (out-of-bounds read), both rated medium and fixed in SDK 1.11.862.

Read full case study

AWS SDK for C++ · DateTime

2026

PR #3896

two DateTime parser bugs confirmed and fixed by AWS in SDK 1.11.877

Cloud SDK · C++

Two DateTime Parser Bugs in the AWS SDK for C++

Returning to the same SDK, we verified its RFC822, ISO-8601 and ISO-8601 Basic timestamp parsers with ESBMC. Two defects surfaced: delimiter-driven fields accumulated digits without bound, overflowing their int accumulators (undefined behaviour), and out-of-range dates were converted without a range check and returned to the caller as successful parses. AWS confirmed both, took our field-width patch, and shipped the fix in PR #3896 (SDK 1.11.877) with 12 new regression tests.

Read full case study

Your project could be next

Get in touch