Open PLC, Arduino OPT A, CONTROLLINO, and Industrial Shields M‑Duino bring IEC 61131‑3 to low‑cost microcontrollers used in real automation and industrial control system security research. Existing verifiers such as ESBMC‑PLC prove safety over an abstract scan‑cycle model with idealized unbounded integers, yet the board runs on a 16‑bit MCU with finite‑resolution ADCs.

This deployment gap makes naive width‑aware verification unsound. Across 123 real programs, checking for 16‑bit overflow without a hardware input model yields 54 false alarms (44%) and finds no genuine defects, because it explores sensor values no ADC can produce. The mismatch occurs where computation meets the physical process—bounded sensor readings scaled by finite‑width arithmetic into actuation commands—allowing an overflow to silently suppress a safety action.

We present hardware‑faithful verification for IEC 61131‑3 on open hardware: a declarative HAL descriptor (width, ADC/PWM resolution, I/O binding) and a sound lowering that interprets arithmetic at target width while constraining inputs to hardware‑realizable ranges. Instantiated for Arduino as the Arduino Tool, the HAL annotator eliminates all false alarms and preserves robustness proofs, detecting rare width‑dependent defects with realizable witnesses.

On the 123‑program corpus, the HAL annotator removes all 54 false alarms, demonstrating that hardware‑aware analysis is essential for reliable formal verification of low‑cost PLCs.