Verification of E-Voting Algorithms in Dafny
Logic in Computer Science
2025-12-25 v1
Abstract
Electronic voting procedures are implementations of electoral systems, making it possible to conduct polls or elections with the help of computers. This paper reports on the development of an open-source library of electronic voting procedures, which currently covers Score Voting, Instant-Runoff Voting, Borda Count, and Single Transferable Vote. The four procedures, of which two are discussed in detail, have been implemented in Dafny, formally verifying the consistency with functional specifications and key correctness properties. Using code extraction from the Dafny implementation, the library has been used to set up a voting web service.
Keywords
Cite
@article{arxiv.2512.21084,
title = {Verification of E-Voting Algorithms in Dafny},
author = {Robert Büttner and Fabian Franz Dießl and Patrick Janoschek and Ivana Kostadinovic and Henrik Oback and Kilian Voß and Franziska Alber and Roland Herrmann and Sibylle Möhle and Philipp Rümmer},
journal= {arXiv preprint arXiv:2512.21084},
year = {2025}
}
Comments
7 pages, 2 figures