#Quint, a language built on top of #TLA+ to make formal specifications more accessible.

https://quint.sh/

Crazy that #LLM coding will make formal verification mainstream in the next 2 - 3 years.

#FormalVerification #TLAPlus #Testing #ModelChecking #Concurrency #Prediction

Lamport's new (and final) book A Science of Concurrent Programs is now officially published! The final draft PDF has long been available for free on Lamport's website, but now you can buy a hardcover from Cabridge press. Discussion on the TLA+ mailing list: https://discuss.tlapl.us/msg06762.html

#TLAPlus

[new blog post]

TLA+ Mental Models

https://muratbuffalo.blogspot.com/2026/03/tla-mental-models.html

#tlaplus

Cette semaine à OpenSourceExperience Paris dans la séquence "Cybersécurité & chaîne de production logicielle", je présente la validation formelle avec #tlaplus pour produire des programmes plus fiables.

Rendez-vous mercredi 10 14:25.

Deux invitations disponibles VIP dispo en MP. @osxp_paris

Spent a bit of time exercising my temporal logic/basic boolean algebra muscles today. Found a nice derivation, felt good!

https://groups.google.com/g/tlaplus/c/4hw3eUzDVA8/m/KKjzEAqOAQAJ

#TLAPlus

Learning fun things like that the TLA+ model checker call stack for evaluating a next state predicate goes:
ITool#getNextStates()
Tool#getNextStatesImpl()
Tool#getNextStatesAppl()
Tool#getNextStatesApplImpl()
Tool#getNextStatesApplImplSwitch()

#TLAPlus

Today published the penultimate chapter of my how-to guide to building your own TLA+ model-checker, in which we actually do a breadth-first search over the state space to check safety properties! Only one chapter remains but it’s more of a clean-up topic. Maybe I should just cut it. I can’t imagine many people who actually work through this tutorial who would want to implement operator parameters as closures.

https://docs.tlapl.us/creating:safety

#TLAPlus