vix.ing · top · new · best · stats · spec

Verification of E-Voting Algorithms in Dafny

2025/12/24 by R. Büttner, Büttner, Robert, Fabian Franz Dießl +17
Computer Science · Economics, Econometrics and Finance · #D.2.4 #F.3.1 #FOS: Computer and information sciences #Formal Methods in Verification #Game Theory and Voting Systems #Internet Traffic Analysis and Secure E-voting #Logic in Computer Science (cs.LO)

paper · doi:10.48550/arxiv.2512.21084

openalex publication_date 2025/12/24 · openalex created_date 2025/12/26 · openalex updated_date 2026/07/28

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.

Citations

Related