Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

GenAI-Accelerated TLA+ Challenge

foundation.tlapl.us

Post reply on HN
Print view View original

11–17 of 17 posts

Re: GenAI-Accelerated TLA+ Challenge

#11

Post by jjmarr »

warkdarrior wrote: post #10
max_ wrote: post #9

Leslie Lamport said that he invented TLA+ so people could "think above the code". It was meant as a tool for people to improve their thinking and description of systems. LLM generation of TLA+ code is just intellectual masterbation. It may get the work done for your boss. But you intellect will still remain bald — in which case you are better off not writing TLA+ at all.

> [TLA+] was meant as a tool for people to improve their thinking and description of systems. Why the speciesism? Why couldn't LLMs use TLA+ by translating a natural-language request into a TLA+ model and then checking it in TLA+?

Not the OP, but I would rather give a formal specification of my system to an AI and have it generate the code.

I believe the point is it's easier for a human to verify a system's correctness as expressed in TLA+ and verify code correctly matches the system than it is to correctly verify the entire code as a system at once.

Then, if my model of the system is flawed, TLA+ will tell me.

I'm an AI bull so if I give the LLM a natural language description, I'd like the LLM to explain the model instead of just writing the TLA+ code.

Re: GenAI-Accelerated TLA+ Challenge

#12

Post by justanotheratom »

svieira wrote: post #5
justanotheratom wrote: post #4

Earlier quoted context omitted.

maybe run it through few other LLMs depending on how much confidence you need - o3 pro, gemini 2.5 pro, claude 3.7, grok 3, etc..

Then you need to be able to formally prove the equivalence of various TLA+ programs (maybe that's a solved problem?)

I didn't mean generate separate TLA programs. Rather, other LLMs review and comment on whether this TLA program satisfies the user's specification.

Re: GenAI-Accelerated TLA+ Challenge

#13

Post by frogmeister57 »

Using generative chatbots to write a formal spec is the most stupid idea ever. Specs are all about reasoning. You need to do the thinking to model the system in a very simplified manner. Formal methods and the generative BS are at the antipodes of reliability. This is an insult to reason. Please keep this nonsense away from the serious parts of CS.

Re: GenAI-Accelerated TLA+ Challenge

#14

Post by frogmeister57 »

Taikonerd wrote: post #2

Using LLMs for formal specs / formal modeling makes a lot of sense to me. If an LLM can do the work of going from informal English-language specs to TLA+ / Dafny / etc, then it can hook into a very mature ecosystem of automated proof tools. I'm picturing it something like this: 1. Human developer says, "if a user isn't authenticated, they shouldn't be able to place an order." 2. LLM takes this, and its knowledge of t…

It makes a lot of sense only for graphics card sales people. For everyone else with a working neuron the sole idea is utter nonsense.

Re: GenAI-Accelerated TLA+ Challenge

#15

Post by siscia »

frogmeister57 wrote: post #13

Using generative chatbots to write a formal spec is the most stupid idea ever. Specs are all about reasoning. You need to do the thinking to model the system in a very simplified manner. Formal methods and the generative BS are at the antipodes of reliability. This is an insult to reason. Please keep this nonsense away from the serious parts of CS.

Anyone who has tried to write formal verification will tell you that there is a WIDE gap between thinking and writing the specs.

Any tool that makes formal verification more accessible, should be welcome.

I believe the valuable part is how accessible we make thinking together with machines.

Us human are great at create innovative solutions, not so great at check and verify every single thing that can go wrong. Machines help with that.

Re: GenAI-Accelerated TLA+ Challenge

#17

Post by max_ »

warkdarrior wrote: post #10
max_ wrote: post #9

Leslie Lamport said that he invented TLA+ so people could "think above the code". It was meant as a tool for people to improve their thinking and description of systems. LLM generation of TLA+ code is just intellectual masterbation. It may get the work done for your boss. But you intellect will still remain bald — in which case you are better off not writing TLA+ at all.

> [TLA+] was meant as a tool for people to improve their thinking and description of systems. Why the speciesism? Why couldn't LLMs use TLA+ by translating a natural-language request into a TLA+ model and then checking it in TLA+?

TLA+ was invented in the first place because we Leslie Lamport thought natural language was a dubious tool for "specifying systems".

Yes an LLM may generate the TLA+ code even correctly, but model checking is not the end goal of TLA+

TLA+ plus is written to fully under how a system works at an abstract level.

Anyways, I guess you could just read the LLM generated TLA+ code. That would help you understand the abstraction of the system — but is the LLMs abstraction equal to your abstraction.

But vibe coded TLA+ sounds extremely dangerous especially in mission critical stuff where its required like Smart Contracts, Pacemakers, Aircraft software etc

Post reply on HN