Feedback on TLA+ tutorial and proofs

[Jskri]

Hello,

Some time ago, I wrote a (long) tutorial on TLA+ intended for engineers.

It is very proof-oriented, using a “correct by construction” approach, as presented by J-R. Abrial, the author of Event-B. The idea is to start with a very abstract model and refine it as many times as necessary until you arrive at a version that can be easily translated into code. For each model, the invariants (safety) and refinement are proven.

The tutorial therefore covers these different concepts, but also how to break down a model into sub-models, and finally how to verify that the implementation (the code) complies with the model.

The approach is illustrated by several examples and finishes by a client-server system, implemented in C++20 / ZeroMQ.

There is nothing new in this work, but I have tried to present what I have learned here and there in a way that I hope is coherent. I also feel that there are not many introductions to proof with TLA+.

The PDF is here: https://github.com/jskri/modeling-with-tla/releases/download/v0.1/modeling-with-tla-v0.1.pdf

(the TLA+ specifications and C++ sources are in the repository)

I am interested in any constructive feedback.

Thanks!

[Irwansyah Irwansyah]

Hello,

May I know your name?

I am reading your PDF, now in chapter 2. I can only say so far your writing is the most friendly TLA+ tutorials out there also it includes all the tutorials I found in a friendly and easy to read manner. I will give more feedback after I finish reading it, so far my feedback is on the font that you use. The font used is mostly found in very serious and dull textbooks but yours is very friendly and easy to read so it must use a different font :)

Irwan

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/646a785a-88eb-46b5-a691-ff9992c3ace1n%40googlegroups.com.

[dbah...@gmail.com]

The “All model sources can be found here.”

Link does not appear to work?!

 

Is this the correct place to send minor edits?

 

Thanks

Dave

--

[dvnh87]

It looks like my previous reply was deleted? Here it is again:

Thank you, the links should be fixed now:

https://github.com/jskri/modeling-with-tla/releases/download/v0.2/modeling-with-tla-v0.2.pdf

For edits, can you make a pull request?

You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/TXK5vZ762vI/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/014501dc2c82%2469f33770%243dd9a650%24%40gmail.com.

[Andrew Helwer]

Apologies for the deletion, google groups has been acting up and deleting random replies for years now. I usually deal with it by sending replies through email, not the google groups web interface. That way if the message gets deleted I can find it in my sent folder and re-send it.

Andrew Helwer

To view this discussion visit https://groups.google.com/d/msgid/tlaplus/UVEyCLHyWXVXB0klrNd6OfNH3DLwlCqCYloYKHYQ09a1FpTecKui8zXF6BUX0Vhfu3j0WXhy2ZZFoihvNY9DXjK3Porl_NqD4NWKStR9evg%3D%40protonmail.com.

[dvnh87]

OK, I'll do that, thank you.

To view this discussion visit https://groups.google.com/d/msgid/tlaplus/CABj%3DxUXhQuKB_KwZYapadnywpgFXPL2vYjCN7d73i9C%3DW9ge5g%40mail.gmail.com.

[Andrew Helwer]

I am reading the tutorial now. Thank you for writing it! I like the focus on refinement from the start, which is usually considered a more advanced feature of TLA+ but I agree should take a more central place. Although all the refinement tutorials I've read go from abstract to concrete; I always seem to end up going the opposite direction! I write the concrete spec and then later write the abstract spec as a sort of super-powered whole-system safety property. Hillel Wayne thinks maybe this is why I find success with it. Although I should actually try the abstract-to-concrete direction for the next system I specify. It's too easy to start cranking away on message formats and actions and multiple nodes and so forth.

I like that you use unicode symbols for TLA+. These are actually now standardized and supported by SANY and TLC! But not TLAPS, yet. You can see the standardized codepoints here. A tool to convert back and forth between Unicode and ASCII symbols (while maintaining conjunction & disjunction list alignment) can be found here.

Would you like this tutorial to be mentioned in the October development update newsletter?

Andrew Helwer

P.S. Thanks to Irwan for emphasizing the importance of engaging with new tutorials posted by members of the community.

To view this discussion visit https://groups.google.com/d/msgid/tlaplus/YyvNcAnvY8LErgLHdoe4R82CTn3SZQJjBgvGJ_4E8MdjK_M61tU-RkmdyMZZ8Jvay7K-D06So3iXadRSSURyIKv1lS3wN66rugP0VY1-_RM%3D%40protonmail.com.

