Rocq Mcp

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 server for Rocq (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 (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) -- 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:

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

For development (includes pytest):

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_ids 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 / OPAMSWITCHPREFIX). 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_ids 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 Requires 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
• Source: LLM4Rocq/rocq-mcp
• License: Apache-2.0

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