Groups

tlaplus

Contact owners and managers

1–30 of 1624

This is a discussion group for users of the TLA+ specification language, the PlusCal algorithm language, and their associated tools.
To find out about the languages and tools, see The TLA Home Page

Posts by non-members are moderated.

We encourage you to join the group.

0 selected

Markus Alexander Kuppe

10:30 AM

TLA+ Debugger: Interactive State-Space Exploration

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

unread,

TLA+ Debugger: Interactive State-Space Exploration

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

10:30 AM

Gregory Terzian, Stephan Merz2

Jan 7

Presentation for the next community meeting

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

unread,

Presentation for the next community meeting

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

Jan 7

marta zhango, Stephan Merz2

Jan 3

Font dependency specification

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

unread,

Font dependency specification

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

Jan 3

tal...@gmail.com, Kant Seemee2

Jan 2

Experience proving liveness with TLAPS

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

unread,

Experience proving liveness with TLAPS

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

Jan 2

Lorin Hochstein, Andrew Helwer4

Jan 2

\subseteq vs \in SUBSET

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

unread,

\subseteq vs \in SUBSET

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

Jan 2

Taylor Waggoner, … Andrew Helwer3

12/30/25

Join us at the next TLA+ Outreach Committee meeting on December 18

Summary of the meeting this month; thank you to Taylor Waggoner for taking detailed notes: It was

unread,

Join us at the next TLA+ Outreach Committee meeting on December 18

Summary of the meeting this month; thank you to Taylor Waggoner for taking detailed notes: It was

12/30/25

Ivanov Dmitriy, Andrew Helwer3

12/19/25

Redundancy in states dump

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

unread,

Redundancy in states dump

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

12/19/25

12/19/25

Code conformance yet again, this time with SMT

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

unread,

Code conformance yet again, this time with SMT

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

12/19/25

12/15/25

TLA+ Community Meeting 2026

