{"ID":6267238,"CreatedAt":"2026-07-10T01:11:38.759438437Z","UpdatedAt":"2026-07-14T08:17:36.581265645Z","DeletedAt":null,"paper_url":"https://arxiv.org/abs/2607.08550","arxiv_id":"2607.08550","title":"ESBMC-Arduino: Closing the Deployment Gap for Formal Verification of Open-Hardware PLCs","abstract":"OpenPLC, Arduino OPTA, CONTROLLINO, and Industrial Shields M-Duino bring IEC 61131-3 to low-cost microcontrollers used in real automation and industrial control system (ICS) security research. Existing open-source verifiers for IEC 61131-3, including ESBMC-PLC, prove safety over an abstract scan-cycle model with idealized unbounded integers. The board artifact runs on a resource-constrained microcontroller unit (MCU) with 16-bit words (8-bit AVR Arduinos), and sensors are read via a finite-resolution analog-to-digital converter (ADC). We show this deployment gap makes naive width-aware verification unsound: across 123 real programs, checking 16-bit overflow without a hardware input model yields 44% false alarms (54/123) and finds no genuine defects, because it explores sensor values no ADC can produce. Since the gap lies where computation meets the physical process - a bounded sensor reading scaled by finite-width arithmetic into an actuation command - an overflow can silently suppress a safety action, such as a high-level alarm. An unbounded input model fabricates alarms that no environment can trigger. We present hardware-faithful verification for IEC 61131-3 on open hardware: a declarative hardware abstraction layer (HAL) descriptor (width, ADC/PWM resolution, I/O binding) and a sound lowering that interprets arithmetic at target width and constrains inputs to hardware-realizable ranges. We instantiate it for Arduino as ArduinoTool, deriving HAL parameters from official cores and realizing the input-range model in the ESBMC Ladder Diagram (LD) frontend. On the 123-program corpus, the HAL annotator eliminates all 54 false alarms while preserving robustness proofs, and a controlled corpus demonstrates the rare width-dependent defects it detects with realizable witnesses.","short_abstract":"OpenPLC, Arduino OPTA, CONTROLLINO, and Industrial Shields M-Duino bring IEC 61131-3 to low-cost microcontrollers used in real automation and industrial control system (ICS) security research. Existing open-source verifiers for IEC 61131-3, including ESBMC-PLC, prove safety over an abstract scan-cycle model with ideali...","url_abs":"https://arxiv.org/abs/2607.08550","url_pdf":"https://arxiv.org/pdf/2607.08550v1","authors":"[\"Pierre Dantas\",\"Lucas Cordeiro\",\"Waldir Junior\"]","published":"2026-07-09T14:42:15Z","proceeding":"cs.PL","tasks":"[\"cs.PL\",\"cs.AR\",\"eess.SY\"]","methods":"[]","has_code":false}