The Efficient SMT-Based Context-Bounded Model Checker (ESBMC) has grown from a research prototype for verifying embedded ANSI-C software into one of the most versatile and industrially capable formal verification platforms available today. Since its first publication in 2009, ESBMC has undergone persistent evolution: expanding its verification techniques, widening its language support to nine front-ends, integrating industrial-strength SMT solvers, and - most recently - coupling with Large Language Models (LLMs) and autonomous AI agents. This survey traces the full trajectory of ESBMC from its original design principles to the state of the art in 2025-2026, documenting 43 awards at SV-COMP and Test-Comp, peer recognition at leading software engineering venues, including a Distinguished Paper Awards at ICSE'11 and ASE'24, a Most Influential Paper Award at ASE'23, and a Best Tool Paper Award at SBSeg'23, its role as a formal verification backend for LLM-driven self-healing software and loop invariant generation, and the first industrial deployment of an integrated agentic model-checking architecture through the NVIDIA-OpenSMA framework, establishing ESBMC as a natively autonomous verification kernel rather than a passive validation backend. We synthesize its economic impact - over GBP 9.3 million and EUR 4.98 million in confirmed public research funding, the VeriBee spin-off, and a defense industrial deployment at Lockheed Martin - and conclude with a structured agenda of open challenges spanning scalability, neurosymbolic verification, counterexample intelligibility, cross-language verification, safety standards compliance, and open-source sustainability.

翻译：基于高效SMT的上下文有界模型检测器（ESBMC）已从最初用于验证嵌入式ANSI-C软件的研究原型，发展成为当今功能最全面、工业级能力最强的形式化验证平台之一。自2009年首次发表以来，ESBMC经历了持续的演进：扩展了验证技术，将语言支持拓宽至九个前端，集成了工业级SMT求解器，并最新结合了大型语言模型（LLM）与自主AI智能体。本综述全面追溯了ESBMC从原始设计理念到2025-2026年最新技术的完整发展轨迹，记录了其在SV-COMP和Test-Comp竞赛中获得的43项奖项，在顶级软件工程会议中获得的同行认可（包括ICSE'11和ASE'24的杰出论文奖、ASE'23最具影响力论文奖、SBSeg'23最佳工具论文奖），其作为LLM驱动的自修复软件和循环不变式生成的形式化验证后端的作用，以及通过NVIDIA-OpenSMA框架首次实现集成式智能体模型检测架构的工业部署——这使得ESBMC成为一个原生自主的验证内核，而非被动的验证后端。本文还综合了其经济影响（已确认的公共研究资金超过930万英镑和498万欧元）、衍生企业VeriBee以及洛克希德·马丁公司的国防工业部署，最后提出了一份结构化的开放挑战议程，涵盖可扩展性、神经符号验证、反例可理解性、跨语言验证、安全标准合规性和开源可持续性等方向。