[Andrew Helwer]

I finished reading the tutorial. Mostly I focused on the proof and trace validation chapters, as I've not yet found a good application for spec composition; I recall my main takeaway from Hillel Wayne's post about the topic is that TLA+ has some shortfalls in that domain since the composed specs must have disjoint variable sets.

These tutorials are truly excellent! I do not think it's an exaggeration to say they are currently the best tutorials out there for both the proof system and trace validation. You also clearly explained the difference between ordinary invariants and inductive invariants, which was useful for my understanding. For the proof system I would be very interested in seeing extended material on how to prove eventually or leads-to statements. In Lamport's new book A Science of Concurrent Programs he spends a lot of time on proof rules & techniques for these properties, which all seem to involve lots of non-constructive reasoning and using false premises to get proofs by contradiction. I would be interested to see how TLAPS handles this.

The trace validation chapter was also very good. One topic I would like to see covered: in Srinidhi Nagendra's ModelFuzz talk at this year's TLA+ conference, he spoke about how sometimes when combining distributed events into a linear log you run into the NP-complete linearizability checking problem. Discussion about in what circumstances this issue arises would be very useful!

So basically my only substantial feedback is I would like to see more tutorials from you! Thank you.

Andrew Helwer

[dvnh87]

Thank you for your feedback.

I think that the direction—from abstract to concrete or vice versa—doesn't matter as long as the two are connected in the end.

Regarding Unicode, in the tutorial, the TLA+ code actually only uses ASCII (you can see this by pasting the code into a text editor). It is only the font used that performs special rendering via ligatures.

You are welcome to mention this tutorial wherever you like. Here is the latest version, with licenses added: https://github.com/jskri/modeling-with-tla/releases/download/v0.3/modeling-with-tla-v0.3.pdf

Regarding the composition of specifications, the tutorial's approach is to share variables for communication and use interleaving composition. This approach seems quite natural to me because it has little impact on the way components are written.

Thanks for the links, I need to study all this!

To view this discussion visit https://groups.google.com/d/msgid/tlaplus/CABj%3DxUX1M2BPs_kq1ESkgfX-aqfM7jZPxdy-9%3DEG7cukDcf_9Q%40mail.gmail.com.

[Stephan Merz]

Thank you indeed for the tutorial: I find it very nicely presented, with helpful illustrations, and a useful complement to existing material.

Here are a few comments and suggestions (I haven’t checked your updated version):

- Throughout, almost all links are broken.

- p.3 bottom: "where hour is in 0 .. 12" – clearly, this should be either 0 .. 11 or 1 .. 12, and you opt for the latter in the formal spec.

- p.4: The current version of the VS Code extension lives at [1], and it does support the prover. At the moment, the "decompose proof" command is not yet there, but it should be available before the end of the year.

- following paragraph: I find it a little unfortunate that you deviate from the usual TLA+ terminology of "specification" for a generic description of a system at a given level of abstraction and "model" for a concrete instance of a specification used for model checking. This might confuse newcomers.

- p.12, def. UserSetsAlarm: Note that this action allows a transition from unset to ringing, which is not represented in the system diagram.

- p.13 top: "random" may suggest probabilities, which are not covered by TLA+, so I’d avoid that word.

- p.13 middle: UNCHANGED <<now, ringing>> is not actually a "shortcut" (in the sense of a macro) for UNCHANGED now /\ UNCHANGED ringing, but the two formulas are logically equivalent.

- p.29: For the refinement proof, perhaps you could have adapted the example a little so that the type correctness invariant was actually required for proving refinement, and take the opportunity to show how a previously proved property can be used in a later proof. This is indeed required for most refinement proofs in practice. You show how to use a previously proved invariant in section 2.2.6, but personally, I think the technique could be explained for invariants first, and then applied in the refinement proof, which could help readers get the idea.

- p. 37 top: Here you enforce a strict alternation between the two components, and I wonder why you did this, as it may make later refinements harder. Indeed, later you rather stick to disjunctive ("interleaving") representations: I would have introduced this first and perhaps mentioned later that you can enforce strict alternation if required.

- p. 37 middle: "The above disjunctive Next" – this should certainly be "conjunctive"

