Quick Install

Copy the config for your editor. Some servers may need additional setup — check the README.

Add to claude_desktop_config.json:

{
  "mcpServers": {
    "rocq-mcp": {
      "command": "uvx",
      "args": [
        "rocq-mcp"
      ]
    }
  }
}

Or install with pip: pip install rocq-mcp

README Excerpt

An [MCP](https://modelcontextprotocol.io/) server for [Rocq](https://rocq-prover.org/) (formerly Coq) proof development. It exposes compilation, verification, querying, and interactive tactic stepping as MCP tools, so that LLM agents can write and check Rocq proofs. - **Rocq / Coq** -- `coqc` must be on your `PATH` (needed by all tools). If the workspace contains a `_RocqProject` or `_CoqProject` file, the server parses it for load-path flags (`-Q`, `-R`, `-I`). For **dune projects** (no `_CoqPr

Tools (20)

ROCQ_COMPILE_MULTI_ERROR_CAPROCQ_COMPILE_MULTI_ERROR_TIMEOUTROCQ_COQC_BINARYROCQ_COQC_TIMEOUTROCQ_ENRICHMENT_TIMEOUT_CAPROCQ_MAX_PET_RSS_MBROCQ_MAX_SOURCE_SIZEROCQ_MAX_STATESROCQ_PET_TIMEOUTROCQ_QUERY_TIMEOUT_CAPROCQ_VERIFY_TIMEOUTROCQ_WORKSPACE_run_with_petrocq_assumptionsrocq_compilerocq_compile_filerocq_diagrocq_notationsrocq_queryrocq_step_multi

rocq-mcp

Quick Install

README Excerpt

Tools (20)

Related AI/LLM Servers