ESBMC-LLB 是一个工具，它利用 ESBMC-PLC+ 通过暴露现有验证器常忽略的功能块逻辑，来检测 IEC 61131-3 PLC 程序中的梯形逻辑炸弹 (LLB)。它将炸弹检测重新定义为形式化验证问题，使用 k-归纳法进行无界证明以确认炸弹不存在，并使用有界模型检查来恢复触发条件。
在 Iacobelli 2024 数据集上，ESBMC-LLB 检测到了全部 30 个炸弹并恢复了每个触发条件，包括那些规避 CFG 分诊的自适应触发条件。在 PLC-Defuser 的 SWaT 语料库 v1.0.0 上，它检测到 149/150 个炸弹（99%），且零误报，但由于求解器超时，对具有非线性非终止行为的后续版本检测率降至 49%。
作者得出结论，语义模型检查与 CFG 分诊是互补的，前者提供无界证明和对自适应触发条件的鲁棒性。