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

Amazon's 2022 paper, “Amazon DynamoDB: A Scalable, Predictably Performant, and Fully Managed

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

> On Sep 26, 2025, at 3:54 AM, Andrew Helwer <andrew...@gmail.com> wrote: > > Wow,

I am similarly confused for the same reasons. -dfid num run the model check in depth-first iterative

Unfortunately that email no longer works. It bounced back to me. I found the lecture series to be

Thanks Andrew, I am testing out using scaled values. On Tue, 2 Sept 2025, 23:59 Andrew Helwer, <

August 2025 update: GenAI challenge winners announced, a startup paying people to write TLA⁺ spec

Hello, there are very few examples of liveness proofs so far. Essentially you want to do an induction

🏆 Announcement: Winners of the 2025 TLAi+ Challenge The TLA+ Foundation, in collaboration with NVIDIA

I found myself needing to do something very similar: I'm working on something where I need to

Hi Basant, TLA+ certainly can accomplish all of your goals, although it should be noted that it

Hi, for your information, the ProB tool can also handle some TLA+ specifications. It works on the

We also wrote a bit about our recent experiences applying model-based test case generation to

And thanks Markus, That was very useful. It confirms the same answer. Thank you for pointing that out

============================================================== CONFEST 2025: 2nd Call for

I've been thinking a lot about custom tooling workflows in the context of TLA+ recently. As a

Thanks for sharing. I enjoyed the article and think it makes a lot of great points. On Sun, Jul 13,

Hi Andrew, Your answer reflects your vision on the future of TLA+. I don't know what your vision