The Votail verified PR-STV tally system.
Votail is an open source Java 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 source code is managed using git hosted at GitHub. https://github.com/FreeAndFair/Votail
See also http://itu.dk/en/Forskning/Technical-Reports/2011/TR-2011-143