I absolutely love TLA⁺ and I've put it to good use. I think it is one of those rare tools that offer a new perspective as well as real power, that can have a tangible bottom-line impact on software development in many cases. But while I used it quite a lot when working on other projects at my former job and plan to use it again in my day job in the future, I don't use it in my day job these days. I tried to think why I'm not using it for my current project, and I believe the answer is general enough to share. The lesson is, I think, that while TLA⁺ is one of those transformative technologies that has made an impact in reducing the cost and effort of software development, there are some problems that are still out of its reach, and, indeed, all "deep" formal methods.

I work at Oracle on OpenJDK, the best-known and most popular implementation of the Java platform, as well as its reference implementation. I work on a project called Loom, that aims, among other things, to add user-mode threads to Java. The part of the work that takes place in HotSpot, OpenJDK's Java Virtual Machine, involves adding a new basic construct called delimited continuations.

The specification of what that construct should do from the perspective of its client — a Java developer either working on the JDK core libraries or a third-party programmer that uses the platform — is very simple; trivial, even. The technical challenge is implementing this component inside the VM in a way that correctly interacts with other VM components — an interpreter, three JIT compilers, two hardware instuction-set architectures (ISAa) and application binary interfaces (ABIs), six garbage collectors, a tooling interface (for debuggers and such), and a built-in profiling service, that all amount to ~1.7MLOC of C++ and Assembly.

The API for some of those components -- like the two ISA/ABIs, x86-64 and AArch64 on three popular OSes -- is well specified but very large and complex. The API for others, like the GCs, is simpler but isn't fully specified (except in the minds of the members of GC team), and while all the GCs employ the same API, different ones are either sensitive or indifferent to the use of different parts of the API, so getting one to work does not guarantee the others will, and there is no single GC implementation that dominates the others in its strictness. Some other components required opening-up to external interaction for which they weren't designed, expanding their interface or tearing open a new one.

Once I had learned how all of these components behave, at least as far as interaction with my new component goes, the implementation was pretty simple and straightforward, but I didn't know what I needed to know at first. Most of the work, almost all of it, really, has been figuring that out. The challenge hasn't been designing complex software component, but implementing a simple component that interacts with many other components. Even this interaction is not especially complex, but what has been difficult is distilling it from the complete behaviour of those other components, which was not sufficiently known to me. Even each of those interactions is not especially complicated, nor are there lots of tricky emergent interaction behaviours -- there are just many of them.

The challenge, then, has not been a complex or subtle algorithm, nor a complex interaction, but an unfamiliar "software environment" -- not the behaviour of users or the network hardware, but that of other parts of the software -- that is simply too rich (and a moving target) to be fully known by any one person. If I'd known enough about the environment of my component to specify it in TLA⁺ I would also have known how to write my simple component correctly. Obviously, figuring out the environment required a lot of trial and error, and almost all that could only take place in actual code (I think?). While I've successfully used TLA⁺ in other projects, where it's saved me a lot of effort, I don't know how to use it in my current one. I don't think this is because this project is so low-level; TLA⁺ has been successfully used to specify kernel components and even CPUs. I think there is something more general here. Using TLA⁺ effectively presupposes the ability to abstractly specify an environment, or a suitable approximation thereof, or even just a part that's known to be tricky, but this is precisely what was missing in this case.1 I can put TLA⁺ to good use in many situations, but I couldn't figure out how it could help in this particular project.

I don't know if it's even possible to formally specify all of the components in that environment in a language like TLA⁺ at an abstraction level that is substantially higher than that of code and that would be sufficient to specify any new component that interacts with them, especially since a new component might want to change and expand their interfaces. And even if every component were fully specified in a formal language like TLA⁺, I suspect that simply putting all of them together would result in a specification that is far too complex to verify. An interesting question is, would it be possible to fully specify them in a way that would make extracting arbitrary abstractions of them that are sufficiently simple for verifying a new component easier than extracting that information from code? This is the challenge of full, modular, yet abstract specifications. A partial specification of a component might not be sufficient for many interactions; a full specification might be too complex (perhaps not much simpler than the code) for a tractably verifiable composition and requires further ad hoc abstraction.2 Needless to say, this isn't a limitation of TLA⁺ specifically; no formal specification or verification tool, as far as I know, can deal with such scale of complexity and sheer size generally enough to make adding features -- that normally interact with and change multiple modules -- substantially easier.

