Hello all,
The first public release of `boulodrome` is finally available !
It is a MCP server for Rocq/Coq proof assistance via the Pétanque protocol
Boulodrome gives LLMs interactive access to the Rocq proof assistant.
It exposes tools for starting proof sessions, running tactics, inspecting goals, searching the library, and undoing steps, turning theorem proving into a tool-calling loop. Since it is using Rocq as a library from OCaml, the latency is very low.
For now it is only working with Rocq 9.1, on project managed by dune.
Let me know what you think about it !