The applications are being growingly executed on IoT systems. Such systems may involve devices that often rely on limited power sources, processing capabilities and shut down for prolonged durations to maximize energy efficiency. They do not possess the means to forge reliable and direct communications with the Internet. Establishing horizontally scalable applications is not always assured in IoT systems. In this paper, we propose a model to verify horizontally scalable IoT applications. Three verification axes are considered: Architectural, Intermediation, and Horizontal Scalability. Thus, we adopted the Event-B formal method to incrementally develop our model, taking advantage of its refinement features. We also engaged proof obligations to accurately verify the model and then leveraged the ProB animator for its validation.