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
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()
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.
August TLA⁺ dev update: GenAI challenge winners announced, a startup paying people to write TLA⁺ spec examples, and efforts to make the tools less file-dependent!
https://foundation.tlapl.us/blog/2025-08-dev-update/index.html
This is the TLA⁺ Foundation monthly development update (subscribe via RSS). Here we summarize the past month of development for the benefit of Foundation patrons and interested members of the community. We will also highlight a good bug or small feature for prospective new contributors to look at! If your TLA⁺ contribution was missed, worry not - we publish monthly, so it’s easy to hop on the next train; open an issue here.
New SPAA paper is out, and it was named one of the four Distinguished Papers! We formally verified the correctness of an adaptive snapshot algorithm with far future-dependent linearization points. The TLAPS proof spans over 15k lines and took several months to complete. It's available on my GitHub for the curious.
Murat Demirbas (Distributolog)
FGM
Andrew Helwer
Alexander Diemand 💚
Samuel Chase
Uğur Y. Yavuz
jnpn