Not sure if you have looked into this discussion : https://github.com/tlaplus/tlapm/discussions/253#discussioncomment-16383825
On Tuesday, November 10, 2026 at 2:59:49 PM UTC Marco Manino wrote:
Hi everybody. I am new in this community, but I have been using TLA+ quite a while lately.
I read the other day the article from Markus about AI-assisted proofs and the new AI agent (TILAPIA). The findings matched our experience very closely, as such I want to share some of our findings as well.
One of the main pain-points are:
- the loop time (as `tlapm` can be sometimes slow, see tlaplus/tlapm#286);
- the token usage in the sense of context filling and cost.
For the second point, the problem is mainly the way the agent interacts with `tlapm`: it will soon recognize that it can accept a line (`--line`) or a line range (`--toolbox`), but the output of these operation modes is *very* verbose as it is tuned to IDE interaction and not AI interaction. As such the context fills *very* quickly with noise: the agent is forced to deal and filter information to mostly useless messages (from the AI perspective, of course). We found out that Sol 6.1 occasionally filters them with `grep` tool or `python` if available, but that's hardly enough and still consumes a lot of tokens, leading to compaction. Compaction for us has often times been a disruptive operation: most of the time it was hard for the agent to continue successfully the proof after compaction.
Another issue is that the agent struggled to understand that `tlapm` by default tried `SMTT(5)` then `ZenonT(10)` then `IsaT(30)` and wasted lots of effort trying out `BY SMT` or `BY Zenon`, etc..
In our effort to optimize for this, me and Alberto Carretero developed an MCP server (see https://github.com/marco6/tlapm-mcp) to deal with the above issues. It features 2 commands:
- `check`: a small syntax check (unfortunately it still uses `tlapm` syntax checking, we will soon try to get `SANY` to work with it)
- `prove`: the main tool. It will accept a range, print only the failed theorems and report suggestions as warnings (for the `BY <solver>` problem).
The latter will accept an agent-friendly syntax to prove theorems and, more importantly, it will provide a compact output by parsing what the `--toolbox` mode prints.
Clearly, this being an MCP is just a matter of AI being trendy these times. Nothing is stopping us from making a standalone wrapper/CLI interface for `tlapm` which is just a CLI tool.
I see that there has been already some thought into this specific problem (for example tlaplus/tlapm#290), so is there a better place to discuss this? How can we collaborate on this together? And (maybe foremost) is there interest in the community for such an effort?
Thanks,
Marco