- p.41, module ThemeCommon1: I do not really understand why you make IsNewestOfItsTheme a parameter rather than a definition?

- p. 42 top: You say that the alternative to constants are definitions, but constants such as Theme and Pack are naturally parameters, it is not clear to me what their definitions would be. Concerning the choice between accessor functions such as PackTheme or PackVersion and an explicit record representation, I think the main advantage of the former is greater (or more obvious) abstraction. It becomes clearer that the spec just describes the part of the real world that is relevant to the current level of abstraction, without pretending to be a full representation of the actual system state.

- p.42, Fig.16: Here "newPack" is both an input and an output to the system, whereas at the beginning of the chapter you said that the two sets had to be disjoint.

- p.50: In the initial condition, I would have expected knownIds to be initialized to { PackId[InitialPack] }, although it does not make a real difference for the behavior. In DeviceSendsListRequest, I find the guard "packs # Pack" quite strange since "unnecessary" list requests may be sent at other times (in the sense that the device will not learn of new packs). Also, realistically the set Pack could be open-ended, without the device really having access to this set, and indeed later you say that you will not implement this condition, so I’d just suggest to remove it.

- Sect. 4.1, par.2: One way of avoiding this way of reconstructing / completing model states is to log *updates* to the model state rather than the model state itself. This is what we do in our approach to trace validation [2], and we also allow the set of logged variables to be incomplete, relying on TLC to find suitable values in order to complete the trace. (Obviously, there is a tradeoff between convenience and completeness of logging and precision of the verdict.)

- Sect. 5, par. 4: I also find it useful that the different tools are based on the same language (or, more precisely, on subsets of the same language). For example, one can extensively run the model checker before starting a proof, and also go back to model checking when the proof suggests a strengthening of an invariant, in order to make sure that the asserted theorem has a chance of being true. I also find it useful to use Apalache (which you do not cover here) to check if an invariant is indeed inductive.

Thanks again for the nice text and best regards,
Stephan

[1] https://marketplace.visualstudio.com/items?itemName=tlaplus.vscode-ide
[2] https://link.springer.com/chapter/10.1007/978-3-031-77382-2_8

[dvnh87]

Thank you for your thorough review. I agree with most of your comments.

The links have been fixed in the v0.2.

Regarding strict alternation (p. 37), IIRC the logic of the text is to follow intuition and first use a conjunctive Next to represent parallel composition ("simultaneity"). Then, relax the constraints and use a strict alternate disjunction instead (since a mapping to the conjunctive spec exists), and finally relax to obtain an interleaving composition, which is acceptable in many cases. This shows that a disjunctive Next allows all the forms of composition that we consider here.

Concerning IsNewestOfItsTheme as a parameter rather than a definition (p.41, module ThemeCommon1), the aim is to avoid ending up with distinct definitions in different instantiations, which would require a bit more work with the prover.

For now, I haven't made any structural changes, but I have made many targeted corrections and additions.

You can see the diffs here and here.

The corresponding PDF is: https://github.com/jskri/modeling-with-tla/releases/download/v0.4/modeling-with-tla-v0.4.pdf

Thank you again.

On Tuesday, September 30th, 2025 at 15:52, Stephan Merz stepha...@gmail.com wrote:

Thank you indeed for the tutorial: I find it very nicely presented, with helpful illustrations, and a useful complement to existing material.

Here are a few comments and suggestions (I haven’t checked your updated version):

- Throughout, almost all links are broken.

- p.3 bottom: "where hour is in 0 .. 12" – clearly, this should be either 0 .. 11 or 1 .. 12, and you opt for the latter in the formal spec.

- p.4: The current version of the VS Code extension lives at [1], and it does support the prover. At the moment, the "decompose proof" command is not yet there, but it should be available before the end of the year.

- following paragraph: I find it a little unfortunate that you deviate from the usual TLA+ terminology of "specification" for a generic description of a system at a given level of abstraction and "model" for a concrete instance of a specification used for model checking. This might confuse newcomers.

- p.12, def. UserSetsAlarm: Note that this action allows a transition from unset to ringing, which is not represented in the system diagram.

- p.13 top: "random" may suggest probabilities, which are not covered by TLA+, so I’d avoid that word.

- p.13 middle: UNCHANGED <<now, ringing>> is not actually a "shortcut" (in the sense of a macro) for UNCHANGED now /\ UNCHANGED ringing, but the two formulas are logically equivalent.

