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

1. Enter the Nix development shell:

nix develop

1. Build the server:

cabal build

1. 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": {
    "agda-mcp": {
      "transport": "http",
      "url": "http://localhost:3000/mcp",
      "command": "cabal",
      "args": ["run", "agda-mcp"],
      "cwd": "/path/to/agda-mcp"
    }
  }
}

Other MCP Clients

The server implements MCP protocol version 2025-06-18 with HTTP transport. Configure your client to:

• Connect to: http://localhost:3000/mcp
• Use JSON-RPC 2.0 over HTTP POST
• Include Content-Type: application/json header
• Optionally include MCP-Protocol-Version: 2025-06-18 header

Available Tools

All tools follow the MCP naming convention (snake_case). Arguments are provided as JSON objects.

1. agda_load

Load and type-check an Agda file.

Arguments:

• file (string): Absolute or relative path to the Agda file

Example:

{
  "name": "agda_load",
  "arguments": {
    "file": "/path/to/Example.agda"
  }
}

Use Case: Must be called first before any other operations. Initializes the Agda interaction session with the specified file.

---

2. agda_get_goals

List all goals/holes in the currently loaded file.

Arguments: None

Example:

{
  "name": "agda_get_goals",
  "arguments": {}
}

Returns: List of goals with their IDs, types, and locations in the file.

Use Case: After loading a file, use this to see what needs to be proven or filled in.

---

3. agda_get_goal_type

Get the type expected at a specific goal.

Arguments:

• goalId (integer): The numeric ID of the goal (starting from 0)

Example:

{
  "name": "agda_get_goal_type",
  "arguments": {
    "goalId": 0
  }
}

Returns: The expected type that should fill this goal.

Use Case: Understand what type of expression is needed to complete a proof.

---

4. agda_get_context

Get the context (available variables and their types) at a specific goal.

Arguments:

• goalId (integer): The numeric ID of the goal

Example:

{
  "name": "agda_get_context",
  "arguments": {
    "goalId": 0
  }
}

Returns: List of variables in scope at this goal with their types.

Use Case: See what variables and hypotheses are available to use in a proof.

---

5. agda_give

Fill a goal/hole with a complete expression.

Arguments:

• goalId (integer): The numeric ID of the goal to fill
• expression (string): The Agda expression to use (e.g., "zero", "suc n", "refl")
• format (string, optional): "Concise" (default) or "Full"

Example:

{
  "name": "agda_give",
  "arguments": {
    "goalId": 0,
    "expression": "refl"
  }
}

Effect:

• Fills the goal in the REPL
• Automatically updates the file: Replaces {! !} with the expression
• Returns success/failure to the LLM

Use Case: Complete a goal when you have the full solution. The file is automatically edited.

---

6. agda_refine

Refine a goal with a constructor or function, introducing new sub-goals.

Arguments:

• goalId (integer): The numeric ID of the goal to refine
• expression (string): Constructor or function name (e.g., "suc", "zero", "+")
• format (string, optional): "Concise" (default) or "Full"

Example:

{
  "name": "agda_refine",
  "arguments": {
    "goalId": 0,
    "expression": "suc"
  }
}

Effect:

• Applies constructor/function to the goal
• Automatically updates the file: Replaces {! !} with applied constructor and new holes
• Returns new goal structure

Use Case: Make progress on a goal by applying a constructor, which creates new sub-goals for the constructor's arguments. The file is automatically edited with the refinement.

---

7. agda_case_split

Split a goal by pattern matching on a variable.

Arguments:

• goalId (integer): The numeric ID of the goal
• variable (string): Name of the variable to pattern-match on
• format (string, optional): "Concise" (default) or "Full"

Example:

{
  "name": "agda_case_split",
  "arguments": {
    "goalId": 0,
    "variable": "n"
  }
}

Effect:

• Generates pattern-match clauses for all constructors
• Automatically updates the file: Deletes the line with the hole, inserts multiple clauses
• Preserves indentation
• Note: File should be reloaded after case split to see new goals

Use Case: Perform case analysis on a variable (e.g., split a natural number into zero and successor cases). The entire line is replaced with multiple pattern-match clauses.

---

8. agda_compute

Normalize and display an expression in a goal's context.

