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

PR #43794

three CLI crash bugs fixed upstream in vLLM

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; three division-by-zero crashes (--block-size 0, --hash-block-size 0, --max-model-len 0) were confirmed and fixed upstream in PR #43794, with three further config-validation gaps filed and open.

Read full case study

Chromium Dashboard

2026

of 10 live findings confirmed and fixed upstream by Google (PR #6451, PR #6452)

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; the chromium-dashboard maintainers at Google confirmed and fixed two of the findings upstream in PR #6451 and PR #6452.

Read full case study

Your project could be next

Get in touch