Election results should come with machine-checkable evidence that the reported winners follow from the ballots and the legal tabulation rules. Alaska's ranked-choice voting statute leaves room for interpretation in how it treats malformed ballots, such as overvotes and duplicate rankings.

The authors formalize a statutory model of AS 15.15.350 in Lean 4 in three layers: statutory vocabulary, a declarative specification of permitted outcomes, and an implementation that computes a tree of defeat sequences. They prove the implementation computes exactly the permitted outcomes. They also build a reproduction model that matches the published round-by-round tallies, selected by testing combinations of ballot-reading rules. Using Lean-checked computations, they compare the two models on published cast vote records.

Across 115 contests, kernel-checked complete tabulation trees are established for both models. 75 ballots in 10 contests were counted differently from the statutory interpretation, and no winners changed. The differences trace to overvote handling (Truncate vs. Stop) and duplicate-ranking handling, and the authors analyze the legal justification for each reading.