Email Gateway (Sep 08 2026 at 14:23): 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.
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,
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
CONFIDENTIALITY: This email is intended solely for the person(s) named and may be confidential and/or privileged. If you are not the intended recipient, please delete it, notify us and do not copy, use, or disclose its contents.
Towards a sustainable earth: Print only when necessary. Thank you.
Email Gateway (Oct 13 2026 at 14:45):From: Makarius <makarius@sketis.net>
On 09/09/2026 04:10, Qiyuan XU (via cl-isabelle-users Mailing List) wrote:
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.
Hi Qiyuan,
I am clearing out old mail threads for the final Isabelle2026 release, to see
if anything is still relevant for it. So I have briefly looked at your private
fork of the Isabelle codebase, together with various experimental addons,
notably https://github.com/xqyww123/my_better_isabelle_prover
That is a relatively new fork, and it remains to be seen how the situation
will look in a few years: Isabelle keeps moving on and on, leaving old things
eventually behind (like the already infamous REPL).
For the moment, only this one is interesting:
my_better_isabelle_prover/patches/Isabelle2024/future_assign_interrupt/future.ML.patch
(without the machine-generated speculations about what might be right or wrong).
When something looks odd in Isabelle sources, step 0 is to browse the
Mercurial history (with its authentic Mercurial ids as cross-references), to
see where the text emerged and in which historical context. Afterwards, the
history can be continued in an informed manner, by producing new changes in a
similar manner.
Here is my current result on that typical Isabelle exercise (now on the
isabelle-release repository):
changeset: 85808:9d3a192c2b3f
tag: tip
user: wenzelm
date: Tue Oct 13 13:08:18 2026 +0200
files: src/Pure/Concurrent/future.ML
description:
proper Exn.reraise exn (amending 461e924cc825) --- e.g. Exn.is_interrupt
during Single_Assignment.assign, which might occur during Timeout.apply (based
on patches/Isabelle2024/future_assign_interrupt by Xu Qiyuan);
diff -r d4d426d79523 -r 9d3a192c2b3f src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML Mon Oct 12 23:39:25 2026 +0200
+++ b/src/Pure/Concurrent/future.ML Tue Oct 13 13:08:18 2026 +0200
@@ -427,7 +427,8 @@
(case Single_Assignment.peek result of
SOME (Exn.Exn e) => Exn.reraise (if Exn.is_interrupt_proper e
then e else exn)
| _ => Exn.reraise exn)
Note that "proper XYZ" is Isabelle jargon: It means that something was
considered wrong and is now hopefully right. The amended change 461e924cc825
also had a "proper ..." in its log entry, so we see a typical example of
degrading the quality of the sources by something that would be called a "fix"
in the majority culture.
Isabelle culture uses other words and other concepts, to approximate the truth
of the development process better. Thus we have funny "tuned, clarified,
proper ..." jargon that outsiders won't understand.
Makarius
Last updated: Oct 29 2026 at 04:52 UTC