Research Summary: Counting by the Book: Verifying Alaska's Ranked-Choice Elections

Researchers evaluated Alaska's ranked-choice election tabulation rules through a Formally Verified Democracy initiative using the Lean proof assistant. An evaluation of 115 ranked-choice contests held since 2022 identified 75 ballot records across 10 contests that were counted differently by published result reproduction software compared to the formal model, stemming from edge-case handling of overvotes and duplicate rankings without altering contest outcomes.

Why it matters

Translating legal mandates into automated code inherently requires discretionary interpretations that can lead to counting discrepancies in complex voting frameworks. Applying formal mathematical verification demonstrates how edge cases like overvotes can be systematically audited to prevent systemic errors. This approach offers institutional leaders a verifiable method to guarantee statutory alignment and reinforce public trust in automated public-sector processes.

Key insights

• Researchers formalized Alaska's ranked-choice voting rules within the Lean proof assistant to verify software implementations against statutory requirements.
• Across 115 ranked-choice contests in Alaska since 2022, 75 ballot records across 10 contests exhibited tabulation differences compared to the formal model.
• None of the identified ballot discrepancies altered the winning outcomes of the analyzed contests.
• The counting variations were traced directly to differing interpretations of overvotes and duplicate rankings when translating legal statutes into software.

Source

arXiv — Computers and Society — https://arxiv.org/abs/2610.36494