# Rocq Mcp

> MCP server for the Rocq prover

- **Type:** MCP server
- **Install:** `agentstack add mcp-llm4rocq-rocq-mcp`
- **Verified:** Yes — security-reviewed for prompt injection and unsafe behavior
- **Seller:** [LLM4Rocq](https://agentstack.voostack.com/s/llm4rocq)
- **Installs:** 0
- **Category:** [Integrations](https://agentstack.voostack.com/c/integrations)
- **Latest version:** 0.1.0
- **License:** Apache-2.0
- **Upstream author:** [LLM4Rocq](https://github.com/LLM4Rocq)
- **Source:** https://github.com/LLM4Rocq/rocq-mcp

## Install

```sh
agentstack add mcp-llm4rocq-rocq-mcp
```

Requires the [AgentStack CLI](https://agentstack.voostack.com/docs/cli). Works with Claude Code, Cursor, and any MCP-compatible agent.

## About

# rocq-mcp

[](https://github.com/LLM4Rocq/rocq-mcp/actions/workflows/ci.yml)
[](https://www.python.org/downloads/)
[](https://github.com/LLM4Rocq/rocq-mcp/blob/main/LICENSE)

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.

- **Thirteen MCP tools** backed by [pet](https://github.com/ejgallego/coq-lsp) (Rocq's coq-lsp interactive backend).
- **Interactive tools.** Inspect proof goals, search the environment, step through tactics.
- **Staged verification.** Sandboxed audit of admits, axioms, and statement mismatches.
- **State is cached across calls** for fast iteration.

> **A note on this README.** The sections that follow are detailed reference documentation aimed primarily at **AI agents** consuming these tools (and the human operators briefing them).

## Prerequisites

- **Rocq / Coq** -- `coqc` must be on your `PATH`. If the workspace contains a `_RocqProject` or `_CoqProject` file, the server parses it for load-path flags (`-Q`, `-R`, `-I`). For **dune projects** (no `_CoqProject` but a `dune-project` file present), the server auto-detects load paths via `dune coq top` (once per `(coq.theory ...)` stanza, so multi-theory workspaces resolve cross-theory imports correctly) and writes a `_RocqProject` file in the workspace so that coq-lsp also picks them up. This generated file stays in the workspace and should be added to `.gitignore`. Otherwise it defaults to `-Q  Test`.
- **pet** (from [coq-lsp](https://github.com/ejgallego/coq-lsp)) -- **recommended**. Powers the interactive tools (`rocq_query`, `rocq_assumptions`, `rocq_start`, `rocq_check`, `rocq_step_multi`, `rocq_toc`, `rocq_notations`) and the proof-state enrichment / multi-error walker on `rocq_compile_file`. Without `pet` you fall back to `coqc`-only operation: `rocq_compile`, `rocq_compile_file` (first error only, no goals), `rocq_verify`, `rocq_diag` — a substantial reduction in what an agent can do.
- **Python 3.11+**

## Installation

Using [uv](https://docs.astral.sh/uv/):

```bash
# Install (includes pytanque for interactive tools)
uv pip install -e .
```

For development (includes pytest):

```bash
uv pip install -e ".[dev]"
```

## Tools

The server exposes thirteen MCP tools:

### Compilation tools (coqc-based, no pytanque needed)

| Tool | Description |
|------|-------------|
| **`rocq_compile`** | Batch-compile Rocq source code via coqc. Best for checking a finished proof. On error, returns error positions and a `state_capture_status` field; when `pet`/coq-lsp is available and the failure is inside a proof, also returns a reusable `state_id` and the goals at the error position. For scratch iteration, prefer `rocq_start` + `rocq_check` / `rocq_step_multi` (interactive session keeps imports warm). |
| **`rocq_compile_file`** | Whole-file `coqc` compile of a `.v` file on disk. Best for finished proofs, axiom audits, and final verification. Preferred over `rocq_compile` for large files (source stays on disk, no full-text transmission over MCP). On error, returns error positions and a `state_capture_status` field; when `pet`/coq-lsp is available and the failure is inside a proof, also returns a reusable `state_id` and the goals at the error position. Cleans up compilation artifacts but preserves the source file. Three opt-in tuning kwargs (`keep_vo`, `mode`, `timing`) — see the **Compile-file options** callout below. For scratch iteration, prefer `rocq_start` + `rocq_check` / `rocq_step_multi` (interactive session keeps imports warm). On failure with `pet` available, the response also carries an `errors` list with per-declaration entries — see the Multi-error reporting callout below. |
| **`rocq_verify`** | Verify that a proof actually proves the original statement. Wraps in a `Module M.` sandbox to catch type redefinition, `Admitted`/`Abort`, custom axioms, and statement mismatches. Run after `rocq_compile` or `rocq_compile_file` succeeds. |

### Interactive tools (pytanque-based, require `pet`)

| Tool | Description |
|------|-------------|
| **`rocq_query`** | Search the Rocq environment — find lemmas, check types, inspect definitions. Three context modes: **preamble** (import commands as a string), **file** (a `.v` file path whose definitions are in scope), or **from_state** (a live `state_id` from a `rocq_check` session — the query sees opened scopes, hypotheses, and local definitions). Use `from_state=` to introspect mid-proof without re-specifying preamble. Optional `max_results` parameter limits output for broad searches. Does not modify any proof state. |
| **`rocq_assumptions`** | List the axioms a theorem depends on. Takes a required `file` parameter (path to the `.v` file where the theorem is defined) to set up the full environment. Returns `assumptions: list[str]` of `"name : type"` pairs from `Print Assumptions` (empty when the theorem is closed under the global context) plus the full `raw_output` for agents that want it. No classification — `rocq_assumptions` is pure introspection; the agent decides what's safe to trust. Use `rocq_verify` for a sandboxed admit-free / axiom-policy decision on a candidate proof. |
| **`rocq_start`** | Start an interactive proof session and return proof goals. Three modes: (1) by theorem name, (2) by position — jump to any point in a file to inspect proof goals there (e.g., error positions from `rocq_compile`); cursor rounds forward through the sentence containing it, so a cursor anywhere on a sentence (including its period) yields the state **after** that sentence, and whitespace before a sentence yields the state **before** it (see docstring for the full rule), (3) from imports. Returns a `state_id` for use with `rocq_check` and `rocq_step_multi`. Optional `force_restart=True` kills pet and clears the state table — recovery primitive for accumulated RAM bloat, indexing corruption, or a state expiry that repeats after a plain retry (see Concurrency model). |
| **`rocq_check`** | Run proof commands with cached imports — fast iterative checking. **Requires `from_state`** (the `state_id` returned by `rocq_start` or a previous `rocq_check`). On error, returns `last_valid_state_id` for immediate recovery via `rocq_check(from_state=...)` or `rocq_step_multi(from_state=...)`. Includes `stale_warning` if the source file was modified since session start. |
| **`rocq_step_multi`** | Try multiple tactics at once — find what works without guessing. **Requires `from_state`**. Useful for auto-solving subgoals (pass standard automation tactics) or exploring proof structure. Does not advance the state; commit the winner with `rocq_check`. Max 20 tactics per call. |
| **`rocq_toc`** | Get the structure of a `.v` file: all definitions, lemmas, theorems, and sections as a hierarchical outline. Does not require an active session. |
| **`rocq_notations`** | List all notations in a Rocq statement and how they resolve (which scope, which module). Helps debug notation ambiguity (e.g., is `+` in `nat_scope` or `Z_scope`?). |

### Diagnostic tools

| Tool | Description |
|------|-------------|
| **`rocq_diag`** | Operational diagnostics: pet health, memory headroom, system load average, recent errors, currently-live proof states. Use after `pet_restarted: True` to diagnose what happened, before a long `vm_compute` to check memory headroom, or **as an orchestrator's monitoring primitive** — call it between sub-agent dispatches to spot shared-pet contention (`live_states[*].file` shows entries from peer callers), accumulating RAM bloat, or a pile-up in `recent_errors`. Does not spawn pet if it is not running; safe to call without `pet` installed. |
| **`rocq_health`** | Toolchain health check: returns `ok` plus **which opam switch** the server is running on and the resolved `coqc` / `pet` binary paths + versions. An MCP server inherits its `PATH` / opam environment from whatever launched it (e.g. an `opam exec --switch= -- …` wrapper), which can differ from your interactive shell — so call this first when `coqc` behaves like a different version than you expect, or when a proof that built before now fails. Read-only; does not spawn pet. (`rocq_diag` is for *runtime* health; `rocq_health` is for *toolchain* health.) |
| **`rocq_switch`** | Change the running server's opam switch in-session: resolves the switch via `opam env`, applies it to the live process, and kills pet so the next call respawns under the new switch. **Sharp tool** — clears the state table (all live `state_id`s are discarded; restart sessions with `rocq_start`), and `.vo` artifacts built under the old switch may be ABI-incompatible. The change is process-global (affects every agent sharing this server). For a stable per-deployment switch, prefer pinning it at launch (see the **Switch selection** callout). |

> **Switch selection:** The server resolves `coqc` and `pet` from the `PATH` / opam environment of **the process Claude Code (or your MCP client) launched** — *not* from your interactive shell. So the switch is fixed at server-launch time and can silently differ from `opam switch show` in your terminal. Pin it explicitly in the MCP client config, e.g. register the server command as `opam exec --switch= -- uv run --directory  rocq-mcp`, or set `env: { … }` (PATH / OPAM_SWITCH_PREFIX). Call `rocq_health` to see the switch the server is actually on. To change it: either edit the launch command and reconnect the MCP server (`/mcp` → reconnect, or restart the client), or call `rocq_switch(name=…)` to swap in-session — the latter clears all live `state_id`s and may leave `.vo` artifacts ABI-incompatible, so prefer the launch-time pin for a stable setup.

> **Stale file warning:** Interactive sessions (`rocq_start` / `rocq_check` / `rocq_step_multi`) read the `.v` file at session start and do not track subsequent edits. If another process or agent modifies the file while a session is active, the proof state becomes stale and tactics may fail or produce wrong results. In multi-agent setups, **work on a copy of the file** for interactive proving, or restart the session with `rocq_start` after edits. A `stale_warning` field is returned when a file modification is detected. See also the [Concurrency model](#concurrency-model) section below.

> **Workspace auto-detection:** When a file-accepting tool (`rocq_compile_file`, `rocq_query`, `rocq_assumptions`, `rocq_toc`, `rocq_start`) is called without an explicit `workspace`, the server walks up from the file's directory looking for `_RocqProject`, `_CoqProject`, or `dune-project` markers and uses the directory of the innermost match. Falls back to `ROCQ_WORKSPACE` if no marker is found. Pass `workspace=` explicitly to override (e.g. for monorepos with nested project files).

> **Workspace warning:** When the resolved workspace contains no `_RocqProject` / `_CoqProject` / `dune-project` marker AND the call provided explicit `workspace=` or a `file=` hint, the response carries `workspace_warning: str` advising on the load-path resolution. Source-string tools without `workspace=` / `file=` (the legitimate scratch / one-off workflow) stay quiet.

> **.vo rebuild warning:** When `rocq_compile_file` rewrites `.vo` artifacts in a workspace that has one or more active interactive sessions (`rocq_start` / `rocq_check` / `rocq_step_multi`), the response carries `vo_rebuild_warning: str` advising the other agents to call `rocq_start` again to refresh held dependency state. Quiet when no `.vo` changed, when no interactive session lives in this workspace, or when the workspace exceeds the internal scan cap. *Calling `rocq_compile_file` with `keep_vo=True` makes the `.vo` persist between calls, so subsequent compiles of the same file are more likely to trip this warning.*

> **Multi-error reporting:** When `rocq_compile_file` fails (`reason: "compile_error"`) and `pet` is available, the response carries `errors: list[dict]` with per-declaration entries (`proof_name`, `kind`, `start_line`, `end_line`, `code`, `message`) covering errors in named declarations and top-level vernaculars (broken `Require`, broken `Notation`, etc.) reached via inter-chunk regions. This surfaces additional errors beyond the first one coqc reports; cascade failures within a single proof body are deduplicated. Collection stops at `ROCQ_COMPILE_MULTI_ERROR_CAP` (default 20; set to `0` to disable). The field can be present and **empty** (`errors: []`) when the walker ran but pet did not reproduce the coqc-reported failure — treat it as "no additional errors found" rather than "no errors at all." Quiet on successful compiles, when `pet` is unavailable, and on source-string `rocq_compile` (this feature is `rocq_compile_file` only).

> **Compile-file options:** `rocq_compile_file` accepts three opt-in tuning kwargs. All default off — pure additions, no behavior change to the baseline call.
>
> - **`keep_vo=True`** preserves the produced `.vo`/`.vok`/`.vos` artifacts. Useful when a sibling file `Require`s the result; the default behavior is to clean every artifact except the source `.v`. *Combining `keep_vo=True` with `mode="vos"` produces only a `.vos`* — downstream full-mode `Require Import` will then fail with `"Unable to locate library ... (.vos file)"`. Use `keep_vo=True` with `mode="full"` when the sibling consumer expects a `.vo`.
> - **`mode="vos"`** selects a fast statements-only pre-pass (`coqc -vos`). Skips proof bodies *entirely* — does NOT execute them — so it catches missing imports, statement type errors, holes, and notation conflicts in seconds, but accepts any proof body (`Theorem t : False. Proof. exact I. Qed.` passes under `"vos"`). Use as a cheap pre-pass during iteration, then run `mode="full"` for the real check.
> - **`timing=True`** runs coqc with `-time` and adds a `timing: {total_sentences, top_slowest, last_completed}` response field carrying per-sentence diagnostics; `top_slowest` is capped at 5 by descending duration. On timeout, `last_completed` is woven into the error string: `"timed out after 590s. Last completed sentence: line 221 [Theorem.foo] (15.3s)"`. On a successful compile, `last_completed` is the file's literal final sentence (not a failure marker).

> **Proof-tactics chain status:** When a `rocq_check` call finishes a proof (`proof_finished: True`), the server walks the LRU state table backward from the leaf to reconstruct `proof_tactics`. If an ancestor state was LRU-evicted, or (defensively) a cycle is detected, the walk cannot complete; the response then **omits** `proof_tactics` and `proof_hint` and carries `proof_tactics_status` (`"ancestor_evicted"` or `"cycle"`), `proof_tactics_broken_at: int` (the state id where the walk gave up), and a short `proof_tactics_hint` instead. Clients that ignore these keys see no half-chain — they never render a partial walk as a finished proof.

> **Per-call timeout clamp:** When any pet-routed tool (`rocq_query`, `rocq_start`, `rocq_step_multi`, `rocq_check`, `rocq_assumptions`, `rocq_toc`, `rocq_notations`) is invoked with `timeout=` exceeding `ROCQ_QUERY_TIMEOUT_CAP` (default 300), the call runs with the cap as the actual budget and the response carries `clamped_timeout: `. The `timeout=` parameter is the user's request; `clamped_timeout` is the server-side ceiling.

### Choosing a tool

The tools table above is reference-style.  This subsection is intent → tool: find the row that matches what you want to do, then read its tool's full entry above for details.

| If you want to... | Use |
|---|---|
| Iteratively develop a single proof, trying tactics | `rocq_start` + `rocq_check` / `rocq_step_multi` |
| Inspect proof state at a specific line / character | `rocq_start(file=..., line=..., character=...)` — cursor rounds forward through its sentence; point at whitespace **before** a sentence for state-before |
| Search for a lemma by pattern (e.g. `S

…

## Source & license

This open-source MCP server is cataloged on AgentStack and links to its original source — we do not rehost the code.

- **Author:** [LLM4Rocq](https://github.com/LLM4Rocq)
- **Source:** [LLM4Rocq/rocq-mcp](https://github.com/LLM4Rocq/rocq-mcp)
- **License:** Apache-2.0

Install and usage instructions live in the source repository linked above.

## Pricing

- **Free** — Free

## Security capabilities

Automated source analysis of v0.1.0 — what this tool can access:

- **Network access:** no
- **Filesystem access:** no
- **Shell / process execution:** yes
- **Environment & secrets:** no
- **Dynamic code execution:** no

*"Yes" means the capability is present in the source — more access means more to trust, not that it is unsafe.*


## Versions

- **0.1.0** — security scan: passed — Imported from the upstream source.

## Links

- Listing page: https://agentstack.voostack.com/l/mcp-llm4rocq-rocq-mcp
- Seller: https://agentstack.voostack.com/s/llm4rocq
- Browse the marketplace: https://agentstack.voostack.com/browse

---
Listed on AgentStack — the marketplace for AI agent skills and MCP servers. Every listing is security-reviewed. Creators keep 70%.