Agda MCP Server

A Model Context Protocol (MCP) server that provides interactive Agda development capabilities. This enables AI-assisted proof development, interactive theorem proving, and exploration of Agda code through a standardized protocol.

Features

• Persistent REPL Session: Maintains Agda interaction state across commands, preserving goals, context, and type-checking results
• 24 Interactive Commands: Comprehensive coverage of Agda interaction operations including proof search, case splitting, and module exploration
• Automatic File Persistence: Commands that modify code (give, refine, case split, auto) automatically persist changes to disk
• HTTP Transport: Standards-compliant MCP server with HTTP/JSON-RPC transport
• Type-Safe Integration: Built with Haskell’s type system for robust MCP protocol handling
• Smart Response Formatting: Concise human-readable output by default (~90% size reduction), with optional full JSON mode

Architecture

The server runs a persistent Agda REPL in a background thread, communicating via channels:

• Commands are sent through a Chan CommandWithResponse
• Responses are routed back via MVar Response
• Each MCP tool call is converted to an IOTCM command and executed in the persistent REPL
• Goals, context, and interaction state persist between commands

File Edit Persistence

When commands modify Agda code, changes are automatically persisted to disk:

• Response capture: The REPL callback intercepts typed Response values (e.g., Resp_GiveAction, Resp_MakeCase)
• Monadic: Edit operations are in the TCM monad context using Agda’s native APIs
• Type-specific strategies: Different edit types for different operations:
  • ReplaceHole: In-place hole filling (give, refine, auto)
  • ReplaceLine: Structural edits with line insertion (case split)
  • BatchEdits: Multiple operations applied in reverse position order (auto_all)
• Position-aware: Edits preserve file structure and handle position invalidation correctly

This architecture ensures that operations like “load file” → “get goals” → “give solution” not only update the REPL state but also persist the changes to the source file.

Prerequisites

• Nix with flakes enabled
• Agda (automatically provided by Nix environment)
• Claude Code or another MCP client

Installation

1. Clone the repository:

git clone https://github.com/faezs/agda-mcp.git
cd agda-mcp

2. Enter the Nix development shell:

nix develop

3. Build the server:

cabal build

4. Run the server:

cabal run agda-mcp

The server starts on http://localhost:3000/mcp by default.

Configuration

Claude Code

Add to your Claude Code MCP configuration file (~/.config/claude-code/mcp.json):

{
  "mcpServers": {