Hello,
I would like to share a project I have been working on, a formally verified endgame tablebase generator, written in Coq.
Here is the project code. I also wrote a blog post explaining the project and some of the design choices I made, which you can read here. Finally, you can play around with some of the results I generated for a sample game here.