Email Gateway (Jun 30 2026 at 07:19): Email Gateway (Jun 30 2026 at 07:19):From: Kevin Kappelmann <cl-isabelle-users@lists.cam.ac.uk>
Dear list,
We have built a Model Context Protocol (MCP) server that lets AI agents
interactively write, edit, and explore Isabelle theories and ML files. [1]
The MCP is headless and editor-agnostic. You can let the agent work on
its own or run it alongside Isabelle/jEdit or Isabelle/VSCode.
It currently requires a development version of Isabelle (we tested it
with Isabelle/c13a4bd3c018). A stable release aligned with Isabelle2026
is planned.
The README covers installation and usage notes:
https://github.com/kappelmann/isabelle-pide-mcp
Note that I/Q [2] is an alternative Isabelle MCP which provides an
Isabelle/jEdit-centred workflow.
Experience reports using both systems are very welcome: we hope that the
strengths of both MCPs can be combined in the future.
Best wishes,
Kevin
[1] https://github.com/kappelmann/isabelle-pide-mcp
[2] https://github.com/awslabs/AutoCorrode/tree/main/iq
Email Gateway (Jul 01 2026 at 14:39):From: Tobias Nipkow <nipkow@in.tum.de>
A short user report:
I have used this Isabelle-Claude Opus connection and was very pleased with it.
It worked very well for a few formal language autoformalizations.
Tobias
On 30/06/2026 09:19, Kevin Kappelmann (via cl-isabelle-users Mailing List) wrote:
Dear list,
We have built a Model Context Protocol (MCP) server that lets AI agents
interactively write, edit, and explore Isabelle theories and ML files. [1]The MCP is headless and editor-agnostic. You can let the agent work on its own
or run it alongside Isabelle/jEdit or Isabelle/VSCode.It currently requires a development version of Isabelle (we tested it with
Isabelle/c13a4bd3c018). A stable release aligned with Isabelle2026 is planned.The README covers installation and usage notes:
https://github.com/kappelmann/isabelle-pide-mcpNote that I/Q [2] is an alternative Isabelle MCP which provides an Isabelle/
jEdit-centred workflow.
Experience reports using both systems are very welcome: we hope that the
strengths of both MCPs can be combined in the future.Best wishes,
Kevin
[1] https://github.com/kappelmann/isabelle-pide-mcp
[2] https://github.com/awslabs/AutoCorrode/tree/main/iq
Email Gateway (Jul 13 2026 at 07:57):From: Kevin Kappelmann <cl-isabelle-users@lists.cam.ac.uk>
We released a version compatible with Isabelle2025-2 in branch 2025-2
of the repository:
https://github.com/kappelmann/isabelle-pide-mcp/tree/2025-2
We also improved the MCP's edit tool and added a plugin system such that
users can freely add and remove tools on their own. Enjoy!
Kevin
On 30.06.26 09:19, Kevin Kappelmann (via cl-isabelle-users Mailing List)
wrote:
Dear list,
We have built a Model Context Protocol (MCP) server that lets AI agents
interactively write, edit, and explore Isabelle theories and ML files. [1]The MCP is headless and editor-agnostic. You can let the agent work on
its own or run it alongside Isabelle/jEdit or Isabelle/VSCode.It currently requires a development version of Isabelle (we tested it
with Isabelle/c13a4bd3c018). A stable release aligned with Isabelle2026
is planned.The README covers installation and usage notes:
https://github.com/kappelmann/isabelle-pide-mcpNote that I/Q [2] is an alternative Isabelle MCP which provides an
Isabelle/jEdit-centred workflow.
Experience reports using both systems are very welcome: we hope that the
strengths of both MCPs can be combined in the future.Best wishes,
Kevin
[1] https://github.com/kappelmann/isabelle-pide-mcp
[2] https://github.com/awslabs/AutoCorrode/tree/main/iq
Email Gateway (Jul 13 2026 at 08:51):From: "\"Becker, Hanno\"" <cl-isabelle-users@lists.cam.ac.uk>
Thank you very much, Kevin, it’s great to see more work being done in this direction.
We have independently developed an initial version of a somewhat similar tool, “IC2”, which the community can find on https://github.com/awslabs/AutoCorrode/tree/main/ic2.
IC2 is an Isabelle component for headless but stateful session development. Under the hood, it is similar to isabelle server and isabelle client (in particular, built upon Headless) but it adds some conveniences we found useful, such as progress updates, cancellation, and diagnostic commands. See the README for more details. It is also integrated with I/R for dropping into fast-looped proof development in a REPL.
A notable change of direction compared to I/Q we’re exploring is the use of CLI rather than MCP. IC2 can be driven both through MCP and through CLI, but the current focus is on effective CLI-driven usage. Happy to hear about opinions/experiences here.
Once the IC2 component is registered (make -C ic2), it should (hopefully, anyway) work in any session, making it easier to setup and use than the other AutoCorrode components.
Happy about any feedback,
All the best,
Hanno
From: cl-isabelle-users-request@lists.cam.ac.uk <cl-isabelle-users-request@lists.cam.ac.uk> on behalf of Kevin Kappelmann <cl-isabelle-users@lists.cam.ac.uk>
Date: Monday, 13 July 2026 at 08:58
To: cl-isabelle-users@lists.cam.ac.uk <cl-isabelle-users@lists.cam.ac.uk>
Subject: RE: [EXTERNAL] [isabelle] PIDE MCP: Connecting AI Agents to Isabelle
CAUTION: This email originated from outside of the organization. Do not click links or open attachments unless you can confirm the sender and know the content is safe.
We released a version compatible with Isabelle2025-2 in branch 2025-2
of the repository:
https://github.com/kappelmann/isabelle-pide-mcp/tree/2025-2
We also improved the MCP's edit tool and added a plugin system such that
users can freely add and remove tools on their own. Enjoy!
Kevin
On 30.06.26 09:19, Kevin Kappelmann (via cl-isabelle-users Mailing List)
wrote:
Dear list,
We have built a Model Context Protocol (MCP) server that lets AI agents
interactively write, edit, and explore Isabelle theories and ML files. [1]The MCP is headless and editor-agnostic. You can let the agent work on
its own or run it alongside Isabelle/jEdit or Isabelle/VSCode.It currently requires a development version of Isabelle (we tested it
with Isabelle/c13a4bd3c018). A stable release aligned with Isabelle2026
is planned.The README covers installation and usage notes:
https://github.com/kappelmann/isabelle-pide-mcpNote that I/Q [2] is an alternative Isabelle MCP which provides an
Isabelle/jEdit-centred workflow.
Experience reports using both systems are very welcome: we hope that the
strengths of both MCPs can be combined in the future.Best wishes,
Kevin
[1] https://github.com/kappelmann/isabelle-pide-mcp
[2] https://github.com/awslabs/AutoCorrode/tree/main/iq
Last updated: Jul 22 2026 at 14:00 UTC