tlaplus

Very exciting! Been wanting to make something like the Lean Natural Number Game but for TLA+ for a

Deciding what fairness conditions it is reasonable to assume requires experience. A typical example

The next TLA+ Outreach Committee meeting is scheduled for today, Thursday, February 19, at 11:00 am

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

A gentle reminder that we'd love to receive your proposals for presentations at the Community

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

Correction: the state cardinality is |Boxes| * |Observed_Boxes| * |{"left", "right

Hi, I've realized that some of you on this list may be not reading social networks. So I've

We offer several fully funded PhD and Postdoc positions in Quantum Software (verification,

Deal :) First typescript PR ever, so if anyone can help get it over the finish line I'd

FYI there is already a DeepWiki for the tlaplus code repo: https://deepwiki.com/tlaplus/tlaplus On

Understood, thank you very much! On Thursday, November 27, 2025 at 10:47:10 AM UTC+1 Stephan Merz

1. Start with the mindset of modeling a discrete system 2. A discrete system has a state in each

Nope, you can use the primed variables as many times as you want. This is a way of writing

The pull request https://github.com/tlaplus/tlaplus/pull/805 mentions the limitation of the current

Hi Stephan, Yes I am very interested. In fact, I am working on a side project with our univerisity

Lamport is retired retired, so there is currently no public way to contact him and report errors.