Update 01/07/19 Greetings from 2019! The good news is that Chicago isn’t yet a radioactive crater. The bad news is almost everything I said about refinement in this article is wrong. I’m working on writing a more in-depth, rigorous treatment of refinement as its own article. But this one is currently explaining something that definitely isn’t refinement. mkay thanks! Update 2020-10-05: I’m probably not going to write that article on refinement in the near future and also Chicago is a ...| Hillel Wayne
Last year a client asked me to solve a problem: they wanted to be able to compose two large TLA+ specs as part of a larger system. Normally you’re not supposed to do this and instead write one large spec with both systems hardcoded in, but these specs were enormous and had many internal invariants of their own. They needed a way to develop the two specs independently and then integrate them with minimal overhead.| Hillel Wayne
tl;dr: online TLA+ manual/advanced techniques/examples here. TLA+ is a tool for testing abstract software designs. I first stumbled on it in 2016 and found it so useful I wrote a free online guide to help others learn it. Then I decided the guide wasn’t good enough and wrote Practical TLA+ in 2018. Then I decided the book wasn’t good enough and needed a second edition. Just kidding! Book’s never getting a second edition, because it costs $26 and no matter how good I make it, it’s neve...| Hillel Wayne
Graphing TLA+ state spaces for fun and profit.| Hillel Wayne
People always tell me that the hardest part of learning TLA+ is finding good examples. This makes sense to me: most of the main ones out there are either toy problems or immensely complex algorithms. It’s sort of the nature of TLA+: if you’re using it, you’re trying to design something complicated, and that’s usually because you’re trying to sell something complicated. Also, the community is tiny. You could probably fit all of the TLA+ experts in the world in a small coffee shop.| Hillel Wayne
I’m writing a book on TLA+! It’s going to be aimed at the same audience as Learn TLA+, but dive much deeper and go much further. I’ll be showing not just how to use TLA+, but how to think about systems, write good specifications, and fix models. I’m really excited and I’m sure you’ll be, too! I’m also trying to make it much better than Learn TLA+, because People are going to be paying money for this, so I can’t just phone it in I asked my technical reviewer to be “almost-com...| Hillel Wayne
In my 2021 TLAConf Talk I introduced a technique for encoding abstract data types (ADTs). For accessibility I’m reproducing it here. This post is aimed at intermediate-level TLA+ users who already understand action properties and the general concept of refinement. Say we want to add a LIFO stack to a specification. You can push to and pop from the end of this stack but you cannot change data in the middle.| Hillel Wayne
When teaching formal methods, I often get asked how we can connect the specifications we write to the code we produce. One way we do this is with refinement. All examples are in TLA+.1 Imagine we’re designing a multithreaded counter. We don’t know how we’re going to implement it yet, so we start by specifying the abstract behavior.2 ---- MODULE abstract ---- EXTENDS Integers, Sequences VARIABLES pc, counter vars == <> \* Two threads Threads == 1.| Hillel Wayne
There’s not a whole lot on TLA+ technique out there: all the resources are either introductions or case studies. Good for people starting out, bad for people past that. I think we need to write more intermediate-level stuff, what Ben Kuhn calls Blub studies. Here’s an attempt at that. Most TLA+ properties are invariants, properties that must be true for every state in the behavior. If we have a simple counter:| Hillel Wayne
My job these days is teaching TLA+ and formal methods: specifying designs to find bugs in them. But just knowing the syntax isn’t enough to write specs, and it helps to have examples to draw from. I recently read Chris Siebenmann’s Even in Go, concurrency is still not easy and thought it would make a good case study for writing a spec. In it, he gives an example of Go code which deadlocks:| Hillel Wayne
I’m in the process of revising some of my workshops. I realized that one particular important aspect of TLA+, fairness, is something that I’ve struggled to explain well. Then again, everybody struggles to explain it well! It’s also a great example of how messy concurrent systems can get, so I figured it would make a good post for the blog. Stuttering Take the following spec of a clock. I used TLA+ but it should mostly be clear from context:| Hillel Wayne
In most testing frameworks, you’re expected to write a lot of low-level tests and few high-level tests. The reasoning is that end-to-end tests are slow and expensive and only cover a tiny amount of the program’s state space. It’s better to focus on testing all the parts in isolation versus testing that they all work together. In practice, global correctness does not follow from local correctness. It’s possible for every part to be individually rock-solid but the system to be broken as...| Hillel Wayne
This is an “intro packet” you can use to argue for the benefits of formal methods (FM) to your boss. It’s a short explanation, a list of benefits and case studies, and a demo. Everything’s in TLA+, but the arguments apply equally well to Alloy, B, statecharts, etc. Adapt the material to your specific needs. Quick notational note: I’m leaving out the code verification side of formal methods, mostly because design verification is a much easier sell.| Hillel Wayne
When we design programs, we usually look for two kinds of properties: that “bad things” never happen and that “good things” are guaranteed to happen. These are called safety and liveness properties, respectively. These are properties that we want to hold true for every possible program behavior. “We always complete every request” is a liveness property. If our system has it, every program trace will complete every request. If it doesn’t hold, I can give you a example behavior wh...| Hillel Wayne
A common question I get about specs is how to model bad actors. Usually this is one of two contexts: The spec involves several interacting agents sharing a protocol, but some of the nodes are faulty or malicious: they will intentionally try to subvert the system. The spec involves an agent subject to outside forces, like someone can throw a rock at your sensor. These “open world” situations are a great place to use formal methods.| Hillel Wayne
I recently did a corporate TLA+ workshop and some people asked what TLA+ specs look like in practice. If you looked at the most common public examples, you’d probably come away thinking that people only used it for critical consensus algorithms. This is a problem for two reasons: first, it makes it harder to learn TLA+, as there aren’t simpler examples to experiment with. Second, it makes it hard for people to see how TLA+ is useful for them.| Hillel Wayne
I am delighted to announce that my book, Practical TLA+, is now available! When I stumbled into TLA+ in 2016 I had no idea it would so define my passions, my values, and my career. I definitely didn’t think I’d be writing a book. But 11 months and 220 pages later, here we are! This is the largest project I’ve ever done and I’m incredibly excited to share it with you all.| Hillel Wayne
I really like the c2 wiki as a historical artifact: a lot of big names in Agile and Extreme Programming argued with each other there.1 One thing they did was the Extreme Programming Challenge, where people tried to test the limits of these approaches. They’d find edge problems (designing databases, remote teams, etc) and see if Agile/XP still worked in that context. In almost every case they quickly decided that yes, it works just fine.| Hillel Wayne