# Formal Verification of Minimax Algorithms

arXiv: https://arxiv.org/abs/2509.20138 · HTML: https://mlsanity.com/paper/2509.20138/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 0 of its 15 references that are in the map.
- First posted on arXiv 24 Sep 2025.

## Abstract (arXiv)

Minimax-based search algorithms with alpha-beta pruning and transposition tables are a central component of classical game-playing engines and remain widely used in practice. Despite their widespread use, these algorithms are subtle, highly optimized, and notoriously difficult to reason about, making non-obvious errors hard to detect by testing alone. Using the Dafny verification system, we formally verify a range of minimax search algorithms, including variants with alpha-beta pruning and transposition tables. For depth-limited search with transposition tables, we introduce a witness-based correctness criterion that captures when returned values can be justified by an explicit game-tree expansion. We apply this criterion to two practical variants of depth-limited negamax with alpha-beta pruning and transposition tables: for one variant, we obtain a fully mechanized correctness proof, while for the other we construct a concrete counterexample demonstrating a violation of the proposed correctness notion. All verification artifacts, including Dafny proofs and executable Python implementations, are publicly available.