Formally verified invariants of vote counting schemes

The correctness of ballot counting in electronically held elections is a cornerstone for establishing trust in the final result. Vote counting protocols in particular can be formally specified by as systems of rules, where each rule application represents the effect of a single action in the tallying process that progresses the count. We show that this way of formalising vote counting protocols is also particularly suitable for (formally) establishing properties of tallying schemes. The key notion is that of an invariant: properties that transfer from premiss to conclusion of all vote counting rules. We show that the rule-based formulation of tallying schemes allows us to give transparent formal proofs of properties of the respective scheme with relative ease. As our proofs are based on the specification of vote counting protocols, rather than a program that implements them, we are guaranteed that the property holds for every possible specification-confirming implementation of the respective protocol. This in particular includes the vote counting programs that are automatically extracted from the specification. We demonstrate this point by means of two examples: The monotonicity criterion for majority (first-past-the-post) voting, and the majority criterion for a simple version of single transferable vote.