Verified and Verifiable Computation with STV Algorithms

Abstract

Single Transferable Vote (STV) is a family of preferential voting systems, different instances of which are used in binding elections throughout the world. Most countries with an STV system rely on archaic manual vote counting or opaque unreliable computerised methods. Although technology exists to enhance the situation by building significantly more transparent, trustworthy, reliable vote counting tools, in practice these technologies are ignored. We introduce a framework which formalises and verifies the similarities of STV algorithms as an abstract machine and realises differences of various STV algorithms as instantiations into the machine. The framework provides a uniform and modular process of (a) producing tools that carry out verified computation with an STV algorithm and (b) synthesising means for verifying the computation carried out independently of the computation's source code. It also provides flexibility and ease for adapting and extending it to a variety of STV schemes. We minimise the trusted base in the correctness of the tools synthesised by using the Coq and HOL4 theorem provers and the ecosystem of CakeML as the technical basis. Moreover, we automate almost all proofs that we establish in Coq, HOL4 and CakeML so that new instances of verified and verifying tools for computation with a variety of STV algorithms can be created with no (or minimal) extra verification. Finally, our experimental results with executable code demonstrate the feasibility of deploying the framework for verifying real size elections having an STV counting mechanism.