Re: [tlaplus] Feedback on TLA+ tutorial and proofs

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

On Sat, Sep 27, 2025 at 8:43 PM Andrew Helwer <andrew.helwer@xxxxxxxxx> wrote:

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.

On Fri, Sep 26, 2025 at 9:15 PM 'dvnh87' via tlaplus <tlaplus@xxxxxxxxxxxxxxxx> wrote:
OK, I'll do that, thank you.
On Wednesday, September 24th, 2025 at 13:52, Andrew Helwer <andrew.helwer@xxxxxxxxx> wrote:

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

On Wed, Sep 24, 2025 at 6:45 PM 'dvnh87' via tlaplus <tlaplus@xxxxxxxxxxxxxxxx> wrote:
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?

On Tuesday, September 23rd, 2025 at 14:06, dbahughes@xxxxxxxxx <dbahughes@xxxxxxxxx> wrote:

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
From: 'Jskri' via tlaplus <tlaplus@xxxxxxxxxxxxxxxx>
Sent: 23 September 2025 12:31
To: tlaplus <tlaplus@xxxxxxxxxxxxxxxx>
Subject: [tlaplus] Feedback on TLA+ tutorial and proofs

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+unsubscribe@xxxxxxxxxxxxxxxx.
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/014501dc2c82%2469f33770%243dd9a650%24%40gmail.com.

--
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/UVEyCLHyWXVXB0klrNd6OfNH3DLwlCqCYloYKHYQ09a1FpTecKui8zXF6BUX0Vhfu3j0WXhy2ZZFoihvNY9DXjK3Porl_NqD4NWKStR9evg%3D%40protonmail.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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/CABj%3DxUXhQuKB_KwZYapadnywpgFXPL2vYjCN7d73i9C%3DW9ge5g%40mail.gmail.com.

--
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/YyvNcAnvY8LErgLHdoe4R82CTn3SZQJjBgvGJ_4E8MdjK_M61tU-RkmdyMZZ8Jvay7K-D06So3iXadRSSURyIKv1lS3wN66rugP0VY1-_RM%3D%40protonmail.com.