Formal Software Verification · ESBMC since 2008

Prove it.
Don't just test it.

We use formal verification — not just testing — to find the bugs other tools miss, and prove their absence in safety-critical software.

Our Services View Case Studies

Published case studies

Intel Arm Ethereum Foundation Rust Foundation AWS NVIDIA

1,500%

Speedup achieved for Intel firmware verification

Additional property violations ESBMC found in Arm's RMM firmware (SAS 2024)

PR #3600

Ethereum consensus-specs fix merged upstream after our ESBMC-Python report (ISSTA 2024)

F-1

Out-of-bounds write in NVIDIA OpenSMA confirmed and fixed upstream after our 2026 PoC

Why formal verification?

Testing is sampling.
Formal verification is proof.

Testing checks the cases you think of. Formal verification checks every possible input — including the integer_squareroot edge case our ESBMC-Python report flagged in the Ethereum consensus specification, the verification bottlenecks that blocked Intel's firmware analysis, and the 23 additional property violations ESBMC identified in Arm's RMM firmware on top of those CBMC had already detected.

ESBMC uses Satisfiability Modulo Theories (SMT) solvers to mathematically reason about your code's behaviour, producing either a proof of correctness or a concrete counterexample showing exactly how a bug can be triggered.

Learn how ESBMC works

integer_squareroot helper (Python)

def integer_squareroot(n: uint64) -> uint64:
  x = n
  y = (x + 1) // 2  # ← overflows to 0 when n = 2⁶⁴ − 1
  while y < x:
    x = y                 # x becomes 0 after the overflow
    y = (x + n // x) // 2  # ← ZeroDivisionError: n // 0
  return x

# Input:  n = 2⁶⁴ − 1 (maximum uint64 value)
# Result: ZeroDivisionError — the unsigned integer overflows to 0,
#         then is used as the denominator of a division operation.
# ESBMC-Python: confirmed the bug and produced a counterexample trace.

How we help

Our Services

All services

Verification Consulting

Embed ESBMC into your SDLC to formally prove the absence of runtime errors in C, C++, Rust, Python, Solidity, and more.

Learn more

Security Code Audit

Deep code analysis using bounded model checking — we produce mathematical proof or a concrete counterexample, not heuristic static-analysis warnings.

Learn more

AI-Assisted Bug Repair

ESBMC-AI automatically detects and patches memory errors, overflows, and undefined behaviour in human- and LLM-generated code. Integrates with VSCode and GitHub CI.

Learn more