This master thesis delves into the multifaceted realm of Social Choice Theory, aspiring to not only deepen but also broaden our understanding of collective decision-making in the face of diverse and conflicting individual preferences. At the core of this exploration is the critical examination of the formalization, verification, and customization of voting systems—foundational mechanisms that significantly impact pivotal decision-making scenarios, including elections and resource allocation. Leveraging the advanced capabilities of Isabelle/HOL, a sophisticated platform for formal mathematical reasoning, this project meticulously investigates the intricacies of the D'Hondt and Sainte-Laguë voting systems. Social Choice Theory, the theoretical backdrop of this study, encompasses more than mere preference aggregation—it accentuates the complex interplay of rationality and fairness criteria essential for fostering democratic governance.