Can LLMs model real-world systems in TLA+?
1–10 of 40 posts
Re: Can LLMs model real-world systems in TLA+?
#2This post reads like an accidental advertisement for approaches like Verus [1], which couple the implementation and verification so you can't end up with a model that diverges from the actual implementation. I'm personally much more optimistic about the verus approach, but I freely admit that's my builder bias speaking.
Re: Can LLMs model real-world systems in TLA+?
#3I remember NVIDA sponsored a TLA+ challenge last year https://foundation.tlapl.us/challenge/index.html
Re: Can LLMs model real-world systems in TLA+?
#4[dead]
Re: Can LLMs model real-world systems in TLA+?
#5I remember NVIDA sponsored a TLA+ challenge last year https://foundation.tlapl.us/challenge/index.html
Whoa didn't even know cool
Re: Can LLMs model real-world systems in TLA+?
#6>... we asked Claude to write a TLA+ specification (spec) for Etcd’s Raft implementation. It passed syntax checks, ran through the TLC model checker, and at first glance looked like a polished formal model.
This is a mistaken use of TLA+!
Leslie Lamport insists that he invented it to be a way of creating "blueprints" for systems.
- You are supposed to go from TLA+ Spec to System (codebase or hardware).
- Not codebase to TLA+ like the author has done.
Otherwise, you may simply model an existing bug properly and the pass all the checks based of its implementation.
He (Leslie Lamport) insists that the value AI can provide is in compiling TLA+ specs to a code base.
Re: Can LLMs model real-world systems in TLA+?
#7Claude has certainly been getting better with TLA+. It's not perfect yet but for laughs I got it to model the rules of Monopoly last night [1]. I haven't done any exhaustive checking on it yet, but it certainly looks passable.
It is pretty impressive at how good it's gotten at this, in a relatively short amount of time no less. I still usually write my specs by hand, but who knows how much longer I'll be doing that.
Re: Can LLMs model real-world systems in TLA+?
#8I don't use tla+ to model real-world systems anymore, Claude is able to model systems in Lean 4 and the binary executable can handle real input or I can directly generate c / rust on proofs with numeric types that have ring structure (integers, rationals, bits).
Re: Can LLMs model real-world systems in TLA+?
#9Claude has certainly been getting better with TLA+. It's not perfect yet but for laughs I got it to model the rules of Monopoly last night [1]. I haven't done any exhaustive checking on it yet, but it certainly looks passable. It is pretty impressive at how good it's gotten at this, in a relatively short amount of time no less. I still usually write my specs by hand, but who knows how much longer I'll be doing that.…
It looks quite complicated and I have no idea what it is doing. Obviously, since I don't know about TLA+. But what about someone who knows TLA+? It still seems hard to make sure it is valid. And it's just for a relatively simple game.
Re: Can LLMs model real-world systems in TLA+?
#10I don't use tla+ to model real-world systems anymore, Claude is able to model systems in Lean 4 and the binary executable can handle real input or I can directly generate c / rust on proofs with numeric types that have ring structure (integers, rationals, bits). https://github.com/lambdaclass/truth_research_zk
[flagged]