tlaplus

https://lamport.azurewebsites.net/tla/learning.html https://learntla.com/ Andrew On Fri, Mar 20, 2026

In the first way to model a network, message loss is not a possibility whereas in the second it is.

Hi Marta, If you'd like, we can set up a video call to chat about your interest in TLA+ and what

After checking in with the actual experts, I realized there's a different link to share re: TLA+

I figured this out. The clue was from the SubstInNode, which SANY uses to wrap expressions from

Ambareesh, Thank you for taking time and reaching out! >How would you prefer the feedback

Using TLA+ to Fix a Very Difficult glibc Bug - Malte Skarupke - C++Now 2025 The glibc condition

Hi Filip, I am very glad to hear that. I am looking forward to your email and to collaborate with you

Thanks Markus. I reviewed the link and that is actually a cool feature and I would like to try it out

> I don't recall if you can put a `goto` inside a macro, Unfortunately you can't.

I agree with Hillel on the answer to the first question. I also agree on his second answer. Just to

Thanks, Stephan! Wow, after all these years parsing TLA+ I am still learning about new corners of the

The list of presentations accepted for the Community Meeting is now online at https://conf.tlapl.us/

It is really cool when you demo'd it to us during the outreach meeting. It is even accessible on

My question was not clear. Suppose one is writing a user or technical guide for TLA. For absolute

Hi Hank Wang, You can find the TLA+ specifications from the book in the examples repository [1]. The

Now that I'm more familiar with how SANY works I might be able to answer this in greater detail.

Hi everyone, we'd like to invite the TLA+ community to check out and contribute to a new

For a discussion about functions vs. operators, see section 6.4 of Specifying Systems. As I should

Thank you very much, Stephan, Indeed it looks like I was thinking too much like a programmer, your

(Cross-posting from subreddit) I ran a small experiment in transpiling TLA+ directly to C++ using

Thanks, Stephan! I guess that makes ENABLED a fairly unique operator. Every other operator either

Hi, Apalache has a number of expression simplifications that rewrite constraints over cardinalities

Adding to Andrew's answer, TLC expects the first occurrence of a primed variable v' in an

Apologies I missed the first meetings. I am surfacing from a deep dive and look forward to upcoming

Hi everyone, The TLA+ Debugger has a new major capability: **interactive state-space exploration**.

Hi Gregory, your presentation during the community meeting is confirmed for next Tuesday (January 13,

How about using a record for representing a font attribute, with the set of all such records defined

A very interesting read! Thanks for documenting the issues you ran into with TLAPS. On Thursday,

Just for fun I hacked together an implementation of this by combining the logic of the SUBSET and \in