GenAI-Accelerated TLA+ Challenge
foundation.tlapl.us
GenAI-Accelerated TLA+ Challenge
1–10 of 17 posts
Re: GenAI-Accelerated TLA+ Challenge
#2Using 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 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.
Re: GenAI-Accelerated TLA+ Challenge
#3Using 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…
A fascinating thought. But then who verifies that the TLA+ specification does indeed match the human specification?
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+?
Re: GenAI-Accelerated TLA+ Challenge
#4Using 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…
A fascinating thought. But then who verifies that the TLA+ specification does indeed match the human specification? 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+?
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..
Re: GenAI-Accelerated TLA+ Challenge
#5Earlier quoted context omitted.
A fascinating thought. But then who verifies that the TLA+ specification does indeed match the human specification? 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+?
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?)
Re: GenAI-Accelerated TLA+ Challenge
#6Earlier 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?)
No idea about SOTA but naively it doesn't seem like a very difficult problem:
- 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.
Re: GenAI-Accelerated TLA+ Challenge
#7Using 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…
A fascinating thought. But then who verifies that the TLA+ specification does indeed match the human specification? 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+?
A fair question! I'd say it's not that different from using an LLM to write regular code: who verifies that the code the LLM wrote is indeed what you meant?
Re: GenAI-Accelerated TLA+ Challenge
#8Using 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…
A fascinating thought. But then who verifies that the TLA+ specification does indeed match the human specification? 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+?
The usual way to check whether a definition is correct is to prove properties about it that you think should hold. TLA+ has good support for this, both with model checking as well as simple proofs.
Re: GenAI-Accelerated TLA+ Challenge
#9Leslie 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.
Re: GenAI-Accelerated TLA+ Challenge
#10Leslie 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+?