Service
Security Code Audit
We apply formal bounded model checking to your codebase and return, within the specified verification bounds, either a formal proof that a class of bugs does not occur or a concrete counterexample showing exactly how one can be triggered.
The problem with static analysis
Heuristic warnings are not proof
Static analysis tools generate warnings based on heuristics. They are fast but produce false positives, miss subtle bugs, and give no guarantee that a class of error is absent. Engineers spend hours triaging warnings that turn out to be benign — and miss the ones that matter.
In our published Arm collaboration (SAS 2024), ESBMC identified 23 additional property
violations in the Realm Management Monitor on top of those CBMC had already detected
in the project's own CI. In our published Ethereum collaboration (ISSTA 2024), our
ESBMC-Python tool identified a division-by-zero in the
integer_squareroot
helper of the consensus specification, with the fix merged upstream as
ethereum/consensus-specs PR #3600.
Our approach
Every confirmed violation is reproducible
ESBMC encodes your program as SMT constraints and hands them to an industrial solver. Every confirmed violation comes with a concrete counterexample — a precise execution trace that reproduces the bug, making it trivially reproducible by your engineers.
When ESBMC finds no counterexample within the specified verification bounds, it provides a formal proof for that bound — not a "no warnings found today" heuristic, but a mathematical statement about the program's behaviour for the bounded execution space.
Coverage
Bug classes we audit for
Process
How an audit works
Scope definition
We agree on the codebase, languages, safety properties, and verification bounds.
ESBMC analysis
We run ESBMC with configurations optimised for your codebase and error classes of interest.
Findings report
Each finding is severity-ranked and accompanied by a concrete counterexample trace.
Remediation guidance
We explain the root cause and recommend a fix. We can re-verify after changes at no extra cost.
Pricing
Fixed-price, scoped per KLOC
We agree scope and a fixed price before starting. No hourly surprises. Contact us with your codebase size and language to receive a quote.