[lykqvrjf] Verifying an endgame playing algorithm

Given black box computer program which claims to be able to give a winning move for every winning position within a certain class of chess endgames, how would one verify the claim?  The answer is brute force, but the exact details seem hairy.  In particular, this program is not required to give the move which gives the quickest way to win, so the checker needs to verify that the program eventually makes progress against every possible defense.  This requires some sort of graph analysis.

Is there a way to probabilistically verify such a claim?  What if it were not a black box, but we can look inside for corner cases?

Other claims to verify: Can hold any drawn position.  Provides the most stubborn defense to any losing position.

Motivation was programs smaller than tablebases to play endgames, with an eye toward playing them on much larger boards.