Provides advanced logical reasoning through Model Context Protocol integration with the Coq proof assistant, enabling automated dependent type checking, inductive type definitions, property proving with custom tactics and automation, and robust error handling.
Unlock the full potential of MCP-RoCQ through LangDB's AI Gateway. Get enterprise-grade security, analytics, and seamless integration with zero configuration.
Free tier available • No credit card required
There may be a better way to set this up with the coq cli or something. Anyone want to try and fix it who knows what they are doing would be great.
MCP-RoCQ is a Model Context Protocol server that provides advanced logical reasoning capabilities through integration with the Coq proof assistant. It enables automated dependent type checking, inductive type definitions, and property proving with both custom tactics and automation.
Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
https://github.com/coq/platform
git clone https://github.com/angrysky56/mcp-rocq.git
cd to the repo
uv venv ./venv/Scripts/activate uv pip install -e .
"mcp-rocq": { "command": "uv", "args": [ "--directory", "F:/GithubRepos/mcp-rocq", "run", "mcp_rocq", "--coq-path", "F:/Coq-Platform~8.19~2024.10/bin/coqtop.exe", "--lib-path", "F:/Coq-Platform~8.19~2024.10/lib/coq" ] },
pip install -r requirements.txt
The server provides three main capabilities:
{ "tool": "type_check", "args": { "term": "", "expected_type": "", "context": ["relevant", "modules"] } }
{ "tool": "define_inductive", "args": { "name": "Tree", "constructors": [ "Leaf : Tree", "Node : Tree -> Tree -> Tree" ], "verify": true } }
{ "tool": "prove_property", "args": { "property": "", "tactics": [""], "use_automation": true } }
This project is licensed under the MIT License - see the LICENSE file for details.
Discover shared experiences
Shared threads will appear here, showcasing real-world applications and insights from the community. Check back soon for updates!