{"repo":"LLM4Rocq/rocq-mcp","free":true,"listed":false,"github":"https://github.com/LLM4Rocq/rocq-mcp","clone":"git clone https://github.com/LLM4Rocq/rocq-mcp.git","description":"MCP server for the Rocq prover","language":"Python","stars":41,"topics":[],"license":"Apache-2.0","category":"mcp-servers","readme_excerpt":"rocq-mcp 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 — or dune rocq top for modern (using rocq ...) projects — once per (coq.theory ...) / (rocq.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 ","default_branch":null,"files":null,"tree":[],"storefront":"/r/LLM4Rocq","claimed":false,"request_supported":{"post":"https://gitbuyer.com/r/LLM4Rocq/rocq-mcp/request-supported","requests":0},"note":"indexed from public GitHub; nothing is for sale on this page. Clone it from GitHub. Paid listings live at /search."}