GenAI-Accelerated TLA+ Challenge

Using LLMs for formal specs &#x2F; 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+ &#x2F; Dafny &#x2F; etc, then it can hook into a very mature ecosystem of automated proof tools.<p>I&#x27;m picturing it something like this:<p>1. Human developer says, &quot;if a user isn&#x27;t authenticated, they shouldn&#x27;t be able to place an order.&quot;<p>2. LLM takes this, and its knowledge of the codebase, and turns it into a formal spec -- like, &quot;there is no code path where User.is_authenticated is false and Orders.place() is called.&quot;<p>3. Existing code analysis tools can confirm or find a counterexample.

Leslie Lamport said that he invented TLA+ so people could &quot;think above the code&quot;.<p>It was meant as a tool for people to improve their thinking and description of systems.<p>LLM generation of TLA+ code is just intellectual masterbation.<p>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.

Interesting. I&#x27;ve always wanted to formalize the US Constitution into TLA+ in order to find loopholes.

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.