Re: [tlaplus] Brainstorming for the GenAI-accelerated TLA+ challenge

Let say someone wants to build a donation site for live streamer where users can send money donation to their favorite streamers through payment gateways like Stripe, Paypal, etc. How can she do that? Will studying logic puzzle examples help her to write the TLA+ specs? Will reading all books and sites on TLA+ help her to write the specs? No, they will get even more confused since instead of learning TLA+ they will have to face with additonal option and complexity which is PlusCal? If they opted not to use the native Eclipse based IDE and go with the VSCode plugin, another complexities with different with different behavior then Eclipse one.

On Wednesday, June 11, 2025, Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx> wrote:

Thanks for the reminder. I forgot to create a related issue: https://github.com/tlaplus/tlaplus/issues/1196.

M.

> On Jun 10, 2025, at 7:24 AM, Younes <younesagma@xxxxxxxxx> wrote:
>
> Hi, and thank you for the great work!
> I was wondering if there are any TLA+ datasets (coding problems, with problem statements, and their solutions); these could be used for a variety of things: by language models, or by benchmarks; for instance, Aider uses Exercism, but TLA+ is not supported for benchmarks. If we had that, I could for example run Aider against TLA+ exercises using different models, and get the results. I would be able to pick, based on the benchmarks, which models perform best for TLA+. Of course, I do understand that benchmarks do not really measure "objectively" how good an LLM is in TLA+, but at least, it gives an idea when picking up the tool/model. TLA+ could even have its own "independent" benchmark against different LLMs, and it could be shared with the community and people could run it against all sorts of LLMs and have results published.. I think the CommunityModules are already a good start for a dataset in that regard.
> Also, I was thinking maybe we could have this great repo (https://github.com/tlaplus/awesome-tlaplus) have a dedicated section for LLM/AI and eventually point to the MCP server PR (I personally didn't know this was done until I saw it on LinkedIn).
> Y.
> ---
>
>
> On Thursday, May 22, 2025 at 7:57:15 PM UTC+2 Markus Kuppe wrote:
> I'm afraid I'm not eligible to participate in the challenge, but I've just contributed a TLA+ MCP server that integrates SANY and TLC into agentic workflows in VSCode, Cursor, or any other environment that supports MCPs. The PR [1] shows how to set up the server.
>
> Markus
>
> [1] https://github.com/tlaplus/vscode-tlaplus/pull/379
>
> > On May 14, 2025, at 1:40 PM, Federico Ponzi <fpon...@xxxxxxxxx> wrote:
> >
> > Hi all,
> >
> > In reference to the challenge: https://foundation.tlapl.us/challenge/index.html what are you planning to work on? If you're not planning to partecipate, are there any tools you wish existed and wouldn’t mind sharing, in case someone else wants to implement them?
>
> --
> You received this message because you are subscribed to the Google Groups "tlaplus" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@googlegroups.com.
> To view this discussion visit https://groups.google.com/d/msgid/tlaplus/6cdd7cf9-6bb5-423a-a799-b47fa730ea15n%40googlegroups.com.

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/2EBFA6F0-83A1-4531-BD07-113C75DE121F%40lemmster.de.