Verifying Alaska’s ranked-choice elections with formal proofs
Counting by the Book: Verifying Alaska's Ranked-Choice Elections
Logic in Computer ScienceComputers and Society
Summary
Figuring out who wins in ranked-choice elections can be complicated, especially when rules and software have to match exactly. The authors created a formal, computer-checked version of Alaska’s election counting rules to make sure the results were accurate and trustworthy. They found some small differences in how ballots were counted, related to extra votes or repeated rankings, but these didn't change who won. This work shows how math and logic can clarify election rules and help spot hidden choices in election software.
What this means in practice
- •For election officials: Check if election software correctly implements complex ranked-choice counting rules using formal proofs to ensure accurate and legally justified results.
- •For software auditors: Identify subtle differences in ballot handling in election software to improve audits and compliance with election laws.
Authors
Lucy Horowitz
Abstract
We present Alaska's ranked-choice elections as a case study in Formally Verified Democracy, a program to establish election results through formally checked proofs. We formalize an interpretation of Alaska's tabulation rules in Lean, verify its implementation, and prove election-specific results. Across 115 ranked-choice contests in Alaska since 2022, we identify 75 ballot records across 10 contests that were counted differently from this interpretation by a program reproducing the published results, without changing any winners. We trace these differences to overvotes and duplicate rankings and examine their legal justification, showing how formal verification can expose consequential choices in translating election law into software.