Verification of E-Voting Algorithms in Dafny
summary
A verified open-source library implements Score Voting, Instant-Runoff Voting, Borda Count, and Single Transferable Vote in Dafny, with 2,385 lines of code — 1,474 lines (≈62%) as specifications — and about 30 minutes of verification per line. Instant-runoff uses a ghost recursive winner predicate to prove elimination and majority progress; STV uses timestamped states. Code extraction produces a working voting web service and two live sites (English/German) that run the verified algorithms.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 1:29E-voting challenges and goals
- 2:33Voting algorithms selection
- 3:56Point-based vs round-based
- 5:23Instant Runoff Voting example
- 6:49Dafny verification of IRV
- 9:15Ghost functions and postconditions
- 11:04Verification statistics
- 12:28Conclusion
- 13:11Project outcomes and demos
related talks
20mVerifiable Elections—Now Is the Time
45mFrom Ballots to Code: Exploring Election Security
22mBuilding a Voting Machine Everyone Can Trust
25mFrom Voting Machines to Discord: A Path to Technological Activism
26mA formal security analysis of Blockchain voting
35mFreeing the software that runs our elections
12mIncreasing security without decreasing usability: A comparison of various verifiable...
21mBuilding trust in a system through transparency: lessons from Swiss Post E-Voting system