[isabelle] MCP resources bounds · Mirror: Isabelle Users Mailing List

Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] MCP resources bounds

Email Gateway (Sep 08 2026 at 14:23):

From: "Putti, Edoardo (UT-EEMCS)" <cl-isabelle-users@lists.cam.ac.uk>

Dear list,

As many of you all I am developing a MCP server for the Isabelle theorem prover to see what is possible today in terms of using LLMs for autoformalization.

In my work I would like to treat Isabelle/ML code as adversarial. It should be limited in how it can affect the control flow and resource usage of my MCP server.

One of the problem with this thesis is that Isabelle/ML code can always send messages to the Isabelle/Scala side. When a human is in control and has a GUI to act this is not a problem. In a headless settings instead I cannot stop the prover and Isabelle/ML code if it continuously sends me garbage.

How are you all dealing with this problem?

Other problems with the current implementation of the PIDE protocol are all based in the fact that it is trusted. This means that, when reading a PIDE frame, the following values are uncapped and can be written with arbitrary values from the Isabelle/ML side.

Header size
Chunks size
Individual Chunk size

Unfortunately I have no control over these values. I cannot setup the PIDE to reject messages that are just way too large and close the connection there are no extension points for me to implement a bounded reader.

I have mitigated the following problems in my implementation but this only happens after the fact. The ML side of the PIDE can send me arbitrary sized garbage and I will first read it into memory and then reject it.

Happy to hear your thoughts.

Edoardo

Email Gateway (Sep 08 2026 at 15:57):

From: Makarius <makarius@sketis.net>

On 08/09/2026 16:22, Putti, Edoardo (UT-EEMCS) (via cl-isabelle-users Mailing
List) wrote:

I have mitigated the following problems in my implementation but this only happens after the fact. The ML side of the PIDE can send me arbitrary sized garbage and I will first read it into memory and then reject it.
There is indeed a fundamental problem here, because the MCP violates
longstanding assumptions about how the prover works, and is used by a human
user. So any "mitigation" can only be symbolic, not really a proper solution.

At FLoC 2026 in Lisbon, I've had some discussions with users of AI + MCP. My
conclusion: we should gradually make the system more robust, and no longer let
doors and windows stand open, as an invitation to mess things up.

This will take quite some time, and it will annoy people who have done various
experiments on "hacking Isabelle" that are outside normal user space ---
depending on the very "doors and windows" to stand wide open.

Makarius

Email Gateway (Sep 08 2026 at 16:21):

From: "Mulligan, Dominic" <cl-isabelle-users@lists.cam.ac.uk>

Hi,

At FLoC 2026 in Lisbon, I've had some discussions with users of AI + MCP. My

conclusion: we should gradually make the system more robust, and no longer let

doors and windows stand open, as an invitation to mess things up.

This will take quite some time, and it will annoy people who have done various

experiments on "hacking Isabelle" that are outside normal user space ---

depending on the very "doors and windows" to stand wide open.

OK, but the alternative approach needs to come first. The alternative is that we will not update Isabelle versions or even move away from Isabelle completely. AI agent integration in 2026 is more important than moving to the latest Isabelle release.

Thanks,

Dominic

Email Gateway (Sep 09 2026 at 02:11):

From: Qiyuan XU <cl-isabelle-users@lists.cam.ac.uk>

Hi,

People try to contribute to the community and to Isabelle. The real issue, I think, is that the Isabelle sources contain very few comments. People are willing to follow conventions, but only if they first know what those conventions are ― what should be used and what shouldn't. Of course, I'm assuming here that the developers still welcome extensions to Isabelle/ML from the community, even if they remain third-party and are never merged into the main line. But if that's not the case, I'm afraid forking is the only way out for enthusiastic users. Narrowing down the "doors and windows" is certainly a good thing, since at least people will finally know what they're not supposed to use...

Hi other Isabelle hackers,

A few years ago I tried to read through the Isabelle sources by hand. It was a challenging and painful stretch of time, given the lack of documentation and comments. But I've since found that Claude Code is remarkably good at reading and understanding code; I think it's more than capable of giving you everything you need, if you could use it properly, e.g. by questioning what it says and actively spawning subagents to verify its conclusions.

Hi Dominic,

I think one option is to use patch management (e.g., https://github.com/xqyww123/my_better_isabelle_prover) to keep track of the changes you have to make to the Isabelle sources, and optionally maintain your own forked release to keep your own ecosystem consistent (e.g., https://conda.qiyuan.me). All of this was done through vibe coding and took me only a few days. I also set up a release pipeline (driven by checklist docs) so that whenever a new Isabelle version comes out, I can update everything with a single Claude Code instruction.

Best wishes
Qiyuan

From: cl-isabelle-users-request@lists.cam.ac.uk <cl-isabelle-users-request@lists.cam.ac.uk> on behalf of Mulligan, Dominic <cl-isabelle-users@lists.cam.ac.uk>
Sent: Wednesday, 09 September 2026 00:21:22
To: cl-isabelle-users@lists.cam.ac.uk <cl-isabelle-users@lists.cam.ac.uk>
Subject: Re: [isabelle] MCP resources bounds

[Alert:
Non-NTU Email] Be cautious before clicking any link or attachment.

Hi,