Eric Spencer
projects
This repository is the first pass at generating TLA+ from English with an LLM, inside the ai4fm research thread at Loyola. It is small and scrappy, and it is a scaffold. The point was to get an end-to-end loop running (English requirement, then a generated .tla module, then TLC actually checking it) before worrying about whether the generations were any good. The later ChatTLA+ dataset and paper extends the idea.
The shape of it: a tiny benchmark of three NL-to-invariant examples (semaphore non-negativity, boolean domain, upper-bound counter), a template .tla file with {{module}}, {{vars}} and {{invariant}} holes, a Python generator that fills those holes either with a real LLM call or a deterministic stub, and an evaluator that runs the resulting module through TLC and reports whether the invariant held, was violated, or the toolchain blew up. Plus a shell script that downloads tla2tools.jar, so TLC runs locally without an afternoon of fighting with Java.
The generator is explicit about its limits. If OPENAI_API_KEY is set, it calls GPT-4 with a one-shot prompt ("Translate this English requirement into a TLA+ invariant expression only") and uses whatever comes back. If the key is not set, it falls back to stub_generate, which returns the ground-truth invariant from the benchmark row. The stub is not cheating; it lets the rest of the pipeline (template rendering, TLC invocation, evaluation) be tested deterministically without an API call. It also makes the evaluation results mean very little while it is on, which is most of the time.
def stub_generate(item):
if 'expected_invariant' in item:
return item['expected_invariant']
nl = item.get('nl', '').lower()
if 'semaphore' in nl or 'counter' in nl:
if 'below 0' in nl or 'non-neg' in nl:
return 'counter >= 0'
...
The evaluation is similarly naive: string equality between the generated invariant and the expected one, plus a check for Invariant Inv is violated or No error has been found in TLC's output. That works for three examples. It does not scale to anything worth claiming, and that was clear going in. The goal was only to establish that generating a .tla file, running TLC on it and parsing the verdict was a tractable feedback loop, because the whole RL-on-spec-generation idea depended on it.
It was tractable. A few months later the work was rebuilt properly: a 209-row SFT corpus filtered by TLC-verified outputs, a 30-problem held-out benchmark across six domains, semantic reward shaping (state coverage, action coverage, mutation-kill rate), and the GRPO/SFT pipeline that became ChatTLA+. That work was accepted to and presented at ICSOFT 2026; the dataset repo is up.
Two decisions in the older repository held up. Separating template rendering from the LLM call from TLC invocation and output parsing means any one of the three can be swapped without touching the other two. Using tla2tools.jar means the evaluator reads TLC's actual verdicts. Two did not hold up. A three-row benchmark with hand-written ground-truth invariants encourages testing on the same problems a lookup would solve, and the deterministic stub exploits exactly that. Matching invariant strings instead of checking semantic equivalence under TLC rejects counter >= 0 against counter \in Nat, which are the same property. The ChatTLA+ work fixed both by validating against TLC directly and scoring by behavioral metrics rather than string match.
The pipeline is at EricSpencer00/tla-formal-generation. The generate -> template -> TLC -> parse structure is a reasonable starting point for similar work, but the benchmark and the evaluation both need to be far heavier before anything real can be said with it.