Arguments:

• goalId (integer): The numeric ID of the goal (for context)
• expression (string): Expression to normalize

Example:

{
  "name": "agda_compute",
  "arguments": {
    "goalId": 0,
    "expression": "2 + 2"
  }
}

Returns: The normalized form of the expression.

Use Case: Evaluate expressions to see their simplified form.

---

9. agda_infer_type

Infer the type of an expression in a goal's context.

Arguments:

• goalId (integer): The numeric ID of the goal (for context)
• expression (string): Expression to type-check

Example:

{
  "name": "agda_infer_type",
  "arguments": {
    "goalId": 0,
    "expression": "suc zero"
  }
}

Returns: The inferred type of the expression.

Use Case: Check what type an expression has before using it.

---

10. agda_intro

Introduce variables using the intro tactic.

Arguments:

• goalId (integer): The numeric ID of the goal

Example:

{
  "name": "agda_intro",
  "arguments": {
    "goalId": 0
  }
}

Use Case: Automatically introduce lambda-bound variables or pattern variables suggested by Agda.

---

11. agda_why_in_scope

Look up documentation and scope information for a name.

Arguments:

• name (string): The name to look up

Example:

{
  "name": "agda_why_in_scope",
  "arguments": {
    "name": "suc"
  }
}

Returns: Information about where the name is defined and why it's in scope.

Use Case: Understand the origin and definition of functions, types, or constructors.

---

Available Resources

Resources expose Agda information as readable data sources. They use URI-based routing.

1. Goals

URI Pattern: resource://goals/{file}

List all goals in the specified Agda file.

2. GoalInfo

URI Pattern: resource://goal_info/{file}/{id}

Detailed information about a specific goal, including its type, context, and location.

3. FileContext

URI Pattern: resource://file_context/{file}

Overall context and scope information for an Agda file.

Example Workflow

# 1. Start the server
cabal run agda-mcp

# 2. In Claude Code, load an Agda file
/mcp agda-mcp agda_load file="/path/to/Example.agda"

# 3. Get all goals in the file
/mcp agda-mcp agda_get_goals
# Output: 5 goals: ?0:Nat(10:12) ?1:Nat(11:12) ?2:Nat(15:12) ?3:Nat(16:12) ?4:A(20:18)

# 4. Check the type of goal 0
/mcp agda-mcp agda_get_goal_type goalId=0
# Output: ?0 : Nat

# 5. See available variables
/mcp agda-mcp agda_get_context goalId=0
# Output: Context:
#   n : Nat

# 6. Fill the goal - FILE IS AUTOMATICALLY EDITED
/mcp agda-mcp agda_give goalId=0 expression="n"
# ✓ Filled ?0 with 'n'
# File now shows: zero + n = n

# 7. Case split on a variable - FILE IS AUTOMATICALLY EDITED
/mcp agda-mcp agda_case_split goalId=1 variable="m"
# Split ?1 into 2 clauses:
#   suc zero + n = {! !}
#   suc (suc m) + n = {! !}
# File now has 2 lines instead of 1

# 8. Reload to see new goals after case split
/mcp agda-mcp agda_load file="/path/to/Example.agda"
/mcp agda-mcp agda_get_goals
# Now shows updated goal structure

File Persistence in Action

When you use commands like agda_give, agda_refine, or agda_case_split:

1. ✅ The command executes in the REPL
2. ✅ The response is captured before JSON encoding
3. ✅ File edits are extracted and applied automatically
4. ✅ The JSON response is returned to the LLM
5. ✅ Changes are persisted to disk immediately

No manual file editing needed! The MCP server handles all source modifications.

Development

Project Structure

agda-mcp/
├── src/
│   ├── AgdaMCP/
│   │   ├── Types.hs        # MCP tool and resource definitions
│   │   ├── Server.hs       # MCP handlers, REPL integration, file edit extraction
│   │   ├── FileEdit.hs     # File editing strategies (ReplaceHole, ReplaceLine, BatchEdits)
│   │   ├── Format.hs       # Response formatting (Concise/Full modes)
│   │   └── Repl.hs         # Persistent REPL adapter
│   └── Main.hs             # Entry point
├── patches/
│   └── mcp-server-header-optional.patch  # Compatibility patch
├── test/
│   ├── Example.agda        # Sample Agda file for testing
│   ├── SearchTest.agda     # Integration test with 1Lab library
│   └── PostulateTest.agda  # Postulate detection tests
├── agda-mcp.cabal          # Cabal package definition
├── flake.nix               # Nix flake for reproducible builds
└── README.md               # This file

