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.

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.

Researchers formalized Alaska's ranked-choice voting rules within the Lean proof assistant to verify software implementations against statutory requirements.

Forward consideration, not a verified fact.