# Detecting Ladder Logic Bombs in IEC 61131-3 PLC Programs using ESBMC-PLC+: A Formal Verification Approach with Trigger Synthesis

arXiv: https://arxiv.org/abs/2607.08417 · HTML: https://mlsanity.com/paper/2607.08417/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 4 of its 34 references that are in the map.
- First posted on arXiv 9 Jul 2026.

## Builds on (most cited first, 4 of 4)

- [K-ST: A Formal Executable Semantics of the Structured Text Language for PLCs](https://mlsanity.com/paper/2202.04076/) (2022)
- [PLCverif: Status of a Formal Verification Tool for Programmable Logic Controller](https://mlsanity.com/paper/2203.17253/) (2022)
- [Towards establishing formal verification and inductive code synthesis in the PLC domain](https://mlsanity.com/paper/2106.15878/) (2021)
- [Formal Verification of PLCs as a Service: A CERN-GSI Safety-Critical Case Study (extended version)](https://mlsanity.com/paper/2502.19150/) (2025)

## Abstract (arXiv)

A Ladder Logic Bomb (LLB) is malicious control logic in a Programmable Logic Controller (PLC) program that lies dormant until a trigger activates a payload to manipulate actuators, forge sensor readings, or deny operator control. We observe that real malicious logic hides inside function-block bodies, which existing ladder-diagram verifiers drop from their intermediate representation (IR), making bombs invisible to provers. We present ESBMC-LLB, which uses ESBMC-PLC+ as its verification engine and adds a modeling layer that exposes function-block logic and recasts bomb detection as a formal verification problem: a scan-watchdog exposes non-termination payloads, and output wiring exposes actuator-forgery payloads as safety violations. k-induction gives an unbounded proof of bomb-absence across all scans, and the bounded model checker returns a counterexample that is the trigger - guarantees that signature, anomaly, and CFG-triage detectors lack. On the public Iacobelli 2024 dataset, ESBMC-LLB detects all 30 bombs and recovers every trigger; it also detects adaptive triggers (computed, opaque-arithmetic, multi-scan) that evade CFG-triage. We also report the first semantic model-checker evaluation on PLC-Defuser's SWaT corpus: our analog extension makes the full corpus parseable; on v1.0.0, it detects 149/150 bombs (99%) with zero false positives, recovering each trigger; on a later version with nonlinear non-termination bombs, detection drops to 49% as the SMT solver times out. We conclude that semantic model checking and CFG-triage are complementary - the former gives unbounded proofs, adaptive-trigger robustness, and handles Boolean/integer and linear analog logic; the latter leads to nonlinear analog non-termination, and we delineate where each wins.