<p>Modern Internet of Things (IoT) systems connect many different parts, from physical devices to cloud-based services, all working together. Keeping these complex systems running reliably, even when problems occur, is a major challenge. A key issue is that a failure starting in one part can quickly spread to others, causing widespread service breakdowns. Current engineering methods often cannot provide solid, mathematically backed promises of fault tolerance, especially in systems built from diverse, spread-out components. This creates a critical need for thorough ways to check and ensure strong resilience at every stage of the IoT system. To meet this need, we introduce a formal verification approach using Event-B. This approach specifically targets important fault-handling strategies like gracefully reducing service, switching to backups, and returning to a safe state after a problem. Our approach begins with abstract, high-level models of how the system should work. We then carefully add more detailed operational information step-by-step through refinement, making sure essential correctness rules are always maintained throughout this process. To thoroughly verify and validate the system, we combine two powerful tools: theorem proving using the Rodin platform to verify logical properties, and model checking using ProB to explore system behavior under different failure conditions. This dual approach allows us to validate both how the system is built and how it acts when things go wrong. The result is a method that delivers strong mathematical guarantees for dependable operation, smooth integration between layers, and consistent recovery actions across the IoT system.</p>