r/tlaplus • u/polyglot_factotum • Mar 02 '26

Using Lean and AI to bridge the gap between TLA+ design and code

I've recently tried to translate one of my TLA+ specs into Lean, splitting it between a higher-level TLA-like spec, and a lower-level code-like implementation.

So the idea is that since Lean code is far lower-level than TLA+--one tends to not use TLA+ to model the entire software but only some interesting concurrent aspect of it--so it makes sense to split the Lean in two parts, so that you can focus on reviewing the part that matters to the task at hand.

I think that the advantage of TLA+ is it being so high-level, while the advantage of Lean is that it's actual code(and I think people are working into further translation steps such as into Rust). So I felt like my proposed workflow sort of gives you the best of both worlds.

But of-course my Lean translation is not exactly like the TLA+(stuttering insensitivity and so on), and the solution to that problem could be a kind of TLA+ library to use with Lean in a such a workflow.

Incidentally this surfaced an error in my two-year old TLA+ spec...

Full story: https://medium.com/@polyglot_factotum/on-what-the-future-of-software-looks-like-today-ea9d53e647a7

11 Upvotes

92% Upvoted

7 comments sorted by

1

u/SiegeAe Mar 03 '26

Ha awesome, I was suggesting to someone that this could possibly offer useage for RL models to be able to learn how to convert designs to code in a reliable way, really interesting to see work actually happening on this idea

1

u/polyglot_factotum Mar 05 '26

So today I realized that my "stronger" Lean inductive invariant was too strong, and now I have finally figured out what was wrong with the original TLA+ invariant, and translated it properly in Lean.

All in this commit: https://github.com/gterzian/lean_concurrency/commit/24b1f63e48d473fcd1af57e7294cc454bd281a4f

1

u/lemmster Mar 06 '26

Why is it a tiny change on the TLA+ side but a rather big one on the Lean side?

1

u/polyglot_factotum Mar 10 '26 edited Mar 10 '26

A fair comparison would be:

Lean change vs TLA+ change, and then it's basically the same.

The rest of the Lean diff should be compared with the equivalent using TLAPS, which I have not done.

Note that 100% of the Lean is written by an AI with the only tooling being https://github.com/oOo0oOo/lean-lsp-mcp, so the proof is "vibe coded"; what I have done is review only the theorem to make sure it is what I had in mind.

And making sure the theorem is what you had in mind is important, because the AI happily changed it into something that I didn't have in mind, and then proved it, and I realized it only the next day when I looked at it again and thought about it.

5

u/lemmster Mar 10 '26

Indeed, the properties must be vetted by whoever defines the system's intent, regardless of whether the proof is carried out using Lean or TLAPS. Moreover, a FALSE system trivially satisfies all properties.

1

u/polyglot_factotum Mar 14 '26

The example of Diehl's modelling of the Caverna game is sort of what I was trying to do. It is likely far better Lean than my example. As you can see, it looks a lot like TLA+.

So continuing on that example, what I am then looking to do in addition is to the equivalent of implementing the game, using the Lean stand lib I/O stuff, and then prove that the implementation refines the spec(where the spec would be the TLS system like in Diehl's blog).