GenAI-Accelerated TLA+ Challenge

https://foundation.tlapl.us/challenge/index.html

35•lemmster•6mo ago

Comments

Taikonerd•6mo ago

Using 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.

omneity•6mo ago

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+?

justanotheratom•6mo ago

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..

svieira•6mo ago

Then you need to be able to formally prove the equivalence of various TLA+ programs (maybe that's a solved problem?)

omneity•6mo ago

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.

justanotheratom•6mo ago

I didn't mean generate separate TLA programs. Rather, other LLMs review and comment on whether this TLA program satisfies the user's specification.

Taikonerd•6mo ago

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?

fmap•6mo ago

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.

frogmeister57•6mo ago

It makes a lot of sense only for graphics card sales people. For everyone else with a working neuron the sole idea is utter nonsense.

max_•6mo ago

Leslie 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.

warkdarrior•6mo ago

> [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+?

jjmarr•6mo ago

Not the OP, but I would rather give a formal specification of my system to an AI and have it generate the code.

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.

max_•6mo ago

TLA+ was invented in the first place because we Leslie Lamport thought natural language was a dubious tool for "specifying systems".

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

frogmeister57•6mo ago

Using generative chatbots to write a formal spec is the most stupid idea ever. Specs are all about reasoning. You need to do the thinking to model the system in a very simplified manner. Formal methods and the generative BS are at the antipodes of reliability. This is an insult to reason. Please keep this nonsense away from the serious parts of CS.

siscia•6mo ago

Anyone who has tried to write formal verification will tell you that there is a WIDE gap between thinking and writing the specs.

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.

kelseyfrog•6mo ago

Interesting. I've always wanted to formalize the US Constitution into TLA+ in order to find loopholes.

KDE going all-in on a Wayland future

Corecore

Garfield's Proof of the Pythagorean Theorem

Pat Gelsinger: 'I've been called here for a purpose'– Lunch With the FT

UAPs as Coherent Field Entities

Planes grounded after Airbus discovers solar radiation could impact systems

Engineering.fyi

Cutting C++ Exception Time by +90%? – Khalil Estell – CppCon 2025 [video]

Plastic can be programmed to have a lifespan of days, months or years

Shopify pulls off real time 8K browser rendering on the Exosphere

The 'S&P 493' reveals a different U.S. economy

It's time for our own Space Age

Show HN: ChikkaDB – A Translation Layer to Use SQLite as a JSON Database

From Cells to Selves

The Real-Life Hunt for Red October Happened 50 Years Ago

AI Companions shape socio-emotional learning and metacognitive development

Seven years later, Airbus is still trying to kick its Microsoft habit

All the Way Down

Wacky Fun Physics Ideas

The Great Downzoning

Proposing a New Cognitive Constant (Ca) with Full Math and Open Dataset

'Good Boy' Star Indy the Dog Becomes the First Animal Nominated for a Film Award

Adventures with Chimera Linux

Show HN: New VSCode extension: Objectify Params

Popping-and-Locking-Zed-Theme

Understanding copy-on-write: why Redis needs memory overcommit

Careless Whisper: Silently Monitoring Users on Mobile Instant Messengers

An ancient foot reveals a hidden human cousin

Surely You're Joking, Mr. Feynman

Tim Cook says he uses an iMac G4 as a monitor (2024)