tlaplus

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

I forgot to mention that there is also a simple way to produce TLA+ specs without going via the whole

Yes, the paper that Finn linked to, "Smart Casual Verification of the Confidential Consortium

> sense since refinement is fundamentally a liveness property, > I don't know if it makes

Dear All, note that the VTSA 2025 summer school will have a strong TLA+ flavor this year! Please

Hi Andrew and everyone, Thanks a lot for the feedback. I thought my first spec was so dumb so no one

Hi all, Let say someone wants to build a donation site for live streamer where users can send money

Just notifying, this is fixed now. Thanks Amanda! (turns out her "hey I fixed it" reply was

Reachability properties are not directly expressible in TLA, but we can cheat and say that `~

(some clarification!) The foundation isn't funding me to work on this, it's just for fun on

Terrific, thanks so much Markus. On Tue, May 20, 2025 at 12:34 PM Markus Kuppe <tlaplus-google-

Hi Erick, It may become less confusing if you know that omitting the name of the step makes the

TLA+ has a syntax for naming sub-formulas of a big formula, see [1]. For example, the n-th conjunct

'will do, thank you! On Wednesday, May 14, 2025 at 10:41:50 AM UTC-4 Andrew Helwer wrote: Please

Does your module include "EXTENDS TLAPS"? Stephan On 13 May 2025, at 18:42, Francisco José

Another way of trying to explain what I am doing is: I am trying to figure out the minimum number of

This is my first time writing a spec and I have used AI tool for some, I wanted to make sure the spec

I have realized that defining axioms with equivalence provides both axioms for a logic as well as