Verification-centric realization of electronic vote counting

Activist computer scientists, including some of the authors of this paper, have been working against the adoption by governments of commercial, proprietary, insecure, poorly designed and implemented voting systems the world-over. And, while we mainly work to accomplish our goals by educating citizens and communicating with the press, we also must propose solutions to the problems of trustworthy e-voting. If a computer-based voting system is to ever be adopted, that system must be demonstrably of extremely high quality. This paper discusses a methodology and a set of tools we have used to implement a vote counting plugin, for an experimental computer-based voting system using applied formal methods.