Building from Source

# Enter development environment
nix develop

# Build
cabal build

# Run tests (TODO)
cabal test

# Install locally
cabal install

Running in Development Mode

# Rebuild and run
cabal run agda-mcp

# With verbose output (TODO: add verbose flag)
cabal run agda-mcp -- --verbose

Troubleshooting

Server Won't Start

Issue: Port 3000 already in use

bind: address already in use (Address already in use)

Solution: Kill existing process or change port (currently hardcoded to 3000).

Connection Refused from Claude Code

Issue: Failed to reconnect to agda-mcp

Possible Causes:

1. Server not running: Start with cabal run agda-mcp
2. Wrong configuration: Verify MCP config file
3. Network issues: Check that localhost:3000 is accessible

Goals Not Persisting

Issue: Goals disappear after loading file

Solution: This should not happen with the persistent REPL architecture. If it does:

1. Check server logs for errors
2. Verify the file loaded successfully with agda_load
3. Check that the REPL thread is running (look for "Starting persistent Agda REPL thread..." in logs)

Type Checking Errors

Issue: Agda reports type errors or missing modules

Solution:

1. Ensure all dependencies are installed
2. Check that your Agda library path is correctly configured
3. Load the file first with agda_load before other operations

mcp-server Patch

This project includes a patch to the mcp-server Haskell library (version 0.1.0.15) to improve compatibility with MCP clients that don't send the MCP-Protocol-Version HTTP header.

What the patch does:

• Makes the MCP-Protocol-Version: 2025-06-18 HTTP header optional
• Falls back to protocol version negotiation during the initialize handshake
• Logs warnings when header is missing but continues processing

Why it's needed: Claude Code's HTTP transport (as of version 2.0.13) sends the protocol version in the initialize JSON-RPC message but not as an HTTP header. The mcp-server 0.1.0.15 strictly requires the header per MCP spec 2025-06-18, causing connection failures.

Patch location: patches/mcp-server-header-optional.patch

This patch is applied automatically during the Nix build process via pkgs.applyPatches in flake.nix.

Technical Details

File Edit Implementation

The file persistence feature is implemented with structural awareness:

Three Edit Types:

1. ReplaceHole (Give, Refine, Auto): In-place replacement of {! expr !} with new text

   • Removes or keeps braces depending on GiveResult type
   • Preserves surrounding code structure

2. ReplaceLine (Case Split): Structural line replacement

   • Deletes the line containing the goal
   • Inserts N new clauses with preserved indentation
   • Handles both function and extended lambda cases

3. BatchEdits (SolveAll): Multiple hole fills

   • Applies edits in reverse position order (bottom-to-top)
   • Prevents position invalidation from earlier edits
   • Each solution extracted from concrete Expr

Position Safety:

• Uses Agda's Range type for precise positions (1-indexed line/col)
• Leverages getInteractionRange :: InteractionId -> TCM Range
• Sorts batch edits by position to avoid coordinate shifts

TCM Context Extraction:

• Works with typed Response values before JSON encoding
• No JSON parsing needed - uses native Agda types
• Runs in the same TCM monad as Agda interaction

Contributing

Contributions are welcome! Areas for improvement:

• Add comprehensive test suite (✓ 15+ tests implemented)
• Persistent file edits (✓ Implemented with structural awareness)
• Response formatting (✓ Concise/Full modes with 90% size reduction)
• Support for stdio transport in addition to HTTP
• Configurable port and host
• Resource URI path parsing for goal_info queries
• Verbose/debug logging modes with --verbose flag
• CI/CD pipeline
• Extended lambda case split support

License

BSD-3-Clause (same as Agda)

Acknowledgments

• Built with mcp-server Haskell library
• Powered by Agda
• Inspired by agda-mode for VSCode

---

Note: This is an experimental project. The MCP protocol and Claude Code's implementation are evolving, and this server may require updates for compatibility with future versions.