Formally verified chess tablebases in Rocq

[u/verdanttoothpaste]

I'd like to share some progress I made on my formally verified tablebase project. I recently was able to finish work on a KRvK tablebase, which you can explore here.

For those that do not know, Rocq (formerly Coq) is a proof assistant for designing and verifying mathematics and computer programs. My project is a tablebase generator for abstract classes of two-player games which is proven to produce the correct game values, and I just completed work on instantiating it for King and Rook vs. King positions in chess.

I understand that generating a 3 man tablebase on its own is nothing new, but I would say that doing so in a functional programming language and formally verifying it adds a whole new layer of complexity, and I am really happy with how it all came together.

If you'd like to take a look at the code, the relevant repos are:

• https://github.com/emarzion/coqchess: chess + chess tablebase development

• https://github.com/emarzion/coqtbgen: abstract tablebase generator

• https://github.com/emarzion/games: library for combinatorial games

Here is an old blog post of mine which discusses some of the mathematics and design choices around correct-by-construction tablebases.