The cardinality operator is indispensable when specifying and reasoning about parameterized concurrent/distributed systems. It provides a level of abstraction and conciseness that makes (manual) proofs go through smoothly. Unfortunately, the automation support for such proofs remains elusive due to challenges in counting sets of unbounded program states. In this talk, I will present #Π a tool that can automatically synthesize cardinality-based proofs of parameterized systems. #Π crucially relies on a sound and precise axiomatization of cardinality for the combined theory of linear arithmetic and arrays. This axiomatization is the key technical contribution of this work. We show that various parameterized systems, including mutual exclusion and consensus protocols, can be efficiently verified using #Π. Many of them were automatically verified for the first time. This is joint work with Nikolaj Bjørner and Andrey Rybalchenko.