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 or Philidor position, say.
(For perspective: eight years ago, proving in a formal proof system that the sieve of Eratosthenes always gives correct results was hard, and apparently couldn't be done in at least some systems; now it is a student project in at least one system, and something that an expert can hack overnight (in a make-do fashion) in at least another.)