hckrnws

> 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...

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.

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.

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.

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

    all x in set: x.id != 1 && !x.active

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.

I agree, latexisms in TLA are on eye brow level of weirdness. Lesser punctuation syntax is always better.

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

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.

You can also use Model-Based Testing (MBT) and produce (arbitrarily many) tests for your production code from your (model-checked) model.

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.

I've always seen it as a tool for validating a design rather than an implementation.

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?

What do you think of embedding it in a formal system like Lean as a frontend?

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...)

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.

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...

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

We do a version of this approach for system behavior V&V: https://docs.auxon.io/conform

"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?

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.

Even 10x speedup would be amazing. Just imagine current 1min check would be performed in 6s.

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.

For TLA it's even worse. Increasing node counts makes the spec immediately more "correct", at least it feels like that xdd.

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.

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.

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.

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.

That's great to hear, and I'm encouraged to try again. Thank you!

The article doesn’t mention PlusCal. What is the future of that, will it co-evolve with TLA⁺?

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/

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

"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.

^ this feeling, i have it too. Everytime i see TLA+ somewhere i get that shameful feeling.

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.

TLA is the worst TLA possible. I'm too old for any more.

So how can we contribute?