The purpose of this project is to make available formal specifications of ranked choice voting (RCV), also known as instant runoff voting (IRV) in the case of a single winner and the single transferable vote (STV) more generally.
The focus will initially be on those variants of RCV used in US jurisdictions. The project will also aim to formalize ways of auditing RCV elections.
The project will use Coq for the formalization.
This work will inform the work of IEEE's Voting System Standards Committee (VSSC) Working Group 1622.6, "Voting Methods Mathematical Models."
This section contains links to statutes and other sources that describe the RCV rules in each jurisdiction we are interested in.
- Berkeley, CA, Municipal Codes. See Charter, Article III, Sec. 5.12, "Use of instant runoff voting in lieu of runoff elections"; and Municipal Code, Title 2, Chapter 2.14, "Elections -- Instant Runoff Voting."
- Cambridge, MA
- TODO
- Minneapolis, MN, Code of Ordinances. See Charter, Article III, Sec. 3.1; and Code of Ordinances, Title 8.5, Chapter 167, "Municipal Elections: Rules of Conduct."
- Oakland, CA, Charter. See Article XI, Sec. 1105, "Ranked Choice Voting."
- Portland, ME
- TODO
- San Francisco, CA, Charter. See Article XIII, Sec. 13.102, "Instant Runoff Elections."
- San Leandro, CA
- TODO
- Saint Paul, MN
- TODO
The project is licensed under a BSD 3-Clause license. See the LICENSE file for details.
- Chris Jerdonek