Modern IoT systems introduce unique challenges related to flexibility, resource limitations, and energy efficiency. As these IoT systems expand to incorporate more devices, ensuring reliable communication, managing energy consumption, and preventing standoff situations becomes increasingly difficult. This paper proposes a formal model to verify complex IoT systems, addressing key areas: design, coordination, flexibility and energy efficiency. Using the Event-B method, our model enables a gradual refinement of system properties, enhancing both reliability and correctness in IoT systems. The model’s validity is further demonstrated through the use of powerful Rodin plugins and tools.