We formalise a variant of the Single Transferable Vote scheme with fractional transfer values in the theorem prover Coq. Our method advocates the idea of vote counting as application of a sequence of rules. The rules are an intermediate step for specifying the protocol for vote-counting in a precise symbolic language. We then formalise these rules in Coq. This reduces the gap between the legislation and formalisa-tion so that, without knowledge of formal methods, one can still validate the process. Moreover our encoding is modular which enables us to capture other Single Transferable Vote schemes without significant changes. Using the built-in extraction mechanism of Coq, a Haskell program is extracted automatically. This program is guaranteed to meet its specification. Each run of the program outputs a certificate which is a precise, independently checkable record of the trace of computation and provides all relevant details of how the final result is obtained. This establishes correctness, reliability, and verifiability of the count.
展开▼
