<p>Recently, there has been a growing focus on developing IoT applications intended to run on dynamic and constrained systems. A dynamic and constrained IoT system incorporates a substantial number of devices that are capable of moving autonomously due to their shrinking size and enhancing portability, without even knowing in advance mobility parameters such as movement durations and destination locations. Besides, these devices often exhibit significant constraints on code space and processing capabilities and most likely lack the necessary resources to communicate directly with the Internet in a reliable manner. They participate in Internet communications with the help of devices that serve as proxies. A proxy is expected to provide scalability, among other properties, in order to assist a rising number of constrained devices and satisfy the variation in demand, while preserving a certain level of Quality of Service (QoS). Nonetheless, guaranteeing the correctness of scalable applications remains challenging in dynamic and constrained IoT systems. In this article, we propose an approach for the modeling and verification of scalable IoT applications, while addressing four verification aspects: Constructural, Mobility, Behavioral, and Scalability. Hence,&#xa0;we selected the Event-B formal method to develop our model progressively, leveraging its refinement mechanisms. We also used proof obligations and the ProB animator to carry out the verification and validation of our model in a mathematically sound way.</p>