- The paper introduces ESBMC-Arduino to close the deployment gap in formal verification for open-hardware PLCs running on microcontrollers like Arduino.
- It highlights that naive width-aware verification without hardware input models leads to false alarms, as demonstrated by 44% false alarms in 123 real programs.
- A hardware-faithful verification approach is proposed using a declarative HAL descriptor and sound lowering to interpret arithmetic at target width and constrain inputs to hardware-realizable ranges.
- The method, instantiated as ArduinoTool, eliminates all false alarms while preserving robustness proofs and detects rare width-dependent defects with realizable witnesses.