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

1 Introduction

• A formally checked proof can make the reasoning from ballots to winners independently checkable; an Oakland tabulation-software configuration error illustrates why ballot treatment matters.The paper notes that a proof against a specification capturing the required treatment could have exposed the Oakland discrepancy before certification.Source: §1 · pp. 1–2
• Rules for malformed ballots—including skipped rankings, repeated candidates, and multiple candidates at one rank—vary across jurisdictions, and those choices can affect ballot counts.Source: §1 · p. 1
• On the reconstructed example ballot, Begich is ranked first through third and Palin fourth; after Begich’s defeat, the statutory model counts it for Palin, while the reproduction model makes it inactive.The difference turns on whether disregarding repeated Begich rankings leaves skipped rankings that can make the ballot inactive.Source: §1 · p. 2
• Because the Division’s tabulation software is proprietary, the authors cannot inspect or formally verify it, so they infer its behavior by matching published round-by-round totals with an independent tabulator.Source: §1 · p. 2
• The paper formalizes Alaska’s rules in Lean, verifies an implementation, and proves election-specific results; its comparison finds different ballot counts but the same winners.Source: §1 · p. 3

2 The Statutory Model

• The model has three layers—statutory vocabulary, a specification of permitted outcomes, and an implementation that computes those outcomes as a tree of defeat sequences.The vocabulary and specification follow the statute closely, while the implementation may differ from its text because it is proved to compute exactly the specified outcomes.Source: §2 · p. 3

2.1.1 Ballots and elections.

• Ballots are lists of rankings, each containing a list of candidates, so the model can represent shared ranks, skipped ranks, and repeated candidates.The statutory model makes a ballot inactive for an overvote only when the overvoted rank is the highest rank containing a continuing candidate; the reproduction model also truncates at some earlier overvotes.Source: §2.1.1 · p. 4, §2.1.2 · p. 4

2.1.3 Skipped rankings. According to the statute,

• A skipped ranking is a blank rank followed by a later mark, and the Lean procedural rule for two consecutive skips agrees with its declarative inactivity condition.For duplicate rankings, the formalization retains repeated marks for blank and overvote checks but prevents them from supplying a later vote; the reproduction model instead uses a hybrid treatment.Source: §2.1.3 · p. 5, §2.1.4 · pp. 5–6

2.1.5 Inactive ballots.

• Inactivity from exhaustion or two skipped rankings persists, but overvote-based inactivity can change as the set of continuing candidates changes.The model therefore carries active ballots between rounds: once removed as inactive, a ballot cannot return to tabulation even if its remaining rankings would otherwise support a continuing candidate.Source: §2.1.5 · pp. 6–7

2.2 Allowable Outcomes

• A round may defeat any lowest-vote candidate when at least three candidates remain, while among the final two it may elect a candidate with at least as many votes as the other.Ties for last place permit any tied candidate to be defeated; a tie between the final two is left to procedures the model does not specify, so either candidate is permitted.Source: §2.2 · pp. 7–8

2.3 Implementation

• Theorem 2.1 proves that tabulate returns exactly the winners permitted by the statutory model for each valid defeat sequence.The computation represents outcomes as paths through an RCVTree; tied-last candidates can yield multiple permitted winners, represented using parallel-universes tiebreaking [46].Source: §2.3 · pp. 8–9
• The 192,289 ballots in the 2022 special election contain just 691 distinct ranking patterns, and Lean proves profile tabulation equals full represented-ballot tabulation.Source: §2.3 · p. 9
• Election-specific theorems require importing entire CVRs as definitions rather than using them as executable-function inputs, motivating profile grouping for tractability.Source: §2.3 · p. 9
• In all 115 contests, both models produce the same tie-free RCVTree, establishing the unique permitted winner and defeat order; reproduction-model round counts match published reports.The complete tabulation trees were checked by Lean’s kernel.Source: §2.3 · p. 9

3 Empirical Results

• The comparison used a statutory model and a reproduction model that matched all 22 published multi-round reports.The authors tested rule combinations against candidate votes and blank, exhausted, and overvoted ballot counts in every round.Source: §3 · p. 9
• The reproduction model combines Truncate for overvotes with Hybrid for duplicate rankings.Hybrid disregards repeated candidate marks when checking whether a ranking is blank but retains them when detecting overvotes.Source: §3 · p. 10
• 75 ballot records across 10 contests were counted for a candidate under the statutory model in a round where the reproduction model made them inactive.Both models elected the same winners in all 115 contests, and their final margins differed by at most seven votes.Source: §3 · p. 10

3.1 Reproduction vs. Statutory Model

• In the 2022 general-election U.S. House contest, all 14 differing ballots remained assigned to candidates under the statutory model in every round.In the final round, the statutory model assigned 10 ballots to Palin and four to Peltola, reducing Peltola’s margin by six votes compared with the reproduction model.Source: §3 · pp. 10–11, Table 2 · p. 11

3.2 Hybrid vs. Retain and Remove

• With Truncate fixed, Retain and Remove made 72 and 46 ballot records count where Hybrid made them inactive across the contests.Neither alternative reproduced all published reports: Retain differed in 11 of 22 multi-round contests, and Remove differed in eight.Source: §3.2 · p. 12

4.1 Overvotes

