Model Context Protocol (MCP) server for Rocq/Coq proof assistant based on Coq-LSP and Petanque
Wellknown found it in public sources; nobody has proven control of it yet. Claiming takes one click if the repository is under your GitHub account, or a small file on your domain otherwise. Verified owners get the badge, 15-minute checks, status alerts, edits that outrank crawled data, and a ranking boost.
Agents can do it too: POST https://wellknown.network/api/v1/claims with {"agent":"iflow-mcp-rocq","method":"well_known_file"} — machine-readable steps at claim.json, guide at /docs/claim.
Everything here was measured by our prober or read from a registry. Nothing is self-reported.
Attributed to the source that supplied each field. Treated as claims, not facts.
# Rocq MCP Server [](https://github.com/llm4rocq/rocq-mcp/actions/workflows/tests.yml) [](https://www.python.org/downloads/) [](https://github.com/llm4rocq/rocq-mcp/blob/main/LICENSE) ## Overview This MCP server exposes the functionality of the Rocq/Coq proof assistant through a set of tools that can be used by MCP-compatible clients (like Claude Desktop). It uses the [Pytanque](https://github.com/LLM4Rocq/pytanque.git) to communicate with a [coq-lsp](https://github.com/LLM4Rocq/pytanque.git) via a Petanque server. ## Features ### Available Tools - **rocq_start_proof**: Start a proof session for a specific theorem in a Coq/Rocq file - **rocq_run_tactic**: Execute tactics or commands on the current proof state - **rocq_get_goals**: Get the current proof goals for a session - **rocq_get_premises**: Get available premises (lemmas, definitions) for the current proof state - **rocq_get_file_toc**: Get table of contents (available definitions and theorems) for a Coq/Rocq file - **rocq_search**: Search for theorems, definitions, and other objects in the current context - **rocq_parse_ast**: Parse a command and return its Abstract Syntax Tree _(only with the dev version of coq-lsp)_ - **rocq_get_state_at_position**: Get the proof state at a specific position in a file _(only with the dev version of coq-lsp)_ ### Key Capabilities - **Two communication modes**: - **Stdio mode (default)**: direct communication with `pet` process via stdin/stdout. - **TCP mode**: socket-based communication with `pet-server` via TCP. - **Interactive theorem proving**: Execute tactics and commands step by step - **Comprehensive feedback**: Access all Rocq messages (errors, warnings, sea…
Mapped onto the structured taxonomy from declared text and observed tool names. Confidence shown for derived entries.
Every source is kept verbatim. Field changes are logged as events.