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

~26 min

two-phase verification of 19 NKI kernels, 100% pass rate

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 harness rediscovers nki-samples PR #74 (matmul shape bug) in ~2 seconds.

Read full case study

Your project could be next

Get in touch