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
@norootcause #TLAplus to the rescue! They have been applying formal methods before.
And yes, the [afks] DNS system is a pillar of the backbone of our Internet, economy, society. Who would have thought almost 50y ago?
@tealeg
My suggestions would be #rakulang, #tlaplus, (multicore) #ocaml, C, modern C++, #commonlisp
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
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.
Published the July 2025 TLA+ development update. GenAI challenge submission deadline passed, TLAPM updated to use Isabelle 2025, TLA+ proofs fixed, critical chapter published on guide to writing your own TLA+ modelchecker!
Lately I've been mulling what exactly will keep TLA+ from going the way of UML in terms of relevance; turns out Hillel Wayne already wrote a pretty good post about that!
https://buttondown.com/hillelwayne/archive/can-formal-methods-succeed-where-uml-failed/
I wrote a blog post about a type of TLA+ contract I've done a few times, why it never goes as well as hoped, and how future contracts could be restructured for greater success.
June TLA⁺ development update: AI contest submission deadline is July 4th, Spectacle gets GraphViz animation support, VS Code extension gets MCP support, and a new research grant for synthesizing inductive invariants!
Conformance Checking at MongoDB: Testing That Our Code Matches Our TLA+ Specs
#HackerNews #ConformanceChecking #MongoDB #TLAplus #Testing #Code #Engineering
I was on Func Prog Podcast talking about formal methods, model checking, TLA+ and Quint! Here are the links in case you want to check it out:
YouTube: https://youtu.be/zKERmkonANM?si=--G5E0HSjyOKvgFQ
Spotify: https://open.spotify.com/episode/4yaIyGbRcG5dBSGSaD3gCa?si=i2m-c89jQ8ON25HmIUjhSw
RSS: https://anchor.fm/s/10395bc40/podcast/rss
Hillel Wayne had some ideas to make TLA+ syntax more familiar to software engineers (basically less LaTeX-y, like "all" instead of "\A"), so I branched the Java-based parser and whipped up some changes to see what this would look like in practice. It was very low effort but also totally works. Taking additional requests!
Spamming TLA⁺ stuff today because I wanted to get that last post out before the publication date of this post: the May monthly development update! TLA⁺ Community Event talk recordings posted, a contest with a NVIDIA RTX 5090 as the grand prize, GraalVM native image builds, and a big focus on improving usability this month.
https://foundation.tlapl.us/blog/2025-05-dev-update/index.html
Oh, look! Another riveting blog post about TLA⁺ development, because clearly the world was desperate for more updates on formal specification languages from 2025. 🎉🤖 Congratulations, Andrew, for making sure our excitement levels match those of a toaster's firmware update. 🍞🔧
https://ahelwer.ca/post/2025-05-15-tla-dev-status/ #TLAplus #TLAplusDevelopment #FormalSpecification #Humor #TechUpdates #HackerNews #ngated
The current state of TLA⁺ development
https://ahelwer.ca/post/2025-05-15-tla-dev-status/
#HackerNews #TLA+ #TLAplus #development #software #engineering #formal #methods #programming
I wrote a blog post version of my talk at the 2025 TLA⁺ Community Event last week. I try to capture the current state of TLA⁺ tooling development: what tools exist, our greatest challenges, and what I want in the near-mid future.
