AI Atlas

Developer Tools · Education & Learning

MCP Rocq logo

MCP Rocq

angrysky56/mcp-rocq

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.

View on GitHub3

Install

Client configuration

{
  "mcpServers": {
    "server": {
      "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"
      ]
    }
  }
}
GitHub stars
3
Author
@angrysky56
Category
Developer Tools, Education & Learning
License
MIT
Updated
Oct 6, 2026

About MCP Rocq

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.

Features

  • Automated Dependent Type Checking: Verify terms against complex dependent types

  • Inductive Type Definition: Define and automatically verify custom inductive data types

  • Property Proving: Prove logical properties using custom tactics and automation

  • XML Protocol Integration: Reliable structured communication with Coq

  • Rich Error Handling: Detailed feedback for type errors and failed proofs

Details on this page are taken from the project's README. Open README

Related MCP servers

More servers
Playwright logo

Playwright

microsoft/playwright

72.2k

Playwright is a framework for web automation and testing. It drives Chromium, Firefox, and WebKit with a single API — in your tests, in your scripts, and as a tool for AI agents.

Developer Tools
repomix logo

repomix

yamadashy/repomix

15.2k

Repomix is a tool that packs a codebase into an AI-friendly format, supporting local and remote repository processing and providing code compression, security checks and multiple output formats.

Developer Tools
UI-TARS-desktop logo

UI-TARS-desktop

bytedance/UI-TARS-desktop

12.9k

TARS is ByteDance's multimodal AI agent stack, shipping two projects: Agent TARS (a CLI and Web UI agent built on MCP) and UI-TARS-desktop (a desktop GUI agent).

Developer Tools
blender logo

blender

ahujasid/blender-mcp

10.6k

formerly blender-mcp — the PyPI package is now mcp-for-blender. Existing setups keep working; no config change is required. Read more.

Developer Tools
Playwright Browser Automation logo

Playwright Browser Automation

microsoft/playwright-mcp

9.2k

A Model Context Protocol (MCP) server that provides browser automation capabilities using Playwright. This server enables LLMs to interact with web pages through structured accessibility snapshots, bypassing the need for screenshots or visually-tuned models.

Developer Tools
2344 logo

2344

comet-ml/opik

7k

Opik is the open-source LLM observability and evaluation platform for AI agent tracing, LLM evaluation, prompt management, and production monitoring. Built by Comet. Apache-2.0 licensed, free to self-host the full platform, with 20,000+ GitHub stars.

Developer Tools