[HN Gopher] The current state of TLA+ development
___________________________________________________________________
The current state of TLA+ development
Author : todsacerdoti
Score : 132 points
Date : 2025-05-15 18:53 UTC (1 days ago)
(HTM) web link (ahelwer.ca)
(TXT) w3m dump (ahelwer.ca)
| femto2151 wrote:
| I think the major contribution that can be made to TLA is in the
| field of divulgation. Sofware engineers don't know modern formal
| methods because for years they were pidgeonholed into safety
| critical systems. Universities are not teaching them anymore
| despite having being successfully applied since the 2010s to the
| development of so many cloud systems that other companies can
| rely on.
| magarnicle wrote:
| Anymore? Did they ever? In my course of formal methods it was
| all done by hand proving Haskell functions or using Hoare logic
| on code. We never used any tools like TLA.
| amenghra wrote:
| "I think we can increase the TLC model checker throughput to 1
| billion states per minute (1000x speedup) by writing a bytecode
| interpreter. C"
|
| I never used TLC with a large model, but I bet making the tool
| faster would make it more useful to lots of people.
|
| I wonder what the speedup would be if the code targeted a GPU?
| PessimalDecimal wrote:
| Agreed.
|
| But I wonder if the logic of model checking is actually
| amenable to vectorization. I suspect not really, even for
| something basic like checking safety properties where you could
| try to shard the state space across cores. There is still
| likely to be some synchronization that is needed that
| eliminates the benefits. A cheaper way to test it would be to
| look to vectorize on the CPU first.
|
| For a pure hardware based speedup, if there is effort to
| transcompile TLA+ specs to C++, there could then be a further
| step to transcompile that to say Verilog and try to run the
| model checking on an FPGA. That _might_ pay off.
| bvrmn wrote:
| Even 10x speedup would be amazing. Just imagine current 1min
| check would be performed in 6s.
| ahelwer wrote:
| There is a strong Jevons Paradox effect at play here though,
| people generally have a set amount of wall-clock time (1
| minute, 10 minutes, etc.) they budget to check their model
| and then find the largest model that fits within that wall-
| clock time. So really this just increases the size of the
| state space people will explore, which might be the
| difference between checking, say, 3 vs. 5 nodes in a
| distributed system.
| bvrmn wrote:
| For TLA it's even worse. Increasing node counts makes the
| spec immediately more "correct", at least it feels like
| that xdd.
| alfalfasprout wrote:
| TBH, as cool as TLA+ is, the biggest issue I generally see with
| trying to use formal methods in practice is that you need to keep
| the specification matching the actual implementation. Otherwise
| whatever you've formally verified doesn't match what actually got
| built.
|
| So formal methods may be used for extremely critical parts of
| systems (eg; safety critical systems or in embedded where later
| fixes cannot be readily rolled out) but they fail to make inroads
| in most other development because it's a lot of extra work.
| ahelwer wrote:
| Hillel Wayne wrote a post[0] about this issue recently, but on
| a practical level I think I want to address it by writing a
| "how-to" on trace validation & model-based testing. There are a
| lot of projects out there that have tried this, where you
| either get your formal model to generate events that push your
| system around the state space or you collect traces from your
| system and validate that they're a correct behavior of your
| specification. Unfortunately, there isn't a good guide out
| there on how to do this; everybody kind of rolls their own,
| presents the conference talk, rinse repeat.
|
| But yeah, that's basically the answer to the conformance
| problem for these sort of lightweight formal methods. Trace
| validation or model-based testing.
|
| [0] https://buttondown.com/hillelwayne/archive/requirements-
| chan...)
| sterlind wrote:
| Plus my Kayfabe system [0], which was partly inspired by Ron
| Pressler's article on trace validation:
|
| 0. https://conf.tlapl.us/2020/11-Star_Dorminey-
| Kayfabe_Model_ba...
| lovich wrote:
| why are the lower case L's in that document bolded? a
| different weight? Not sure what the right technical change
| term is for the visual difference but it was extremely
| noticeable immediately upon opening the document
| hwayne wrote:
| To be totally fair, my article is about the problem of
| writing specs when your product features could change week to
| week, whereas I think u/alfalfasprout is talking about
| regular updates to an existing system slowly bringing it out
| of sync with the spec. For the latter problem, yeah trace
| validation and model-based testing is the best approach we
| have so far.
| im_down_w_otp wrote:
| We do a version of this approach for system behavior V&V:
| https://docs.auxon.io/conform
| yuppiemephisto wrote:
| What do you think of embedding it in a formal system like Lean
| as a frontend?
| jazzyjackson wrote:
| On the other hand, how many million man hours are spent re
| inventing the wheel that could instead be spent contributing to
| a library of extremely well-specified wheels?
| dkarl wrote:
| I've always seen it as a tool for validating a design rather
| than an implementation.
| cmrdporcupine wrote:
| _" The 2025 TLA+ Community Event was held last week on May 4th at
| McMaster University in Hamilton, Ontario, Canada. "_
|
| Damn. Happened a 10 minute drive from my house and I didn't even
| know about it.
|
| TLA+ is on the infinite bucket list for me. I'm sure like many
| others, I know the value of learning and applying formal
| verification, but it feels impenetrable knowing really how to
| jump in.
| ahelwer wrote:
| Hillel Wayne wrote https://learntla.com/ which is quite good!
| Leslie Lamport also has a webpage of other possible learning
| resources, including a video course he put together where he
| wears many strange hats:
| https://lamport.azurewebsites.net/tla/learning.html
|
| Personally I learned by reading the first few chapters of
| _Specifying Systems_.
| hbogert wrote:
| ^ this feeling, i have it too. Everytime i see TLA+ somewhere i
| get that shameful feeling.
| layer8 wrote:
| The article doesn't mention PlusCal. What is the future of that,
| will it co-evolve with TLA+?
| ahelwer wrote:
| There are some proposals floating around to evolve PlusCal.
| Probably the most prominent is Distributed PlusCal[0]. There's
| a programming language lab at UBC which is also doing a lot of
| experimentation with transpiling PlusCal to Golang[1]. They
| presented a paper at the latest community event.
|
| The PlusCal-to-TLA+ transpiler is considered part of the core
| TLA+ tools and will definitely keep being maintained.
|
| [0] https://conf.tlapl.us/2020/03-Heba_AlKayed-
| An_Extension_of_P...
|
| [1] https://distcompiler.github.io/
| dgan wrote:
| about a year ago, at my job, i wrote a spec for authentication in
| TLA+, and while writing it, i discovered a bug/attack vector,
| which would allow an attacker to basically bypass the double-
| authentication.
|
| It surely did produce a fancy, mathy PDF which I proudly shown
| and explained to my team, but honestly, a little duck-talking
| would have permitted to find the same bug without TLA+
|
| For aome context, it's a CRUD api + web interface for external
| clients, nothing too complicated, and I really wanted to try TLA+
| in real life
| pron wrote:
| > I think we can increase the TLC model checker throughput to 1
| billion states per minute (1000x speedup) by writing a bytecode
| interpreter.
|
| Truffle [1] can convert an interpreter to a JIT compiler --
| there's no need to invent bytecode, and instead of an interpreter
| you get compilation to native, and it's easy to add intrinsics in
| Java; optimisations can be added gradually over time. This would
| probably be the most effective strategy, even in general, and
| certainly compared to cost.
|
| [1]: https://www.graalvm.org/latest/graalvm-as-a-
| platform/languag...
| ahelwer wrote:
| That's very neat! I will look at Truffle. The TLA+ interpreter
| is definitely "weird" in that it does this double duty of both
| evaluating a predicate while also using that same predicate to
| extract hints about possible next states. I wonder how well
| this highly unusual side-effectful pattern can be captured in
| Truffle.
|
| Edit: okay the more I look into GraalVM the more impressed I
| am. I will have to sit down and really go through their docs.
| Oracle was actually cooking here.
| PessimalDecimal wrote:
| I'm very happy to see this!
|
| A few years ago I tried making some contributions to the TLC
| codebase. It was definitely "academic code," lacking tests,
| reinvesting basic structured instead of using them from
| libraries, and largely the work of a single contributor with
| seemingly no code reviews for commits. I was motivated to try to
| help improve things and wanted to get a sense for what that would
| be like by sending a small PR to get a feeling for working with
| the code owners. They basically stonewalled me. It was odd.
| ahelwer wrote:
| There has definitely been a focus on improving developer
| onboarding in the past few years! If someone's PR is rejected
| now that can be considered a failure of the process, something
| to be fixed. I think when TLA+ was mostly a product of MSR this
| sort of thing could kind of fly (still unfortunate) but now
| that we're out in the wild with a foundation it's really a
| survival thing to not bounce willing contributors.
| geertj wrote:
| My current thinking on model checking (still evolving):
|
| Modeling languages are useful to check the correctness of an
| algorithm during development. During development, a model can
| also serve as a specification for the actual implementation. This
| requires that your the modeling language is readable to a broad
| range of developers, which TLA+ is not. We have been
| experimenting with FizzBee (fizzbee.io) which looks promising in
| this regards.
|
| When you go to prod, you really want to test your actual
| implementation, not a model of it. For this you want something
| like https://github.com/awslabs/shuttle (for Rust), or
| https://github.com/cmu-pasta/fray (for Java). Or use something
| custom.
| bvrmn wrote:
| TLA+ has its own quirks, you could add sugar here and there,
| but from semantic standpoint you couldn't do much. It's
| "unreadable" because requires some mental model most of
| developers don't have. My point: you either provide "simple"
| tools which could do nothing for real models or they become on
| same level of "unreadableness" really fast.
| bugarela wrote:
| It is in deed tricky, but we tried. We fully kept the
| semantics of TLA+, so the same mental model people still need
| to learn (at least a little), but a syntax that is much more
| familiar to engineers/programmers.
|
| This is Quint [1], a different syntax for TLA+ with some
| extra tooling (type checker, CLI, evaluator, REPL, VSCode
| extension, testing framework, etc) which can be transpiled to
| TLA+ (which is a very direct translation, as the semantics is
| the same [2]) and therefore make use of the TLA+ tools as
| well (mainly the model checkers).
|
| I think this is far from the same level of "unreadableness"
| than TLA+, and it makes formal methods much more
| approachable. It would be great if you could take a look and
| tell me whether you agree.
|
| [1]: https://quint-lang.org/ [2]: https://quint-
| lang.org/docs/lang
| bvrmn wrote:
| I did an eval of Quint about year ago and did not find it
| compelling. It constantly refers to TLA+ and doesn't bring
| much benefits except typing. Syntax tries to cover
| underlying fact that state machine is expressed in terms of
| logic and math using "understandable" for programmers
| concept but it's very leaky in the end. IMHO "assign" is
| quite hard to grok without TLA experience. Documentation is
| scarce.
|
| The most frustrating part it's hard to use with TLA+
| background. I know how to do something in TLA but have no
| clue with Quint because translation rules aren't direct and
| obvious.
|
| On the other hand it's a way better than PlusCal!
|
| But I'm heavily biased. Please take this "critique" as a
| mumble from TLA+ initiated duckling.
| hwayne wrote:
| I taught a lot of people TLA+ and while there's definitely
| essential complexity, a nontrivial amount is just syntactic
| friction. Consider \A x \in set: x.id /= 1
| /\ ~x.active
|
| vs all x in set: x.id != 1 && !x.active
|
| The latter has the same semantics but is much easier to read
| for the average developer, and more importantly is easier to
| type without syntax errors.
| bvrmn wrote:
| I agree, latexisms in TLA are on eye brow level of
| weirdness. Lesser punctuation syntax is always better.
| elcapitan wrote:
| That is literally what is holding me back every single time
| I get back to TLA+. I love your book and posts and always
| use it as reference to get back into it, but most of that
| "getting back" is just trying to remember all the minutia
| of the syntax. I wish there was simply a transpiler from
| some common syntax into TLA+. I don't even need Pluscal for
| the most part, and I'm fine with the concepts of temporal
| logic.
| bugarela wrote:
| You can also use Model-Based Testing (MBT) and produce
| (arbitrarily many) tests for your production code from your
| (model-checked) model.
| kurtis_reed wrote:
| So how can we contribute?
| wigster wrote:
| TLA is the worst TLA possible. I'm too old for any more.
___________________________________________________________________
(page generated 2025-05-16 23:02 UTC)