A TLA+ Community Meeting will be organized as a satellite of ETAPS 2026 (https://www.etaps.org/2026/)

unread,

TLA+ Community Meeting 2026

A TLA+ Community Meeting will be organized as a satellite of ETAPS 2026 (https://www.etaps.org/2026/)

12/15/25

Jaco van de Pol

12/13/25

Fully funded PhD and Postdoc in Quantum Software, Aarhus, Denmark

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

unread,

Fully funded PhD and Postdoc in Quantum Software, Aarhus, Denmark

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

12/13/25

Miguel Raz-Guzmán Macedo, Andrew Helwer3

11/30/25

Can the VSCode TLA+ extension do Unicode autocomplete?

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

unread,

Can the VSCode TLA+ extension do Unicode autocomplete?

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

11/30/25

Younes, William Schultz2

11/27/25

TLA+ repo on Google CodeWiki?

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

unread,

TLA+ repo on Google CodeWiki?

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

11/27/25

Quentin DELAMEA, … Stephan Merz10

11/27/25

Prove properties of the form [](P => []P) with TLAPS

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

unread,

Prove properties of the form [](P => []P) with TLAPS

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

11/27/25

王圣予, … Irwansyah Irwansyah4

11/26/25

Looking for Guidance on Getting Started with TLA+: Tips for a New Learner

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

unread,

Looking for Guidance on Getting Started with TLA+: Tips for a New Learner

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

11/26/25

Mathew Kuthur James, … Andrew Helwer5

11/26/25

Rules for writing formulae with primed variables

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

unread,

Rules for writing formulae with primed variables

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

11/26/25

Dave Hughes, … Markus Kuppe9

11/24/25

Science of Concurrent Programs: 3.4.1.4 Error in Composition?

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

unread,

Science of Concurrent Programs: 3.4.1.4 Error in Composition?

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

11/24/25

Chris Ortiz, … Stephan Merz4

11/24/25

What is the plan for Distributed PlusCal?

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

unread,

What is the plan for Distributed PlusCal?

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

11/24/25

Dave Hughes, Andrew Helwer2

11/22/25

Question about Science of Concurrent Programs: Status

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

unread,

Question about Science of Concurrent Programs: Status

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

11/22/25

Chris Ortiz, … dbah...@gmail.com13

11/19/25

Aside from WF and SF?

All, I have been studying this hugely valuable work for a month or two now – and I am wondering about

unread,

Aside from WF and SF?

All, I have been studying this hugely valuable work for a month or two now – and I am wondering about

11/19/25

11/13/25

Presentation of the TLAi+ Challenge Winning Project – Specula

The winners of the 1st TLA+ GenAI Challenge [1] presented their winning submission, Specula [2], at

unread,

Presentation of the TLAi+ Challenge Winning Project – Specula

The winners of the 1st TLA+ GenAI Challenge [1] presented their winning submission, Specula [2], at

11/13/25

Dylan Zueck, Stephan Merz3

11/12/25

Proving an action leads to a temporal formula

Thanks! I was thinking something along those lines would work, the only issue with that is that in my

unread,

Proving an action leads to a temporal formula

Thanks! I was thinking something along those lines would work, the only issue with that is that in my

11/12/25

Chris Ortiz, … Markus Kuppe6

11/7/25

Will there be a lesson learned on AWS 2025 East-1 Outage due to DynamoDB with regards to TLA+?

Thank you all for sharing. Murat's TLA+ spec is really cool, and also cool is the Spectacle

unread,

Will there be a lesson learned on AWS 2025 East-1 Outage due to DynamoDB with regards to TLA+?

Thank you all for sharing. Murat's TLA+ spec is really cool, and also cool is the Spectacle

11/7/25

Weining Cao, … Igor Konnov3

11/3/25

Discussion: Apalache found counter-example for invariant that was claimed proved via TLC→TLAPS

Hi Weining Cao, Seconding what Stephan wrote. The most important question is whether the

unread,

Discussion: Apalache found counter-example for invariant that was claimed proved via TLC→TLAPS

Hi Weining Cao, Seconding what Stephan wrote. The most important question is whether the

11/3/25

Ugur Yavuz, … Ugur Y. Yavuz3

11/1/25

Initializing local variables in PlusCal

Yes, that's what I saw in the manual as well, but I was a bit surprised there wasn't any

unread,

Initializing local variables in PlusCal

Yes, that's what I saw in the manual as well, but I was a bit surprised there wasn't any

11/1/25

Dylan Zueck, … Markus Kuppe3

10/28/25

Checking that a specific path is always possible to take

Interrupt cannot occur at any time in your example specification because you restricted Interrupt to

unread,

Checking that a specific path is always possible to take

Interrupt cannot occur at any time in your example specification because you restricted Interrupt to

10/28/25

Rostislav Nikitin

10/26/25

Re: [tlaplus] Digest for tlaplus@googlegroups.com - 2 updates in 1 topic

Hello Stephan. Thank for your answer. Yep, you are absolutely right. Yesterday I found this article:

unread,

Re: [tlaplus] Digest for tlaplus@googlegroups.com - 2 updates in 1 topic

Hello Stephan. Thank for your answer. Yep, you are absolutely right. Yesterday I found this article:

10/26/25

Rostislav Nikitin, Stephan Merz2

10/25/25

Temporal property unexpectedly fails

A TLA+ specification Init /\ [][Next]_vars allows for behaviors that end in infinite stuttering after

unread,

Temporal property unexpectedly fails

A TLA+ specification Init /\ [][Next]_vars allows for behaviors that end in infinite stuttering after

10/25/25

Shane Miller, Andrew Helwer3

10/23/25

Checking temporal properties (2 quick questions)

Thank you for your reply On Thu, Oct 23, 2025, 4:07 PM Andrew Helwer <andrew...@gmail.com>

unread,

Checking temporal properties (2 quick questions)

Thank you for your reply On Thu, Oct 23, 2025, 4:07 PM Andrew Helwer <andrew...@gmail.com>

10/23/25

Markus Kuppe, Hillel Wayne2

10/14/25

Towards a migration guide: TLA+ Toolbox → TLA+ VSCode extension

I need to rewrite learntla to use vscode, but might be a bit before I can get to that. If this

unread,

Towards a migration guide: TLA+ Toolbox → TLA+ VSCode extension

I need to rewrite learntla to use vscode, but might be a bit before I can get to that. If this

10/14/25

Ugur Yavuz, Stephan Merz2

10/10/25

The Naturals module

I don't know why that module was changed in the distribution [1] with respect to the presentation

unread,

The Naturals module

I don't know why that module was changed in the distribution [1] with respect to the presentation

10/10/25

Search

Clear search

Close search

Google apps

Main menu