Hello TLA+ community, Taylor Waggoner at the Linux Foundation suggested that this mailing list would

Hello Stephan, thank you for the information. I have to check for accessible web sites. Best,

Ah, easy enough. I guess I glossed over the command palette piece...this is now working well. Thanks!

I'm working on a research spec called SynodEnergy, which extends classical Paxos (Synod) with an

Hello, Small correction to my previous update: the published release tag is `1.0`, not `v1.0`.

One of my experiments was to define a formula Equiv == (Spec1 <=> Spec2) in the .tla file and

A friendly reminder that the next Outreach Committee meeting [1] will start in about 30mins at 8:00

Hi Neil, Thank you for the sharp critique — these are important points worth addressing. On “horribly

Thank you for all who had interest. I sent the writing through private messaging. Adding some more

Thank you Stephan Le jeudi 9 juillet 2026 à 13:42:27 UTC+1, Stephan Merz a écrit : Unless there are

Hi Neil, having to decide between two different techniques for formal verification may be seen as a

Super nice! I bet it's going to be a meme in the future, Zed is just like OCaml will too. They

Hi , Anyone interested in Formal Verification/Analysis of Web/Network Protocols from a security/

- Did you assume that CASE expressions evaluated their branches sequentially? Yes, I assumed they

Also at https://conf.tlapl.us/2012/ > On Jun 8, 2026, at 3:19 AM, Alex Hajjar <alexandre.hajjar

Hi Shane, Thank you for your response! If I have a correct understanding: BFS construction and

This is a quick note that the examples in: https://github.com/gshanemiller/tla-examples together with

There is also this somewhat classic blog post about package manager design, which is now old enough

It was a while ago, but I did read through it, and I thought it was worth it. One thing I took away

Hi all, Our monthly TLA+ Community Call is happening now. Please join us at https://zoom-lfx.platform

The videos of the presentations at the meeting in Torino are now online at https://www.youtube.com/

An interesting reference what others are discussing : https://github.com/rust-lang/leadership-council

Unless you want TLC!RandomElement to bias successor selection with a custom (rational) distribution,

You can post these questions to this mailing list. Andrew On Fri, May 1, 2026 at 11:31 AM 'TT

Hi Stephan, Thanks again for your feedback and comments! Apologies for the delayed response. I wanted

I'd love to, but I'm not sure how much time I can dedicate to it right now. I'm currently

I have something to contribute to the implementation question. I have done some experimentation with

There are no real differences between P and C PlusCal except for the start/end block syntax. I

Mr. Suckrow, Consider reading the pdf in https://github.com/gshanemiller/tla-examples. The RPC

Ah that is a good spot, I will have to update the XML Exporter documentation. Thanks! Andrew On Mon,