Formal verification for IEC 61131-3 PLCs on open hardware (Arduino, OpenPLC, CONTROLLINO) has had a concrete problem: the tools operated on abstract models with idealized unbounded integers, but the hardware runs on 8- or 16-bit AVR MCUs reading sensors through finite-resolution ADCs. On a 123-program corpus, naive 16-bit overflow checking produced a 44% false alarm rate and found zero genuine defects, because it explored sensor input values that no ADC can physically produce. ESBMC-Arduino fixes this with a declarative hardware abstraction layer that constrains inputs to hardware-realizable ranges and interprets arithmetic at target width. The 54 false alarms drop to zero; the real defects stay detectable with witnesses the hardware can actually trigger.
The mechanism is a declarative HAL descriptor: word width, ADC/PWM resolution, I/O bindings per board. The verifier instantiates this as input-range constraints in the ESBMC Ladder Diagram frontend. The key insight is that the gap between "verified on the abstract model" and "safe on the deployed board" sits exactly at the junction of finite-width arithmetic and bounded sensor readings. An overflow that silently suppresses a high-level safety alarm is the failure mode the abstract model cannot see.
This matters for industrial teams using Arduino-class hardware in real automation and ICS roles. The open-hardware PLC segment has been growing because low-cost MCUs got good enough for many control loops. The missing piece was a formal checker that understood the hardware constraints well enough to produce actionable results. A 44% false alarm rate means the tool cannot run in CI, because engineers tune out tools that cry wolf on every other program.
ESBMC-Arduino is the first formal verifier to bridge the open-hardware PLC deployment gap with a hardware-faithful model. If the approach extends to SAMD, RP2040, and ESP32 targets, it gives industrial teams CI-runnable formal verification at a price point that does not require a PLC vendor contract. The teams most exposed are industrial automation vendors who sell proprietary PLC toolchains partly on the grounds that open-source alternatives cannot be formally verified.