tlaplus

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

Friendly reminder that the meeting is scheduled for four hours from now. We'd welcome your

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

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.

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

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

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

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

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

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

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

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

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

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

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

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

The best way to answer these questions is to understand the TLA+ specification that corresponds to a

I mostly use neovim to write TLA+, with the tree-sitter-tlaplus grammar for highlighting. Syntax

Thank you for your thorough review. I agree with most of your comments. The links have been fixed in

Thank you to everyone who joined the presentation! The recording is available here. On Tuesday,

> On Sep 25, 2025, at 7:58 PM, Shane Miller <gshane...@gmail.com> wrote: > > Hello