About Rocq MCP
Rocq MCP is an MCP server published by sanjit-bhat in the Developer Tools category: mCP server for the Rocq prover.
Recent commit activity is the strongest signal that reported issues will get attention.
Install
git clone https://github.com/sanjit-bhat/rocq-mcpThis server has no ConduID identity, so agent calls to it are not receipted. Pin the version you install and review the source before granting it credentials.
Ask AI
Ask AI about Rocq MCP
Powered by Claude · Grounded in docs
Security checks
- ✓README presentThe repository ships documentation.
- ✓License declaredUsable under a stated license.
- !Scoped permissionsDoesn't declare a permission scope. Assume it can do anything its process can.
3 checks have not been run yet.
README
rocq-mcp
An MCP server that connects AI agents to the Rocq proof assistant.
It wraps vsrocqtop (the Rocq LSP server) and exposes proof-checking tools over MCP,
so an agent can open .v files, step through proofs, inspect goals, and fix errors interactively.
Tools
| Tool | Description |
|---|---|
rocq_open |
Open a .v file in the proof checker |
rocq_close |
Close a file and release resources |
rocq_sync |
Re-read a file from disk after editing |
rocq_check |
Check up to a position; returns goals and diagnostics |
rocq_check_all |
Check the entire file |
rocq_step_forward |
Step forward one sentence |
rocq_step_backward |
Step backward one sentence |
Output format
All proof operations return the same format: current focused goals in full, counts for any unfocused/shelved/given-up goals, prover messages, and diagnostics.
Installation
Prerequisites
Install vsrocqtop:
opam install vsrocq-language-server
Install
go install github.com/sanjit/rocq-mcp@latest
Usage
Configure your project
Add a .mcp.json to your Rocq project root:
{
"mcpServers": {
"rocq": {
"command": "./etc/run-rocq-mcp.sh"
}
}
}
Create etc/run-rocq-mcp.sh:
#!/usr/bin/env bash
ARGS=$(sed -E -e '/^#/d' -e "s/'([^']*)'//g" -e 's/-arg //g' _RocqProject)
exec rocq-mcp $ARGS
This reads your _RocqProject file and passes the flags (load paths, warnings, etc.) through to vsrocqtop.
Allow MCP tools in Claude Code
In .claude/settings.local.json:
{
"permissions": {
"allow": [
"mcp__rocq"
]
},
"enabledMcpjsonServers": [
"rocq"
]
}
Add the workflow skill
Copy .claude/skills/rocq-build/ into your project. This teaches the agent the open/check/edit/sync workflow.
Example project
See pav-proof for a working setup.
README copy captured when this server was indexed; it may lag the repository. The original is authoritative.