------------------------------------------------------------------ FRIDA @ POPL 2027 - 13th Workshop

Hi TLA+ Foundation and Stephan, I forgot to follow up last April for what is the plan to integrate

Thanks, Taylor, for driving this. If you use or contribute to TLA+, please take a few minutes to fill

Hello Stephan, thank you very much, this is indeed helpful. TLC gives a warning when combining

Hello to all, receiving a success message from TLC for a spec I wrote was confusing. I was sure a

Again, thank you very much, Markus. This is very interesting. On Monday, September 28, 2026 at 9:38:

Surprisingly (or unsurprisingly, depending on how much of Lamport's writing you've read) the

Hey Andrew, I briefly met you grabbing a coffee at the hotel waiting for the Software Should Work

Hello TLA+ user group! I'd like to share my latest little use case for our favorite formal

Hello, using an environment action together with a suitable (probably weak) fairness hypothesis

I find a forum interface more conducive to finding the most relevant topic/discussion without adding

Hello TLA+ community, A brief technical update since my World 7 v0.2 note: the architecture has now

Hi all, I posted a longer version of this a couple of weeks ago that didn't get much traction — I

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