About Rocq MCP
Rocq MCP is an MCP server published by sanjit-bhat in the Developer Tools category: rocq MCP Server. It has been installed 0 times through Conduid.
The repository has 1 stars and 0 forks, with the last commit 6 months ago. Six months or more without a commit doesn't mean the server is broken, but check the open issues (0) before depending on it in production.
Install
npx 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 presentNot checked yet.
- ·License declaredNot checked yet.
- ·Tests presentNot checked yet.
- ·Dependencies pinnedNot checked yet.
- ·No dynamic code executionNot checked yet.
- !Scoped permissionsDoesn't declare a permission scope. Assume it can do anything its process can.
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 mirrored from the source repository 4 months ago. The original is authoritative.