Here are two posts I published recently about TLA+:
I look at how well PlusCal works as a pseudocode replacement, taking the case study of a string algorithm paper published in 1980 that contained bugs in its pseudocode. It was for this post that I was spamming up this group last week with questions about proofs. I didn't end up writing a proof for this algorithm because I figured it was extremely complicated and would have taken about two weeks, but I'm glad I finally learned how to write TLA⁺ proofs (it's been a goal for nearly a decade!). I also compared the TLA⁺ proof language to the Lean proof language. I wonder how much of the Lean user experience could be transferred to the TLA⁺ proof language UX.
Report about an experience with TLA⁺ use on the Microsoft Azure DNS team, with a now-open-sourced spec. The model checker found an interesting 12-step error trace in the proposed design. It also talks about the experience of implementing actual code following a TLA⁺ spec.
Hope you enjoy!
Andrew Helwer