General purpose correct-by-construction synthesis methods are limited to\nsystems with low dimensionality or simple specifications. In this work we\nconsider highly symmetrical counting problems and exploit the symmetry to\nsynthesize provably correct controllers for systems with tens of thousands of\nstates. The key ingredients of the solution are an aggregate abstraction\nprocedure for mildly heterogeneous systems and a formulation of counting\nconstraints as linear inequalities.\n