- p.29: For the refinement proof, perhaps you could have adapted the example a little so that the type correctness invariant was actually required for proving refinement, and take the opportunity to show how a previously proved property can be used in a later proof. This is indeed required for most refinement proofs in practice. You show how to use a previously proved invariant in section 2.2.6, but personally, I think the technique could be explained for invariants first, and then applied in the refinement proof, which could help readers get the idea.

- p. 37 top: Here you enforce a strict alternation between the two components, and I wonder why you did this, as it may make later refinements harder. Indeed, later you rather stick to disjunctive ("interleaving") representations: I would have introduced this first and perhaps mentioned later that you can enforce strict alternation if required.

- p. 37 middle: "The above disjunctive Next" – this should certainly be "conjunctive"

- p.41, module ThemeCommon1: I do not really understand why you make IsNewestOfItsTheme a parameter rather than a definition?

- p. 42 top: You say that the alternative to constants are definitions, but constants such as Theme and Pack are naturally parameters, it is not clear to me what their definitions would be. Concerning the choice between accessor functions such as PackTheme or PackVersion and an explicit record representation, I think the main advantage of the former is greater (or more obvious) abstraction. It becomes clearer that the spec just describes the part of the real world that is relevant to the current level of abstraction, without pretending to be a full representation of the actual system state.

- p.42, Fig.16: Here "newPack" is both an input and an output to the system, whereas at the beginning of the chapter you said that the two sets had to be disjoint.

- p.50: In the initial condition, I would have expected knownIds to be initialized to { PackId[InitialPack] }, although it does not make a real difference for the behavior. In DeviceSendsListRequest, I find the guard "packs # Pack" quite strange since "unnecessary" list requests may be sent at other times (in the sense that the device will not learn of new packs). Also, realistically the set Pack could be open-ended, without the device really having access to this set, and indeed later you say that you will not implement this condition, so I’d just suggest to remove it.

- Sect. 4.1, par.2: One way of avoiding this way of reconstructing / completing model states is to log updates to the model state rather than the model state itself. This is what we do in our approach to trace validation [2], and we also allow the set of logged variables to be incomplete, relying on TLC to find suitable values in order to complete the trace. (Obviously, there is a tradeoff between convenience and completeness of logging and precision of the verdict.)

- Sect. 5, par. 4: I also find it useful that the different tools are based on the same language (or, more precisely, on subsets of the same language). For example, one can extensively run the model checker before starting a proof, and also go back to model checking when the proof suggests a strengthening of an invariant, in order to make sure that the asserted theorem has a chance of being true. I also find it useful to use Apalache (which you do not cover here) to check if an invariant is indeed inductive.

Thanks again for the nice text and best regards,
Stephan

[1] https://marketplace.visualstudio.com/items?itemName=tlaplus.vscode-ide
[2] https://link.springer.com/chapter/10.1007/978-3-031-77382-2_8

On 23 Sep 2025, at 12:30, 'Jskri' via tlaplus tla...@googlegroups.com wrote:

Hello,
Some time ago, I wrote a (long) tutorial on TLA+ intended for engineers.
It is very proof-oriented, using a “correct by construction” approach, as presented by J-R. Abrial, the author of Event-B. The idea is to start with a very abstract model and refine it as many times as necessary until you arrive at a version that can be easily translated into code. For each model, the invariants (safety) and refinement are proven.
The tutorial therefore covers these different concepts, but also how to break down a model into sub-models, and finally how to verify that the implementation (the code) complies with the model.
The approach is illustrated by several examples and finishes by a client-server system, implemented in C++20 / ZeroMQ.
There is nothing new in this work, but I have tried to present what I have learned here and there in a way that I hope is coherent. I also feel that there are not many introductions to proof with TLA+.
The PDF is here: https://github.com/jskri/modeling-with-tla/releases/download/v0.1/modeling-with-tla-v0.1.pdf
(the TLA+ specifications and C++ sources are in the repository)
I am interested in any constructive feedback.
Thanks!

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/646a785a-88eb-46b5-a691-ff9992c3ace1n%40googlegroups.com.

--
You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/TXK5vZ762vI/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/270296D6-3560-4FDC-981F-7DD096F496B8%40gmail.com.