• The statutory provisions condition inactivity on an overvote at the highest continuing ranking, whereas Truncate blocks lower preferences even when no candidate at the overvoted rank remains continuing.The Division’s glossary announces Truncate but does not explain how it follows from the statute’s qualified inactivity condition.Source: §4.1 · pp. 12–13
• The election pamphlet’s statement that a ballot will not count after an equal ranking appears more restrictive than either Stop or Truncate.The authors conclude that this pamphlet language does not independently determine when an overvote renders a ballot inactive.Source: §4.1 · p. 13
• For any set of continuing candidates, every ballot Truncate counts is counted for the same candidate under Stop, while Stop counts some additional ballots.The authors argue that this inclusion relationship favors Stop under Alaska’s preference for preserving ascertainable voter choices, provided the statutory text admits both interpretations.Source: §4.1 · p. 13

4.2 Duplicate Rankings

• Hybrid disregards repeated marks when checking for skipped rankings but retains them for overvote detection, while the regulation does not specify how duplicate rankings interact with those statutory checks.The authors find no express basis for treating the same mark as blank for one check but present for another.Source: §4.2 · pp. 13–14
• With Truncate fixed, every ballot Hybrid counts is also counted for the same candidate under Remove and Retain, and each alternative counts some ballots Hybrid excludes.The authors say this additional exclusion weighs against Hybrid under Alaska’s preference for preserving ascertainable voter choices, but does not settle whether Remove or Retain is preferable.Source: §4.2 · p. 14

5 Related Work

• The work extends prior Alaska RCV investigations by constructing a model that reproduces published round-by-round tallies and comparing it with an independently formalized interpretation of Alaska’s statutes.Source: §5 · p. 15
• Unlike much prior formal verification work that starts with a specified voting rule, this paper treats deciding what the rule should be as part of the problem.Previous work verified voting methods in Lean, Dafny, Rocq, and other systems [12].Source: §5 · p. 15
• The paper separates a statutory specification from a model of observed tabulation behavior, enabling comparison of discrepancies in actual election results.The related formal-rcv work formalizes San Francisco election law, adopts an interpretation informed by observed practices, and has an incomplete top-level implementation correctness proof.Source: §5 · p. 15

6 Conclusion and Future Work

• The case study connects a formal interpretation of Alaska’s election rules, a verified implementation, and comparison with published results.The authors say making interpretations explicit can help legislators, administrators, and developers resolve disagreements before they affect elections.Source: §6 · p. 15
• The authors propose repeating the analysis in other jurisdictions, noting that Maine’s statute refers to an overvote at the highest continuing ranking while its regulations invalidate rankings at or below an overvote.They identify this as a way to better understand ranked-choice voting rules around the country.Source: §6 · p. 15
• The authors plan a general framework for ballot interpretation rules that characterizes relationships between rules, generates distinguishing examples, and identifies when differences can affect election outcomes.They also identify a formal account of ascertainable voter preferences as a needed part of the framework.Source: §6 · pp. 15–16

A Lean Listings

• An RCVTree leaf records an elected candidate; branch edges record defeated candidates and permitted continuations, though the type does not enforce that correspondence.Source: A Lean Listings · p. 19
• tabulate computes an RCVTree by checking write-in eligibility and first-round majority, then recursively tabulating until two candidates remain.The final-round winner is the candidate with more votes.Source: A Lean Listings · p. 19
• The first-round majority check and separate final-round handling can be omitted: recursive rounds from the initial candidates elect the same candidate(s) as tabulate.Source: A Lean Listings · p. 19

B An Election Decided by Tiebreaking

• A tie between B and C for fewest votes permits either defeat, and the resulting winner differs by which candidate is defeated.Defeating B leads to C's win, while defeating C leads to A's win.Source: B An Election Decided by Tiebreaking · pp. 19–20, Figure 5 · p. 20
• The example has three candidates and seven ballots; initial tallies are A: 3, B: 2, and C: 2.Source: B An Election Decided by Tiebreaking · p. 19

C Identifying the Reproduction Model

• Only the reproduction model matches all 22 published reports; variants change one rule at a time.Source: C Identifying the Reproduction Model · p. 20, Table 3 · p. 20
• The Division's listed settings include excluding unresolved write-ins, not skipping overvoted rankings, and exhausting ballots with two or more skipped rankings.These settings formed the reproduction model's starting point.Source: C Identifying the Reproduction Model · p. 20
• A report match requires agreement on candidate tallies each round, while an all-counts match also requires agreement on blank, exhausted, and overvoted ballot counts.The two criteria differ when rule sets classify inactive ballots for different reasons.Source: C Identifying the Reproduction Model · p. 20

D Multi-Round Contests

• Among 93 contests decided in the initial round, only the 2022 governor contest has a differing ballot, due to duplicate treatment.Source: D Multi-Round Contests · p. 20, Table 4 · p. 21
• The table covers 22 contests that went past the initial round plus the 2022 governor contest, reporting final-round margins and differing ballots by rule.A margin is the winner's lead over the runner-up in the final round.Source: D Multi-Round Contests · pp. 20–21, Table 4 · p. 21
• The reproduction model (T/H) matches every report, while S/Ret is the statutory model.Source: D Multi-Round Contests · p. 21

• LLMs helped construct Lean proofs and some declarations after the authors specified them in natural language.Source: E Use of Large Language Models · p. 21
• The authors wrote or personally reviewed all major formal definitions and theorem statements, while Lean’s kernel checks proofs regardless of how they were produced.Source: E Use of Large Language Models · p. 21
• LLMs also assisted with manuscript revision, citation management, and identifying potentially relevant legal precedent; the authors remained responsible for their interpretations and arguments.Source: E Use of Large Language Models · p. 22