Obvious reply that most likely wasn't made as such simply because this question was posed eight years ago: wouldn't it be an appealing exercise to give a human-readable formal proof (in Lean, Coq, etc.) that certain endgames are drawn or won? I'm thinking of "cases where the algorithm is non-trivial, and where it is clear that the arguments given in endgame textbooks (a) are conceptual rather than merely brute-force, (b) could in principle be turned into actual proofs".

It seems that there is a bitnof work on this issues, but more along the lines of "formally verify brute-force databases on K v. K and Q/R/B/N endings". I'm thinking more along the lines of the Lucena position, say.