Votail: A Formally Specified and Verified Ballot Counting System for Irish PR-STV Elections
Votail is an implementation of Ireland's method of Proportional Representation by Single Transferable Vote (PRSTV). The functional requirements derived from Irish electoral law are specified using Business Object Notation (BON) and the Java Modeling Language (JML). Formal methods have been used to verify the correctness of the software.
The Republic of Ireland uses Proportional Representation by Single Transferable Vote (PR-STV) for its national, local and European elections. Oireachtas Eireann, the National Parliament of the Republic of Ireland, has two chambers. The people directly elect Dail Eireann, the lower chamber of the Oireachtas, for a term of up to five years. The upper house, called the Seanad, also uses PR-STV, but uses postal ballots and is indirectly elected, except for the six seats elected by university graduates. The Seanad has an advisory role and a smaller electorate. It is therefore a lesser target for electoral fraud, and a low risk election, so it is more interesting and important to look at verification of Dail elections.
In elections to the Dail, recounts are often called for closely contested seats, because the intermediate count results often vary slightly, indicating small errors in the manual process of counting votes. Paper-based voting with counting-by-hand is popular in Ireland, and the pilot project for use of voting machines in elections to the Dail was undermined by errors in the proprietary ballot counting software.
The Commission on Electronic Voting (CEV) laid down several guidelines for development of electronic voting systems, including the following:
- Clear definition of functional requirements and specifications
- Robust and formal approach to design and development
- Separation of critical concerns e.g. voter registration and ballot counting
- Publication or public inspection of the source code (preferably open source)
- Open public testing of the system