Brainstorming for the GenAI-accelerated TLA+ challenge

[Federico Ponzi]

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?

Thanks,

Federico

[Markus Kuppe]

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

[Younes]

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.

---

[Markus Kuppe]

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

M.

> --
> 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+u...@googlegroups.com.
> To view this discussion visit https://groups.google.com/d/msgid/tlaplus/6cdd7cf9-6bb5-423a-a799-b47fa730ea15n%40googlegroups.com.

[Irwansyah Irwansyah]

Hi all,

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.

Overall, there are so many barriers to entry to pickup TLA+ and that is why rarely people using it. If no one attacking the barriers to entry problem then the situation in the future will be the same. No one will pickup TLA+. 

The other thing is, the support from the community. Is the community inclusive to new comer? Is new comers feel welcome to learn TLA+? As the saying goes: If you want to go fast, go alone. If you want to go far, find a company.

Linux made revolution because there are people that guide/help Linus to write a portable OS. Rails also, there are people that guide/help DHH in learning Ruby and write better framework. I wish Lamport's vision for TLA+ can come true and revolutionize software development.

Irwan

> 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.