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.

翻译：电子投票程序是选举系统的具体实现，使得借助计算机开展投票或选举成为可能。本文报告了一个开源电子投票程序库的开发工作，该库目前涵盖计分投票、即时复选投票、博尔达计数法与单一可转移投票四种方法。其中两种方法在文中被详细讨论，所有四种程序均已通过Dafny语言实现，并形式化验证了其与功能规范的一致性及关键正确性属性。通过从Dafny实现中提取可执行代码，该程序库已被用于搭建在线投票服务系统。