Swarm robotics, comprising decentralized collectives of robots with emergent behaviors, holds promise for tasks like exploration and construction. However, verifying safety and liveness properties in these systems proves challenging due to their nature. This paper proposes an approach using the Event-B formal method for modeling and verifying swarm robotics systems. Event-B offers a framework to specify models and prove properties mathematically. Demonstrating the method’s efficacy, we model swarm behaviors and environments using Event-B, formulate key safety and liveness properties, and discharge proof obligations for verification. Applying this approach to case studies involving swarm construction and navigation, we successfully verify critical properties, including collision avoidance, localization, and goal reaching. This rigorous verification allows for the validation of swarm system correctness before deployment, offering certified guarantees that enhance trust and facilitate real-world deployment.