Formal Verification of Minimax Algorithms

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. The document is 18 pages long and is a revised and extended version submitted to CAV 2026. It can be cited as arXiv:2509.20138 [cs.AI] or arXiv:2509.20138v2 [cs.AI] for this version, with the DOI https://doi.org/10.48550/arXiv.2509.20138, which is an arXiv-issued DOI via DataCite. The submission history includes two versions, with the first version submitted on September 24, 2025, and the second version submitted on April 22, 2026.