Rigorous treatment of Meek's method for single transferable vote with formal proofs of key properties

Abstract

This thesis presents a mechanised formalisation of key concepts and properties of Meek's method of Single Transferable Vote (STV). This method is currently in use in a number of local elections in New Zealand, the Royal Statistical Society, and even the Stack Exchange network. Using a formal approach, we show that the iterative solution to the surplus transfer round of Meek's method converges to a unique and valid solution, and connect a functional implementation of its key components to a more abstract and generalised proof.

Along the way, we consider and address issues present in existing pen-and-paper proofs, and discuss a general representation of strict ballots suitable for the proof patterns encountered in our formal development and for the implementation of Meek's method.

We believe that this work pushes the boundaries of interactive theorem proving for the formal verification of voting algorithms, and offers multiple promising avenues for further work on formally verifying the correctness and termination of STV methods in Isabelle/HOL.