Лампорт опубликовал черновик своей новой книги с предварительным названием "A Science of Concurrent Programs". Если "Specifying Systems" больше про использование TLA+, то эта книга рассказывает про научные принципы, лежащие в основе языка TLA+ и почему TLA+ такой, какой он есть. Лампорт предупреждает, что книга содержит много математики. Вообще Лампорт классно объясняет и если например выбирать книгу про TLA+ между Specifying Systems и Practical TLA+, то мой выбор будет за первой. Из новой книги я успел прочитать только первую главу и стиль написания Лампорт не поменял.