Isabelle-MCP

MCP server that lets AI agents (Claude Code, Codex, …) drive the Isabelle theorem prover through its LSP/PIDE commands — fully autonomously, with no human in the loop.

Purpose

This MCP server exists so that Claude / Codex can issue Isabelle LSP commands without any human mediation. The entire Isabelle process is encapsulated behind the MCP tools — it exposes no UI to the user. The agent works by editing .thy/.ML files on disk and calling the tools to evaluate them and query proof states; nobody watches or steers the prover interactively.

This server is not designed for human–AI collaboration (there is no jEdit/VSCode front-end in the picture). It implements a single AI ↔ Isabelle, no-human-in-the-loop model.

⚠️ One agent per server instance. This server holds a single Isabelle session with global mutable state — one set of open documents, one perspective, and one evaluation in flight at a time. It is single-threaded and not concurrency-safe: pointing multiple agents at one instance, or interleaving concurrent requests, corrupts the evaluation and document state with catastrophic, hard-to-debug results. The server runs over stdio, so each agent already gets its own dedicated server process (and its own isabelle mcp_server) — just don't share one or drive it concurrently.

Quick Start

pip install isabelle-mcp      # or: uv tool install isabelle-mcp

# register into Claude Code / Codex (auto-detects whichever is installed):
isabelle-mcp install

For Claude Desktop, register manually instead (~/.config/claude/claude_desktop_config.json):

{
  "mcpServers": {
    "isabelle": {
      "command": "isabelle-mcp"
    }
  }
}

Tools

With isabelle_launch(session, debug=true) the ML debugger tools come alive (eleven more tools): set/delete/list breakpoints on compiled Isabelle/ML code (isabelle_set_breakpoint, isabelle_del_breakpoints, isabelle_list_breakpoints, isabelle_list_breakable_sites), arm and disarm them in bulk (isabelle_enable_all_breakpoints, isabelle_disable_all_breakpoints), and work with hits — threads stopped at a breakpoint: inspect (isabelle_debug_state), evaluate ML in a stack frame's scope (isabelle_eval_at_breakpoint), print a frame's locals (isabelle_locals_at_breakpoint), resume (isabelle_continue_breakpoint) and single-step (isabelle_step_at_breakpoint). A hit pauses the evaluation: the isabelle_evaluate_to result leads with a hit report (position, call stack, frame-0 locals), and asynchronous events arrive as one-line debugger notices on the next tool result. The full design lives in docs/archive/DEBUGGER_DESIGN.md.

All positions are 1-indexed. File paths must be absolute.

Every query tool names a file and a line, and the prover answers about the command there without moving its caret — so a query can run while an evaluation is in progress, and it may only be refused for the position it asked about, not because the session is busy. A query that cannot produce a result says why ("this command is not a proof operation", "it has not finished evaluating"); nothing is concluded from a timeout.

Development

pip install -e ".[dev]"             # editable install from a checkout
pytest                              # unit tests
pytest -m integration               # requires running Isabelle
python -m mypy src/                 # type checking

Architecture

server.py         FastMCP entry point — tool registration, lifespan
lsp_client.py     JSON-RPC 2.0 client for isabelle mcp_server
tools/            Tool implementations (one file per tool)
utils/            Position conversion, URI handling, HTML parsing
models.py         Pydantic output models

License

Copyright © 2024-2026 Qiyuan Xu.

This project is free software: you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation, either version 2.1 of the License, or (at your option) any later version. See LICENSE for the full text.