Formal Verification of Minimax Algorithms
Wieger Wesselink, Kees Huizing, Huub van de Wetering
公開日: 2025/9/24
Abstract
Using the Dafny verification system, we formally verify a range of minimax search algorithms, including variations with alpha-beta pruning and transposition tables. For depth-limited search with transposition tables, we introduce a witness-based correctness criterion and apply it to two representative algorithms. All verification artifacts, including proofs and Python implementations, are publicly available.