rocq-mcp by LLM4Rocq - MCP Server

Rocq MCP Server

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 to communicate with a coq-lsp 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, search results)
State management: Navigate proof states and compare them
Session management: Support multiple concurrent proof sessions
AST parsing: Get abstract syntax trees for commands and file positions (only with the dev version of coq-lsp)
Position-based queries: Get states at specific file positions (only with the dev version of coq-lsp)

Prerequisites

Install coq-lsp with Petanque support:

# Install dependencies
opam install lwt logs coq-lsp

# Or install one of the dev versions of coq-lsp, e.g., for Coq.8.20
opam install lwt logs coq.8.20.0
opam pin add coq-lsp https://github.com/ejgallego/coq-lsp.git#v8.20

Installation

Install from GitHub (Recommended)

pip install git+https://github.com/llm4rocq/rocq-mcp.git

Development Installation

We recommand using uv.

Clone this repository
Use the project workflow:
```
cd rocq-mcp
uv sync
```

Usage

Running the MCP Server

# Default: stdio mode (uses 'pet' command directly)
rocq-mcp

# Use TCP mode for multi-client usage
rocq-mcp --tcp

# TCP mode with custom server configuration  
rocq-mcp --tcp --host 127.0.0.1 --port 8833

Development mode (if using uv sync):

uv run rocq-mcp
uv run rocq-mcp --tcp

Communication Modes:

Stdio mode (default): Spawns and communicates directly with the pet process via stdin/stdout. This is more efficient and simpler as it doesn't require a separate server process.
TCP mode: Starts a pet-server process and communicates via TCP socket. Use this for multi-client usage scenarios where multiple applications need to connect to the same Petanque instance.

MCP Client Configuration

Run the following command to install rocq-mcp for claude code.

claude mcp add rocq-mcp -- rocq-mcp

Note: If you are using virtual envs, rocq-mcp may not be in the path by default. First, activate the venv, and copy the path returned by which rocq-mcp. Then install rocq-mcp using this absolute path:

claude mcp add rocq-mcp -- /path/to/rocq-mcp

When you start a claude session, you can check the server with:

> /mcp

Then, simply ask claude a question.

> help me prove addnC in test.v

Testing

# Install with dev dependencies
uv sync --dev

# Run tests
uv run pytest tests/

Troubleshooting

Common Issues

Server Connection Errors

Verify port availability
Check that coq-lsp is properly installed

Installation Issues

Ensure coq-lsp is properly installed
Install lwt and logs before coq-lsp (required for pet and pet-server)
Verify pytanque dependency is correctly resolved

Note: This project was build with the help of Claude from the code of pytanque.

Related Projects

pytanque: Python client for the Petanque protocol
coq-lsp: Language server for Coq/Rocq
MCP: Model Context Protocol specification