Intro to TLA+ for the LLM Era: Prompt Your Way to Victory
emptysqua.re
emptysqua.re
If you want to 'prompt your way' with TLA+, this is a decent one for ChatGPT. But don't expect to do wonders and find a better abstraction than you and if you run it 'agentically' with TLC in the loop, it will bloat the spec in no time:
Write the smallest TLA+ model that captures only the safety-relevant state of [the thing you're modeling]. Do not model implementation data structures unless they affect the property. Use clear names, not abbreviations. Start with: constants, variables, TypeOK, Init, and 2–4 invariants. Use copious amounts of comments at the module level (use multi-line comments) and for each key variable, action, invariant, and temporal property (use one or more single-line comments). Prefer fewer variables and coarser atomic steps unless finer interleavings are essential. Keep the spec under 100 LoC (excluding comments) unless there is a specific reason not to. After writing it, list what was intentionally abstracted away.
"Running leading LLMs across the eleven systems shows that LLMs are great at producing correct TLA+ syntax but struggle to ensure conformance and appropriate invariants."
> It’s still your responsibility to understand your system and define what “correctness” means, and you need a high-level understanding of temporal logic.
Using a TLC model checker to verify invariants or properties, finding a valid counterexample can scale non-elementarily.
In fact, in some situations it can end up being Ackermann-complete[0], but even recursively enumerable problems can be Tower-complete.
I would say that unless you focus on more detailed temporal logic pitfalls you may have issues.
So IMHO this will stay a use case specific solution, that you choose based on context.
Even a common solution like adding Circumscription causes counterintuitive changes [1][2].
IMHO, if you want to use TLA+ as a primary method, you will need some depth or be ready to abandon it by time boxing etc…
Remember that we know the open domain frame problem in [2] is equal to HALT, it will not universally apply.
It is just another tool that works well when it works well.
[0] https://arxiv.org/abs/2104.13866
Ran it on my tricky caching changes and it found bugs the standard agentic review flows missed on all frontier models. Good stuff.
There's always a moment, usually annoyingly late in the process, where I realize I've been massively overthinking everything or solving the wrong problem. Time is an essential an ingredient. Clear thinking is extremely hard.
LLMs are definitely useful along the way, but the thinking is the spiritually fulfilling part.
(One of the entries cited is something I worked on).
I wrote about this a bit on my blog[1], different angle but along the same line. You explain TLA+ and model checking well which makes the case concrete.
I'm curious of you have thoughts on these other methods and tools like P, Lean, Dafny, etc?
They have a development pace very quick and can verify real world Rust code. There's a huge graveyard of Rust verification tools, but I hope this one gets broader usage
You can also work backwards from the races it generates and ensure that they're real races.
"look at @design-document and generate a TLA+ specification for the interactions between local and remote"
I understand that this is not the tool for everything but scxml, state chart XML, gives you something like this but something that you can actually read without investing time learning syntax.
It also has some plugins on vs code that allow you to edit it visually in case you don't want to write a bazillion XML tags.
Well, the article disagrees, but the answer is obviously yes: if you have two beans left, regardless of whether they match, the first step is to discard them. Then you have zero beans. After that, you then add 1 additional bean.
So already we can see that the problem is underspecified: are we considering the entire action to be a single atomic "transaction" (in which case it never hits zero), or are these individual steps?
But also, I feel like if you needed TLA+ to answer that question, you're probably not capable of evaluating the TLA+ script? In particular, the TLA+ script doesn't address the "underspecified" aspect at all.
It could be the case that Tony Hoare was right, just too early.
BB == b > 1 /\ b' = b - 2 /\ w' = w + 1 \* Picked 2 black
EDIT: Actually, the original spec doesn't even say what is a valid state after initialization. It provides only a requirement on the initial state (that w + b > 0 and that w and b are both in Nat, or >= 0, when initialized). The correctly formulated rules ensure that w and b remain in Nat, but there's no other piece of the specification that seems to require it.
Once the author starts adding invariants (like NotEmpty) that adds a requirement that w + b > 0 remains true for ever, but since w is incremented and b is decremented, even BB results in NotEmpty remaining satisfied. Each of the steps does, since they all add one bean back.
> If the algorithm terminates with b = 1, what must have been true at the start?
For anyone that wasn't clear, "b" isn't the number of beans in general, it's specifically the the number of black beans. Introducing a variable before defining what it is can be a bit confusing, hope this comment helps others.