tlaplus

===================================== CONFEST 2025: Call for Participation https://conferences.au.dk/

> 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 Ognjen! I'm leaving this in my inbox until I have some more time to read and think and follow

June 2025 update: AI contest submission deadline is July 4th, Spectacle gets GraphViz animation

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

The TLA+ Foundation, in collaboration with NVIDIA, is pleased to announce the GenAI-accelerated TLA+

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

For anyone else with the same questions, these guys did a machine checked proof of Vertical Paxos in

> it's possible they could be defined over a non-abelian group where this leads to unexpected

Hello Stephan, thanks a lot for your quick answer. I appreciate your patients and time to ramp up

Again, it seems to me that the assumption runningTask # “” can be removed because it is redundant

Hello, Regarding point 2 and in particular for the Raft spec. The original spec is just hard to model

Early registration is ending on April 1st so it is good to book within the next few days if you want

Final Call for Papers CONCUR 2025 https://conferences.au.dk/confest2025/concur This is the final CFP

Got it. It worked. Much appreciated On Friday, March 21, 2025 at 11:37:06 AM UTC-4 Hillel Wayne wrote

You're absolutely right. Thank you for pointing that out! I've corrected it, and I was able

Hello! This is mainly a question for Markus Kuppe and Jack Vanlightly, but I'll ask in public for

Yup! Thank you! Works fine Spec == Init /\ [][Next]_vars /\ SF_vars(initial /\ pc'["Job