Service
AI-Assisted Bug Repair
Large language models accelerate development but introduce security debt at scale. ESBMC-AI acts as a formal safety net — surfacing what the LLM missed and proposing candidate patches for engineer review.
The challenge
AI generates code. ESBMC verifies it.
Development teams using LLMs to generate code ship faster — but they inherit the security vulnerabilities that LLMs routinely introduce: memory leaks, integer overflows, null dereferences, and undefined behaviour. At scale, this creates a security debt that testing alone cannot surface.
ESBMC-AI was developed as part of the £1.2M NW CyberCom project led by Lancaster University. It combines ESBMC's formal verification engine with AI-driven repair to close the loop: detect, patch, and re-verify — automatically.
ESBMC-AI workflow
Capabilities
What ESBMC-AI delivers
Bug detection
ESBMC-AI helps identify memory errors, overflows, and undefined behaviour in both human-written and LLM-generated code, using ESBMC's underlying SMT-based analysis.
Candidate patch generation
For each identified violation, the system proposes a candidate patch and re-verifies it against the original safety property — patches are presented to your engineers for review, not applied silently.
VSCode integration
Developers can receive inline ESBMC-AI feedback in the editor as part of their normal review workflow.
GitHub / GitLab CI integration
Verification runs as part of pull-request checks; failed properties surface as actionable PR comments.
Regression verification
After a candidate patch is accepted, ESBMC re-verifies the affected code to surface regressions before merge.
AI-generated code hardening
A formal-methods safety net for teams adopting LLMs in their development workflow — the verifier the LLM itself cannot run.
Research provenance
Built on a published research base
ESBMC-AI was developed by our research group as part of the £1.2M NW CyberCom Connecting Capability Fund project (Research England, led by Lancaster University with partner universities including Manchester). The underlying technique is documented in Tihanyi, Charalambous, Jain, Ferrag and Cordeiro, "A New Era in Software Security: Towards Self-Healing Software via Large Language Models and Formal Verification" (arXiv 2305.14752), and subsequent work by the same group.
ESBMC-AI is a research-grade tool whose findings and proposed patches are intended for engineer review — it is not a drop-in autonomous remediation system.
Pricing
Retainer or project-based
We integrate ESBMC-AI into your pipeline and provide ongoing verification support. Contact us to discuss your CI/CD setup and team size.