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.
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+?
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.
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
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.
Taikonerd•5mo ago
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 the codebase, and turns it into a formal spec -- like, "there is no code path where User.is_authenticated is false and Orders.place() is called."
3. Existing code analysis tools can confirm or find a counterexample.
omneity•5mo ago
I’m guessing using an LLM as a translator narrows the gap, and better LLMs will make it narrower eventually, but is there a way to quantify this? For example how would it compare to a human translating the spec into TLA+?
justanotheratom•5mo ago
svieira•5mo ago
omneity•5mo ago
- Ensure all TLA+ specs produced have the same inputs/outputs (domains, mostly a prompting problem and can solved with retries)
- That all TLA+ produce the same outputs for the same inputs (making them functionally equivalent in practice, might be computationally intensive)
Of course that assumes your input domains are countable but it's probably okay to sample from large ranges for a certain "level" of equivalence.
EDIT: Not sure how that will work with non-determinism though.
justanotheratom•5mo ago
Taikonerd•5mo ago
fmap•5mo ago
frogmeister57•5mo ago