A High-Level View of TLA+
lamport.azurewebsites.net
A High-Level View of TLA+
1–10 of 20 posts
Re: A High-Level View of TLA+
#2I’m curious about the practical workflow after you’ve written and verified a TLA+ spec. How do you go from the TLA+ proof to actual code? Is there any established process or best practices for translating the spec into implementation while ensuring you’re not introducing bugs during that translation? And once you’ve written the code, how do you maintain the connection between spec and implementation as things evolve?
Re: A High-Level View of TLA+
#3I’m curious about the practical workflow after you’ve written and verified a TLA+ spec. How do you go from the TLA+ proof to actual code? Is there any established process or best practices for translating the spec into implementation while ensuring you’re not introducing bugs during that translation? And once you’ve written the code, how do you maintain the connection between spec and implementation as things evolve?
I've never did that before but this recent post from mongodb team has a interesting view on this.
https://www.mongodb.com/blog/post/engineering/conformance-ch...
Re: A High-Level View of TLA+
#4Asking from ignorance: Can newer languages like Lean do the job of model checkers like TLA+? There are so many formal model checkers/languages that it is difficult to know which one is the "best".
Re: A High-Level View of TLA+
#5If you are interested in TLA+, you might want to check out Quint (https://quint-lang.org), a modern take on a specification language which shares the same underlying temporal logic of actions, but with a syntax more familiar to programmers.
Re: A High-Level View of TLA+
#6I’m curious about the practical workflow after you’ve written and verified a TLA+ spec. How do you go from the TLA+ proof to actual code? Is there any established process or best practices for translating the spec into implementation while ensuring you’re not introducing bugs during that translation? And once you’ve written the code, how do you maintain the connection between spec and implementation as things evolve?
I've never did that before but this recent post from mongodb team has a interesting view on this. https://www.mongodb.com/blog/post/engineering/conformance-ch...
You can also go the other way around and generate traces [1] from the TLA+ or Quint [2] specs using the Apalache model checker [3], map each action in the trace to an action on your system under test, and check that the abstract and concrete states match at each step.
Re: A High-Level View of TLA+
#7Asking from ignorance: Can newer languages like Lean do the job of model checkers like TLA+? There are so many formal model checkers/languages that it is difficult to know which one is the "best".
Doing distributed systems work in Lean is possible, but right now is much harder than something like TLA+ or P. It's possible that a richer library of systems primitives in Lean ('mathlib for systems') could make it easier. Lean is a very useful tool, but right now isn't where I'd start for systems work (unless I was doing something specific, like trying to formalize FLP for a paper).
Re: A High-Level View of TLA+
#8I’m curious about the practical workflow after you’ve written and verified a TLA+ spec. How do you go from the TLA+ proof to actual code? Is there any established process or best practices for translating the spec into implementation while ensuring you’re not introducing bugs during that translation? And once you’ve written the code, how do you maintain the connection between spec and implementation as things evolve?
Runtime monitoring of system behavior against the spec is one way to close the gap. We wrote about our experiences with one tool for that (PObserve) here: https://cacm.acm.org/practice/systems-correctness-practices-...
Re: A High-Level View of TLA+
#9Asking from ignorance: Can newer languages like Lean do the job of model checkers like TLA+? There are so many formal model checkers/languages that it is difficult to know which one is the "best".
It should be possible to write protocol specifications in Lean, e.g., this is a recent case study on specifying two-phase commit in Lean [1] and proving its safety [2].
However, there are no model checkers for Lean. Currently, you either have to write a full proof by hand, with some assistance from LLMs, or rely on random simulation, similar to property-based testing.
[1] https://protocols-made-fun.com/lean/2025/04/25/lean-two-phas... [2] https://protocols-made-fun.com/lean/2025/05/10/lean-two-phas...
Re: A High-Level View of TLA+
#10I’m curious about the practical workflow after you’ve written and verified a TLA+ spec. How do you go from the TLA+ proof to actual code? Is there any established process or best practices for translating the spec into implementation while ensuring you’re not introducing bugs during that translation? And once you’ve written the code, how do you maintain the connection between spec and implementation as things evolve?
I’m wondering the same. I’ve read multiple articles about formal methods and how they’ve been used to find obscure bugs in distributed systems, but usually they just show a proof and talk about formal methods without concrete examples.