Verification of E-Voting Algorithms in Dafny

TL;DR

This paper presents a formally verified library of electronic voting algorithms implemented in Dafny, ensuring correctness and enabling deployment in a web voting service.

Contribution

It introduces an open-source library of verified e-voting procedures in Dafny, covering multiple voting methods with formal correctness guarantees.

Findings

Verified correctness of four voting algorithms

Successful deployment of a web voting service

Open-source library available for further use

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.