[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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



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

On Tue, Sep 23, 2025 at 5:40 PM 'Jskri' via tlaplus <tlaplus@xxxxxxxxxxxxxxxx> 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+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 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/CA%2BKOs4wk5_9cqNN79tMLmEExxJ-E9O0i7_aRZfZdE7bxB2Hr0g%40mail.gmail.com.