We study the verification of safety properties over symmetric parametrized systems. These systems consist on an arbitrary and unbounded number of threads running the same program. In this scenario, following standard deductive techniques leads to the need of verifying an unbounded collection of verification conditions which grows with the number of threads involved in the system. To handle this problem, we present a technique based on parametrized invariance rules to reduce the verification of finite and infinite state parametrized programs to the analysis of only a finite number of verification conditions. In our approach, all necessary VCs are automatically generated from the program and its specification, independently of the number of threads involved in the system. In this talk, we present the latest advances in our research as well as some running examples including a ticket-based mutual exclusion algorithm and a concurrent single-linked list implementation. Both examples are verified using Leap. Leap is a tool under development at the IMDEA Software Institute which implements the parametrized invariance rules. Our tool is able to automatically generate all necessary VCs starting from the program and the properties specifications. Leap also implements decision procedures to automatically verify VCs, and is also extended to interactively assist the user in the verification process. Currently, the decision procedures allow to programs that manipulate numbers, sets, list layouts and their combinations, built on top of state-of-the-art SMT solvers. This is joint work with César Sánchez.