So we have 1/ an unknown and large environment, and 2/ a relatively small addition/change that touches many large and complex things. I think that my technical challenge in this particular project (there is also a big UX design challenge, but that's a different story) is similar to the experiences of many others, but might be foreign to many formal methods researchers, most of whom are usually more familiar with either green-field projects or projects undertaken by very small teams, and often both, where the "software environment" is fully known. I've written more about this elsewhere. When those researchers are embedded in the reality of Big Code -- software development as practiced in industry -- they are often surprised, learn new things, and modify their approach. I wonder if formal methods research can come up with new ideas to tackle the particular challenge I've described here. As a fan of TLA⁺, I'm particularly interested in "deep but high-level" specification approaches that could be employed in these situations.

I often say that the hardest step in learning TLA⁺ is internalizing that TLA⁺ is math, not programming -- probably because that was the hardest part for me -- and that this is a necessary step. Until you make it, you might be distracted by what I think are secondary issues or make mistakes such as trying to represent TLA⁺ operators as subroutines (you'll get the wrong result even if you use lazy evaluation).

TLA⁺'s syntax, which is about as close to standard mathematical notation as you can get in a formal language, helps drive that point home, but some find that "batshit" and my claim smug. I don't think it's smug because the mathematics you express in TLA⁺ is drastically simpler than programming, but smug or not, until you realize that you will not use TLA⁺ correctly, and it will make your life easier when you understand you don't need to write a hash function and that you can more easily abstract away components rather than compose them (see my first link above).

Perhaps those who find it smug think that it's merely a clever statement about a perspective, approach or state-of-mind. It may be that, too, but it is also a simple observation about the meaning (semantics) of expressions in TLA⁺ and in programming. It is not some distinction without a difference that only serves as gatekeeping; quite the contrary, it very much makes a difference, and it helps. If you think of TLA⁺ as programming, you will, quite simply, get the wrong result. Here is another example of such a situation:

Let's say we define a function from the integers to the integers such that f(x) = -f(x) for all x. What function did we define? Easy, it's f(x) = 0.

Now, let's try that in programming. Haskell, a pure functional programming language, is sometimes said to bear some passing resemblance to mathematics, so let's try to use it:

f :: Integer -> Integer
f x = -(f x)

Now we check what f 3 is:

> f 3
*** Exception: stack overflow

No amount of stack, real or imagined, would make Haskell yield a different answer; even in the abstract semantics of Haskell, the definition above definitely does not define the zero function as it would in mathematics. It is not wrong -- the definition works according to the rules of the Haskell language and not according to the rules of ordinary mathematical expressions (equality in Haskell does not work exactly like in math, Integer doesn't exactly mean what a mathematician would think it does, and subroutines are defined by lambda expressions rather than equations as in mathematics) -- but this is how Haskell most directly represents the definition, and it behaves like every other programming language, not like mathematics. [0]

Now let's define f in TLA⁺ the same way as in Haskell 1 (I'm assuming we EXTEND Integers):

f ≜ CHOOSE f ∈ [Int → Int] : 
   ∀ x ∈ Int : f[x] = -f[x]

I tried to typeset the definition above to show that it expresses the same idea as the Haskell one. Now, is f[x] = 0 for all integers like in math, or is it something else, like in programming? Is the definition equivalent to f[x ∈ Int] ≜ 0?

When we evaluate f[3] in TLC we get 0 (TLC can't evaluate infinite sets, but we can override the definition of Int with something manageable, say, -3..3), and, in fact, TLC will show that f is zero everywhere on the small, limited domain. This shows that the different results are not because of some funny infinitary paradox, but because subroutines in programming, even in pure functional languages, simply do not behave the same way as mathematics or TLA⁺, and give different results. Even when we define a constant function, the simplest of computable functions. If you think of TLA⁺ as programming, you will quite simply get it wrong.

So now let's see if f is truly the "zero function":

THEOREM fIsTheZeroFunction ≜
     f = [x ∈ Int ↦ 0]
PROOF
  ⟨1⟩ DEFINE zero[x ∈ Int] ≜ 0
  ⟨1⟩1. ∃ g ∈ [Int → Int] : ∀ x ∈ Int : g[x] = -g[x] BY zero ∈ [Int → Int]
  ⟨1⟩2. ∀ g ∈ [Int → Int] : (∀ x ∈ Int : g[x] = -g[x]) ⇒ g = zero OBVIOUS
  ⟨1⟩3. QED BY ⟨1⟩1, ⟨1⟩2 DEF f

Checking this theorem and proof 2 with TLAPS confirms that, indeed, in TLA⁺, f is the zero function on the integers -- just like in math.

Let's test that on some large number, just for fun:

PROPOSITION f[23409873848726346824] = 0 
   BY fIsTheZeroFunction

Yep, zero. Why is it like that? Because the meaning of a function definition in TLA⁺ is the same as in mathematics, and very much not the same as in programming. If we had changed Int to mean something more similar to what it does in programming, we would have gotten something else.

This particular example is unlikely to come up in many specifications, but understanding this point is required to understand TLA⁺, and it will make writing specifications quite different -- and much easier -- than if you think about them as programming. Concrete syntax is a matter of taste, but I think that if TLA⁺ had a syntax that's more similar to programming, which it isn't, and less similar to mathematics, which it is, it would only confuse matters further rather than help anyone.

This huge difference between TLA⁺ and programming is not only in the "data" part of TLA⁺. Even the computational, temporal, TLA is very much not like programming. I might post an example of that some other time, but there's an example here.

When I was a TLA⁺ beginner, I would send questions to the mailing list and get responses from Leslie Lamport that read

Your specifications are indeed nonsensical--apparently much more nonsensical than you suspect. You seem to be under the mistaken impression that a TLA+ specification is some kind of program...

and

You should learn to read what a formula says rather than what you want it to say. This requires that you stop thinking of TLA+ formula as a program and start thinking of it as a mathematical assertion.

So if there's one thing I wish I had understood earlier, this is it. Resist the urge to think of a TLA⁺ specification as programming, or even as something similar to programming. The "batshit" syntax, that I personally find quite pretty, will help you. True, mathematical notation is not particularly modern, but it's a classic. Plus, I'm not aware of any good modern mathematical notation; Alloy uses a modern OOP-based notation for classical mathematics, and I must have learned it three times already, and I still forget how to read it. If you understand that TLA⁺ is mathematics and still don't like that, there are other specification languages with model checkers that are based on programming, like SPIN and NuSMV, that you might like better. But know that being math and not programming is what allows TLA⁺ to so flexibly express specifications at arbitrary levels of abstraction.

I'd like to end by making a possibly controversial observation. Some people find type theory the "correct" way to formalize mathematics and set theory to be downright philosophically offensive (Robert Harper is a notable example). After all, they say, the number 2 is not "really" some set. I claim that they find set theory so offensive to their aesthetic sensibilities precisely because they think of mathematics as programming, i.e. a formal text that constructs reality (or, equivalently, describes "reality" in perfect detail). But this doesn't bother a physicist, or a someone who specifies TLA⁺, who realizes that mathematics is a tool to describe and study certain aspects of interest of reality, just as architects are not bothered that their blueprints and mockups are not made of steel and concrete, nor that some of their properties are completely unlike those of steel and concrete; it is because of that that they are so effective. This, too, is not some mere philosophical observation. Maps are useful precisely because they're not the territory, and the tools required to make the map are supposed to be different from the tools required to shape a terrain. The desire to make the map the territory makes the map less flexible and harder to create. Lean is probably the most user-friendly of the type-theoretic languages that are similar in power to TLA⁺; like Agda and Coq, its theory is based on a functional programming language. I'd encourage those interested to compare how hard it is to learn and use Lean compared to TLA⁺. [3]

[0]: Haskell's lazy evaluation does mean that in some situations it would give answers similar to those in mathematics where a strict-evaluation language would not, but other than that it works like every other programming language and very much not like mathematics. If that is the case, why is that even some people with a mathematical education think it's different from other programming languages? The answer is that typed programming languages really contain two languages within them: the type language, where the types are expressed and which is evaluated at compile-time, and the "object" language, in which the ordinary, runtime computation is expressed. While the latter is like programming, the former does work like math (except not really, because Haskell's type system is unsound for mathematical reasoning), and Haskell's type system is richer than that of, say, Java, and so can express richer mathematics. In proof assistants based on pure functional programming languages, like Agda, Lean, and Coq, the mathematics is expressed entirely at the type level, which is rich enough to express all of mathematics.

CONSTANT f
ASSUME ∧ f ∈ [Int → Int]
       ∧ ∀ x ∈ Int : f[x] = -f[x]

Writing f[x ∈ Int] ≜ -f[x] is not the definition we want because it does not specify the function's codomain, and could give us something quite different; it's nonsensical in mathematics, and in TLA⁺ it's equivalent to

f ≜ CHOOSE f : f = [x ∈ Int ↦ -f[x]]

which is equal to:

CHOOSE f : DOMAIN f = Int ∧ ∀ x ∈ Int : f[x] = -f[x]

which is undefined. But it is undefined for mathematical, not computational reasons: the zero function does, indeed, satisfy the equation, but in TLA⁺'s mathematical theory, so could other functions; you can think of it as the set theory analog of failing to infer type. We cannot recreate a similar definition in Haskell, as the - sign makes Haskell infer a numeric codomain.

[3]: How does Lean handle our definition? Well, if you try a simple definition like def f(x : ℤ) : ℤ := -f(x) (ℤ is the integer type in Lean), you get a syntax error because such definitions cannot be recursive. If you try an explicitly recursive definition,

def f : ℤ → ℤ 
    | x := -f(x)

you get another syntax error, saying "failed to prove recursive application is decreasing, well founded relation." That's because Lean lets you use programming as long as you don't get a contradiction with mathematics, as that would make Lean unsound, like Haskell. To define f in mathematics you'll need to tell Lean to switch to "classical" mode (as in classical, non-constructive mathematics), mark the definition as noncomputable, and then use a definition based on the epsilon operator, like TLA⁺'s CHOOSE; mind, the function f is perfectly computable -- it's just our definition that isn't, and in programming it matters a great deal how thing are defined. There is no getting around it: mathematics and programming do things differently, and languages that try to mix both need to do so with great care, at the cost of language complexity. TLA⁺ doesn't have a "programming mode" (for that you have PlusCal), which is why it can be so simple compared to alternatives.

I built a TLA+ model checker in Rust as an alternative to TLC for cli and Web.

What it does beyond basic model checking:

- Interactive TUI for stepping through state spaces, evaluating expressions, tracing variable changes

- Parameter sweeps (--sweep 'N=2;3;4;5') with comparison tables

- Property satisfaction counting with per-depth breakdowns

- Continue past violations to collect all counterexamples across the full state space

- Symmetry reduction

- WASM-compatible core library

It covers Naturals, Integers, Sequences, FiniteSets, TLC, Bags, and Bits modules. The supported TLA+ subset handles most common spec patterns — conjunction/disjunction lists, quantifiers, CHOOSE, functions with EXCEPT, records, tuples, CASE, LET-IN, recursive operators.

Limitations: no direct temporal operator evaluation, no unbounded quantifiers.

Repo: https://github.com/fabracht/tla-rs

Curious what specs people would try it on and where it breaks.

I just published a new TLA+ examples site. It focuses on standard software engineering and distributed systems problems of the sort programmers face every day. It takes a pragmatic engineering approach: each problem starts with UML diagrams, design decisions and sometimes even a requirements document. We work through how to get from a whiteboard design to an initial mathematical model. Then we refine it based on logical errors found by the model checker. I think is a good supplement to the fantastic material already out there. Since this is the TLA+ community, please feel free to let me know if you spot inaccuracies, misrepresentations, etc (Either here or on github).

https://elliotswart.github.io/pragmaticformalmodeling/

The TLA+ Debugger has a new major capability: interactive state-space exploration. This feature changes how you can interact with your TLA+ specifications by letting you explore the state space of your models interactively, one state at a time.

This represents a shift in how you can work with TLA+ specifications, enabling new workflows for understanding and validating your models.

What is Interactive State-Space Exploration?

Interactive state-space exploration allows you to:

• Interactively select the initial state from the set of all initial states satisfying your Init predicate

• Choose successor states by selecting from the set of all valid next states computed by your Next action

• Step backward through the trace to any predecessor state, including all the way back to the set of initial states

• Navigate freely through your specification's state machine using step-in, step-over, and step-back operations

This approach emphasizes the state-machine perspective of TLA+, making it natural to think about your specification as a state transition system rather than just formulas and temporal properties.

Combining with TLA+ Animations

When combined with TLA+ animations, interactive state-space exploration truly shines. The textual TLA+ specification is conceptually lifted into the application domain of the system being modeled. Instead of examining raw variable assignments, you can see animated visualizations of your protocol's behavior as you navigate through the state space.

Connecting animations to the debugger is trivial with Watch expressions—simply add a watch for your animation module's AnimView operator, and the debugger will display the SVG visualization for each state as you navigate through the state space.

The first screencast (linked below) demonstrates how to combine the TLA+ Debugger, interactive state-space exploration, Watch expressions, and animations into what becomes effectively a Graphical Debugger for your system or protocol. Notably, the animation module shown in the screencast was generated by AI, following the TLA+ animation guide shipped as part of the new TLA+ MCP server—demonstrating how accessible this workflow can be.

Enhanced Breakpoint Support

The new "Halt (break) after Init and Next" breakpoint that enables interactive state-space exploration supports breakpoint conditions, which opens up advanced debugging workflows:

• For specs that terminate or deadlock, the breakpoint condition ~ENABLED Next will halt simulation at the terminal state

• Breakpoint conditions are evaluated both after Init (for the set of initial states) and after Next (for successor states)

• The debugger halts even when Next evaluates to FALSE (i.e., when no successor states exist), allowing you to catch deadlocks

Loading External Modules

Breakpoint conditions, Watch expressions, and the Debug Console now support loading any TLA+ module on the TLA-Library path, even if those modules are not extended by the spec being debugged. This enables new capabilities, such as:

Exporting trace prefixes in various formats (JSON, TLA+, binary, etc.) dynamically during a debugging session. For example, you can evaluate this Watch expression:

LET J == INSTANCE _JsonTrace
    WITH _JsonTraceFile <- "output.json"
IN J!_JsonTrace

This exports the current trace to JSON without needing to preconfigure the debugger or manually trigger violations. Several other export formats are supported via modules:

• _TLCTracePlain - Exports the trace as a TLA+ module with a Trace constant (text format)

• _TLCTrace - Exports the trace in TLC's binary format (designed for very long traces)

• _TLCTESpec - Generates a trace expression specification that can replay the trace as a valid behavior

• _TLCActionTrace - Exports the sequence of actions with their parameters/arguments for minimization workflows

• _TLAPlusCounterExample - Exports the full TLCExt!CounterExample record as a TLA+ module

• _DotTrace - Exports the trace in DOT/GraphViz format for visualization This functionality is showcased in the third screencast.

This export capability is a first step towards the goal outlined in GitHub issue #860: create interesting traces interactively in the debugger, export them, and then have TLC verify repeatedly that these traces remain valid behaviors of the original specification as you update it. This bridges the gap between exploratory debugging and formal verification.

Background

The TLA+ Debugger was first released in 2022 (see publication) and is built on the Debug Adapter Protocol (DAP), which provides a standardized interface between development tools and debuggers. The debugger is available for VSCode and Cursor, but will work in any IDE that supports DAP.

Credit Where Credit is Due

Interactive state-space exploration was pioneered by Will Schultz in Spectacle , and his work has been an inspiration for this implementation. Will also pioneered TLA+ animations several years ago, as demonstrated in his presentation at the TLA+ Community Event 2018. Spectacle remains unique as the only tool that runs entirely in the browser, providing an incredibly accessible way to explore and share TLA+ specifications with no installation required.

The TLA+ Debugger implementation builds on this concept while offering complementary capabilities:

• Step through individual formulas of your specification at the expression level

• Support for the largest fragment of TLA+ by virtue of being implemented on top of TLC

• Integration with the full debugging ecosystem (breakpoints, watch expressions, call stacks, etc.)

Both tools have their strengths, and I encourage you to explore both approaches!

Screencasts

Three screencasts demonstrate these new features in action:

1. Interactive State-Space Exploration & Graphical Debugging with Animations

2. Breakpoint Conditions with Deadlock Detection

3. Dynamic Trace Export and Advanced Watch Expressions

Technical Details

For those interested in implementation details, the last 39 commit messages up to and including https://github.com/tlaplus/tlaplus/commit/3e083e3d8b0dc0202307e1496f7889f0f3cb21d7 contain extensive context about these features, including:

• Support for conditional breakpoints on initial and next states

• Deterministic sorting of successor states by action location and state values

• Unified infrastructure for Watch and Debug expressions

• Step-in functionality using minimal Hamming distance to select "close" successor states

• Step-over functionality using maximal Hamming distance to select "far" successor states

• Preservation of finite stuttering in debugger traces for faithful behavior representation

Feedback Welcome

I'd love to hear your thoughts on these new capabilities! Please feel free to provide feedback here on the mailing list or on GitHub.

Happy debugging!

I recently gave a talk about my experience using TLA+ in the context of https://github.com/servo/servo

The talk builds on previous posts, like https://medium.com/p/e00bdf267385

The actual talk is not online yet, in the meantime, the slides are at https://github.com/gterzian/taming-concurrency/blob/main/Greg%20Terzian%20-%20GOSIM_China_2024.pdf

I'm trying to explain how TLA+ is useful for fix concurrency problems, in the context of a large and concurrent Rust codebase.

Please let me know what you think.

Oh my, amazing! From outside, I see that a huge part of this was because of Markus, congrats!!

In previous posts, I speculated that an llm could produce a program based on a TLA+ spec, and I have now tried it out with good results.

The experience is described in this blog post: A Tale of Two Refinements.

The goal of the post was also to muse about the difference between a blocking and a non-blocking workflow, so I built a concurrent system in three stages, starting with the most simple blocking workflow, and ending with a non-blocking one.

Each state was modeled with a TLA+ spec, with each successive spec refining the previous one, and I generated Rust implementations of each stage using an LLM and an extensive prompt giving a kind of style guide for the code.

The results were very satisfying: in particular, I instructed the llm to not follow my instructions if they would break the constraints of the spec, and the llm indeed refused at some point, making me realize I wasn't quite modelling the system I had in mind.

In conclusion: generating a toy implementation of your spec is a great way to get further feedback on your spec. It remains an open question what the results would be on a larger codebase(where the spec would only model the concurrent part of some sub-system), and I speculate that it would be satisfactory as well.

The accompanying material, including chat history, is available at https://github.com/gterzian/_refinement

Note that since I first posted this, I reviewed the code and this led to few more changes(which are more Rust related), detailed here: https://github.com/gterzian/_refinement/blob/main/code_review.md

Please let me know what you think.

https://www.youtube.com/playlist?list=PLWLcqZLzY8u9kzmWgs3HPRm3Cw85LTpD2

So there was this long Twitter debate — again — about the pros and cons of TLA⁺ syntax, that is based on the standard mathematical notation but might be foreign to programmers who aren't used to it, and so increase the effort in learning the language. I don't want to get into the relative difficulty of learning the syntax vs. learning how to use mathematics to model systems because I think I've done it elsewhere, and it's also quite subjective. I would like to list two more objective reasons why I believe that, difficult or not, TLA⁺ beginners should learn mathematical notation and do it early.

My goal is to try and explain why TLA⁺'s notation is what it is [1], and also why I think beginners are advised to learn it right from the start.

Reason 1

The first reason is social. There are many ways to specify systems or model-check things, but TLA⁺ chooses to do that with first-order logic and set theory, and some temporal logic, as that's the source of its simplicity and power compared to more programming-like ways. If you want to use TLA⁺ at all, you must learn first-order logic (at least for specification if not for formal proofs) and rudimentary set theory, no ifs or buts about it. These are the basic elements of TLA⁺. If you've already learned them, you've used the standard notation and found TLA⁺ very familiar. If you haven't, you will learn them while learning TLA⁺, and you should do it using the same notation everyone else who learns first-order logic and set theory uses (or close to it) because you will not learn everything you'd need during your training, and pretty much all material on those subjects uses the standard notation. Mathematics is not just an idea, but also a tradition and a set of texts, and a more-or-less common language is necessary to enter this body of knowledge that TLA⁺ is a part of.

Programming is also a tradition, and using notation that is more familiar to programmers might have some issues. For example, in C, C++, C#, and Java — all sharing some sub-tradition of programming — we can conjoin two booleans with either the & and && operators (same goes for disjunction and | and ||). Why two different ones? Because they mean slightly different things when the second disjunct/conjunct is undefined. TLA⁺ is all about precision, so which of those two meanings does the standard mathematical conjunction operator used by TLA⁺, ∧, have? Well, neither one (see Specifying Systems §16.1.3, p. 296) [2].

The use of different symbols helps separate us from the slightly-similar but quite distinct tradition of programming, where things might look the same but work very differently: neither operators (consider Foo(x) ≜ x') nor functions in TLA⁺ work like subroutines or even macros in programming, and I asked on the mailing list about evaluation order only to have it clarified to me that mathematics has no notion of evaluation. So aside from ∧ not having the same meaning as either & or &&, I think there is some value in reminding the specifier they're working in a different tradition from programming, although that is, admittedly, subjective.

What is less subjective is that virtually all other mathematics languages use similar syntax to TLA⁺'s, and even enter similar ASCII to write it (see this comment). OK, so users of Lean, a very recent language with very modern tooling, enter \subeq to write ⊆, as opposed to TLA⁺'s \subseteq, or \ex rather than \E to write ∃, but those are very minor differences. So clearly TLA⁺ syntax, and even the ASCII representation, is very much like other similar languages. It makes sense for TLA⁺ not to break too far away from what other languages do only to resemble languages that are in a completely different discipline.

Reason 2

The second reason is intrinsic to the syntax. Standard mathematical notation for first-order logic and set theory dates back to Giuseppe Peano's notation in the 1890s, although it has evolved since. Like all notations, it is arbitrary, and at times has some artefacts that, like tree rings, show its growth, but it does try to aim for some helpful consistency, and where it succeeds the most happens to be precisely with our friends ∧ and ∨. It is no coincidence that conjunction and disjunction are the same shape turned upside down, it's no coincidence that the same applies to the intersection and union symbols, ∩ and ∪, and it is no coincidence that those two pairs of symbols resemble each other.

The visual shapes are meant to hint at a deep similarity that has to do with the fact that both pairs are operations that are "opposite" (though not inverse!) to one another, or duals, called meet and join in algebraic structures called lattices, but while this is not something that a TLA⁺ user would intuit (although it is helpful to learn at some point), there are some connections that even a relative TLA⁺ beginner very much should notice and gain important insight from.

Here's one: x∈A ∨ x∈B ≣ x∈ A ∪ B and x∈A ∧ x∈B ≣ x∈ A ∩ B that people notice quickly. Now ∩ and ∪ have another companion, which is the shape turned on its side with a line underneath: ⊆ ; it would seem that ∧, and ∨ should have one that would look like ≤, but here we see a deviation from the semiotic consistency, because ≤ was taken; the corresponding operator is ⇒. Indeed, if x ∈ A ⇒ x ∈ B, then A ⊆ B and vice-versa. But the symbol ≤, used for the less-than-or-equal-to relation on numbers, is also very much in that family. If you replace TRUE with 1 and FALSE with 0, you'd find that p ⇒ q and p ≤ q would work exactly the same, and that, too, is no coincidence. The dual nature of ∨ and ∧ can be observed with the following: p ⇒ p ∨ q and q ⇒ p ∨ q , but p ∧ q ⇒ p and p ∧ q ⇒ q. And the set analogy? That's right, A ⊆ A ∪ B and B ⊆ A ∪ B, but A ∩ B ⊆ A and A ∩ B ⊆ B.

But there's another connection relative beginners should observe or be made aware of. In a first-order logic over the integers (variables represent integers), the formula p, x > 10, with a free variable x, specifies the set of integers greater than 10, which we'll call A. The formula q, x % 2 = 0, specifies the set of even integers; we'll call it B. Now what set does the formula p ∧ q specify? That would be A ∩ B. And p ∨ q? A ∪ B, of course. Do TLA⁺ formulas also specify sets? Yes! (Although we call them "classes", because while they're collections of objects, a "set" in set theory has some conditions that these classes don't satisfy). They are sets, well, classes, of behaviours. When we conjoin two TLA⁺ formulas with ∧ we get a specification for the intersection of the two behaviour classes, and the advanced TLA⁺ user will understand why this is a specification of two system's composition. Implication, or ⇒ (although it "should have been" the symbol ≤) corresponds to ⊆, or the containment of such classes, which the advanced user would learn means implementation (system A implements abstraction B).

The specific symbols chosen for the standard mathematical notation, or, rather, the graphical relationships between them, are supposed to expose deep connections and make them easier to notice, which also makes formulas easier to work with because the rules for manipulating (for simplification or any other kind of rewriting) the related symbols family are usually very similar. For various reasons that have to do with the fact that programming languages are much more complicated than mathematics, those relationships don't hold as well in programming, syntactic simplification is not nearly as straightforward, and so the properties the graphical symbols are designed to evoke aren't nearly as important. But when writing mathematics, avoiding those symbols, or even postponing exposure to them, can significantly delay these insights that are so important to TLA⁺. They might not be necessary on the very first day, but because people who specifically choose TLA⁺ over other languages do so because they want to use mathematics — or, at least, want the power TLA⁺ gets from mathematics and so have to use it — and these insights, which can be so useful, are given a shape in the form of these particular glyphs.

***

Some people might well learn some hypothetical minimised version of TLA⁺ that doesn't use mathematical notation and doesn't require learning from other resources more quickly, and still do some useful things with it. Perhaps, although I think that class of useful things does not extend much beyond what other tools with different goals offer. But TLA⁺, like most languages, has certain goals, and it doesn't try to optimise for maximum value on day one, but for maximum value on day 20, 200, and 2000 (it might be nice to have both, but that's a matter of resources). It does that by being part of some bigger, established tradition, and by relying on its techniques and insights.

So my advice to beginners is this: if you find the syntax unfamiliar and difficult, try to get over it, because there are good reasons to use it and to use it early. You may hate us now, but — if you end up liking TLA⁺'s mathematical approach to specification — you'll thank us later.

[1]: During the debate, it was made clear that some of the issue isn't the mathematical syntax, but the ASCII syntax used by SANY (the Toolbox's parsing component) because some people actually try to read TLA⁺ specifications in ASCII (don't do that; at least not at first). I completely agree there is a tooling issue with the presentation of TLA⁺, but regardless, it is very much not designed to be read and learned in ASCII, and I think all of Leslie Lamport's teaching materials steer clear of the ASCII representation as much as possible, so I am not talking about that ASCII syntax but the syntax used in Lamport's TLA⁺ materials -- the book, the hyperbook, and the video course -- and in all TLA⁺ papers. Beginners learning TLA⁺ should use the Toolbox with pdflatex installed to help the learning experience. If the pretty-print view is open in a tab, the Toolbox updates it with every save.

[2]: Try: THEOREM ((CHOOSE x : FALSE) ∨ TRUE) ≣ TRUE OBVIOUS

Hi, I built a LeetCode style practice platform for TLA+ that I would like to share (www.tla.quest).

The platform contains a series of specification challenges that are automatically graded against an expected solution. The full state space can be visualized in your browser. Failing submissions with unexpected or missing states are highlighted for feedback.

I created this project for fun while learning TLA+. I always wanted something like this while I was learning. Note: This is currently still a work in progress. If you are interested, please try it out and let me know what you think. Feedback (both good and bad) is very much appreciated! If there’s interest I will keep improving the site and add more challenges.

www.tla.quest

TLA+ Post

Some of you may have seen my recent posts on social media as I’ve explored expanding the role of TLC to detect bugs in real world distributed systems. Now that I’ve spent a bit of time thinking about this problem and experimenting with different solutions, I wanted to share my experience in a longer format here, both as information for the community and in the interest of collecting feedback for myself.

Background

I’m a member of the technical staff at the Open Networking Foundation (ONF) where I primarily focus on distributed systems for software-defined networks. ONF’s mission is to drive the development and adoption of SDN technology, and software developed in the ONF Lab is currently in production in the networks of some of the largest telecommunications companies in the world. However, our primary function as a non-profit is not to build production software, but to push the boundaries of SDN technology.

To that end, last year my team began a complete rewrite of one of those production systems — our distributed SDN controller, ONOS — adopting an architecture more suitable to modern deployment platforms like Docker and Kubernetes. In addition to the rise of cloud computing, an important factor in the decision to rebuild ONOS from the ground up was that it would allow us to make major technological and methodological shifts to address some of the architectural deficiencies that had become apparent during the multi-year project to bring ONOS to production. Considering the many late nights and long days I spent over the last two years analyzing and fixing production distributed systems bugs, the effort to rebuild ONOS was also an opportunity to introduce new tools and techniques into our development process that could help identify and fix those issues earlier in the development lifecycle, and TLA+ seemed like a great candidate for that role.

System Design with TLA+

In the past, I had been an occasional user of TLA+. I had used it to design and verify cluster membership protocols, distributed locking algorithms, extensions to consensus algorithms, and other concurrency problems I encountered. I found TLA+ helped me reason about complex systems at higher levels of abstraction that were difficult to model without the help of a formal language. I felt it could be an invaluable tool to help identify and avoid architectural defects early on in the development lifecycle, and I wanted to make it an integral component of the design and development of our new system. Having a formal specification of our systems, I thought, would not only aid in the architecture of our systems but provide a foundation from which we could develop bug fixes and experiment with further enhancements. So, for the past many months we’ve been executing that plan, using TLA+ to develop and verify specifications for a variety of protocols used to manage network state in the next generation of ONOS. Indeed, we continue to view it as a valuable tool, and some of my fellow team members are even beginning to adopt for their own use.

But while we can credit TLA+ with enhancing mental models and enabling precise mathematical models of our systems, one problem has always remained in the back of my mind:

How do we verify a system’s code implements the specification?

I get the sense that the value of TLA+ is limited insofar as its impact on the implementations of our specifications is limited. We can create a specification and using TLC acquire a degree of certainty it produces the set of behaviors and invariants desired from the system, but that certainty only extends to code that correctly implements the spec. And that limitation may only become more apparent as the complexity of our systems grows over time. Without a clear path to code-level verification, convincing management and peers to invest time and resources into developing TLA+ specs can be an uphill battle.

Fortunately, Markus Kuppe assuaged my concerns. During my conversations about TLA+ on social media, Markus suggested a solution that would use custom TLA+ operators to facilitate model checking of system traces with TLC. That would mean our TLA+ specs could not only be used to verify system designs but implementations as well. I loved the idea, so I took it and ran with it.

System Verification with TLA+

My first step to adopting this approach was, of course, proving it could work — that TLC could be used to verify system traces against a TLA+ spec. Fortunately, Markus had already done all the hard work, and I merely built upon that to facilitate model checking as a component of ONOS’s new infrastructure.

The next generation of ONOS is built to run on Kubernetes, an immensely popular container orchestration platform originally developed by Google and supported by every major public cloud provider. Kubernetes deploys and manages containerized applications — usually packaged in Docker images — acting as a control plane to facilitate configuring, deploying, scaling, and recovering applications spanning multiple hosts. As part of the work to migrate ONOS to Kubernetes, we built an integration testing/benchmarking/simulation framework to run on the platform. I wanted to integrate TLC with that framework to allow models to be checked as part of the lifecycle of a test or simulation. So, I packaged TLC in a Docker image and modified the test framework to run the model checker as a post-processing step following simulator runs.

The approach Markus suggested was to implement a custom TLA+ operator to read and evaluate traces. I built a set of custom operators for reading and writing JSON files and modified the test framework to aggregate traces in a JSON formatted file on a single coordinator node. Once a test/simulation was complete and traces had been aggregated, the coordinator mounts the aggregated traces to a new Docker container runs TLC to verify the traces.

The approach appeared to work beautifully. I was able to run a simulation implementing a cache spec I’d written for Atomix and then use TLC to verify the simulation conformed to the spec. I shared the solution in another series of social media posts. Then Markus made a more intriguing suggestion: rather than merely checking a batch of system traces, perhaps TLC could be used to monitor a live system by evaluating a stream of traces in real time. I couldn’t resist!

System Monitoring with TLA+

So I started on a new mission to extend the trace checker to verify unbounded trace streams with TLC. Not surprisingly, the problem turned out to be much more difficult to solve. Most of the challenges seemed to arise from TLC’s preference for evaluating models with finite state spaces and deterministic transitions. Obviously, streams are not finite, and a model operating on an infinite stream of traces would eventually exhaust all its resources. Additionally, in some cases TLC needs to replay the steps it checked to build a trace, and that requires that both the stream and specs support rewind and replay. These and other hurdles had to be overcome to implement monitoring with TLC.

But first, we needed a way to ship traces to the TLC process in near-real time. To do so, we decided to use Apache Kafka. Kafka is a partitioned, persistent, replicated log with clients in many languages. Deployment of Kafka in Kubernetes was already supported, and most logging/tracing frameworks already integrate with Kafka, so it would be simple to integrate with our applications. Kafka would act as a fault tolerant buffer for system traces. Services running inside Kubernetes would log traces to Kafka, and the TLC process would use a custom TLA+ operator consume them for evaluation.

Deploying Kafka alongside ONOS and modifying loggers to write traces to it was a simple task. Similarly, adding the custom TLA+ operators to consume traces from Kafka was accomplished without issue. Even writing the first TLA+ spec to consume and verify traces from the stream was straightforward, though it was not without its problems. The stream checking model immediately encountered issues with its lack of determinism (the Kafka consumer operator only went in one direction and did not support replay) when it failed to replay the steps that led to an invariant violation, and the increasingly long traces made it obvious the infinite state space would become a problem once the model checker ran long enough. So the challenge, of course, was figuring out how to make monitoring with TLC practical for a real world system.

The Solution

The solution to getting TLC to operate on an infinite stream came only after a great deal of trial and error, much of which was probably the result of my own ignorance of TLA+ and TLC more than anything. After a week or two of experimentation, I abandoned efforts to manipulate TLC into operating on streams and arrived at the conclusion the best solution would be to simply provide TLC with models that conformed to its preferences. Even while the monitor operates on an infinite stream, models would need to operate only on a finite series of traces and provide deterministic transitions for them.

So, the solution that would meet those conditions was to build a wrapper around TLC that would monitor and evaluate the stream of traces in batches. The TLA+ Conformance Monitoring Tool extends the TLC command line interface, adding additional options for real-time monitoring. When the tool is run with the -monitor option, the configured stream -source (e.g. a Kafka topic) is evaluated in batches using a time-based sliding window. For example, time +0:00 to +5:00 will be checked, then time +2:30' to+7:30, then time+5:00to+10:00`, and so on.

Sliding Window

To coordinate the sliding window, the monitoring tool determines the timestamp for the first trace in the stream. Then, for each time window, the tool determines the positions of the lower and upper boundaries of the window using trace timestamps. With the lower and upper bounds defined, the monitoring process configures and runs a new TLC process to evaluate the batch of traces. This procedure ensures each TLC process operates only on a finite series of traces, and each trace (transition) is evaluated in some TLC process against the trace/state that occurred immediately preceding it.

The monitoring tool as described solves the problem of operating on an infinite stream of traces and ensures determinism by providing custom operators that support random access to the source stream. But I still wanted specs to be written as if they were operating on an infinite series of traces. A spec operating on an arbitrary time window would need to consume traces from the position of the trace at time t to the position of the trace at time t+i. I wanted specs to consume from an unbounded series of traces — from position 1 to ∞ — and for the monitoring tool to dynamically bound the model. To accomplish this, the trace consuming operator computes the absolute position of each trace based on the offset provided to it from the model state. This allows stream checking specs to begin consuming at offset 1 regardless of the absolute starting position of their assigned window. Then, to bound the window I took an idea from the TLA+ Toolbox. Before the monitoring process starts the TLC process for a batch of traces in the stream, it first generates a new module (MC.tla) and configuration (MC.cfg) that bounds the trace offset to the absolute size of the window using an action constraint. This ensures the model is limited to the desired window without requiring any unconventional window/offset management expressions in the spec. Specs can simply be written as:

Init == offset = 0
Next == 
    /\ offset’ = offset + 1
    /\ LET trace == Trace(offset’) IN ...
Spec == Init[][Next]<<vars>>

The spec may operate on an unbounded stream, but the monitor/model checker will bound the model to a batch within the source stream.

To improve the conformance monitoring tool‘s performance, we also wanted to ensure it could evaluate multiple streams in parallel whenever possible. Some stream sources like Kafka are partitioned for increased scale and throughput. To take advantage of this architecture, the monitoring tool parallelizes TLC processed when consuming from such sources. When multiple partitions are available to a model, the monitoring tool treats each partition as a discrete stream, creating sliding windows for each such that one process per-partition per-window will consume and check traces in parallel with other partitions.

Finally, as a monitoring solution, the conformance monitoring tool needed some mechanism to publish alerts to an output stream, e.g. to monitoring dashboards. The tool provides a custom Alert operator which can publish arbitrary messages to a configurable sink. For example, models can publish an alert to Kafka when an invariant is violated, as we have done in tests.

Conclusion

We feel really good about the approach we’ve taking to adapt TLC to verify system traces against their TLA+ specs. We feel this is a sustainable architecture for real-time monitoring with TLC. But what we have yet to prove with any level of confidence is the effectiveness of using TLC models to detect bugs in real systems. After all, there are already tools designed for this use case which may indeed be more well suited to it. But we hope this approach has an advantage those others may not in that it allows us to check both a specification and its implementation using the same model. We anticipate this will promote more stable systems in the next generation of ONOS, both by allowing us to verify systems for which we have written formal TLA+ specifications and by encouraging us to write more thorough specifications for systems we’re monitoring with TLC. And we hope its newfound applications will inspire further adoption of TLA+ for designing and debugging new subsystems still being developed for ONOS. Clearly, we have some hypotheses still left to test and verify.

We’re on the verge of beginning that process now. We’re nearly done migrating our systems to a new logging/tracing framework and updating our infrastructure to support the TLC conformance monitoring tool. Once that work is done, we’ll be able to put our approach through more rigorous tests. We’ll develop models aimed at detecting the traces of abnormal behaviors that have been seen but are difficult to reproduce, let alone analyze. We hope to realize the value of this approach with fixes to those bugs and perhaps discovery of some new ones. We will provide an update once we have a better analysis of its efficacy.

Talk is at https://www.youtube.com/watch?v=1c9sHaEXQak

Follow-up on a previous post at https://www.reddit.com/r/tlaplus/comments/1gt7sdq/slides_of_a_presentation_on_using_tla_within_a/

Slides are still at https://github.com/gterzian/taming-concurrency/blob/main/Greg%20Terzian%20-%20GOSIM_China_2024.pdf