Machine Checked Properties of the Schulze Method
Date:
The correctness of electronic vote-counting software programs is crucial in establishing the trust of people in electronic voting. However, most of these vote-counting programs, used in various jurisdiction for legally binding election, establish the correctness by means of testing which is not sufficient and leaves much to be desired. Therefore, we propose that legally binding vote-counting software programs should be formally verified and its correctness should be evaluated against some well established framework from social choice theory.
In this work, we formally prove (machine-checked) that our Coq implementation of the Schulze method, a preferential voting method, follows the Condorcet winner property. We leave the formal machine-checked proof of other properties, e.g., reversal symmetry, Pareto, monotonicity, etc., for future work. This is, to the best of our knowledge, the first machine-checked proof of properties of the Schulze method implementation, and in fact, any preferential vote-counting implementation.