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!
--