Formal methods offer rigorous techniques for modeling and reasoning about concurrent and distributed systems. However, their adoption in practical software engineering remains limited, often due to usability challenges and the perceived complexity of existing tools. This limitation is particularly evident in emerging domains such as the Internet of Things (IoT), where systems are inherently concurrent, heterogeneous, and susceptible to subtle coordination errors. In this paper, we explore the use of the Anemone Workbench, which combines the Linda-like coordination language Multi-Bach with temporal logic, to support the modeling, animation, and verification of concurrent IoT systems. Anemone aims to bridge the gap between informal requirements and formal specifications, providing a lightweight and accessible platform that makes concurrency both explicit and analyzable. Through three case studies, a dynamic sports simulation, a smart garden for energy management, and an immersive role-playing game, we demonstrate how properties can be specified, visualized, and verified. Beyond technical contributions, we reflect on the educational value of Anemone, showing how it fosters understanding of formal methods through hands-on modeling activities. Our findings highlight opportunities for integrating lightweight formal tools into both academic and industrial workflows, contributing to software reliability and opening new directions for scalable formal modeling in IoT contexts.