Monthly Development Update newsletter

252 views
Skip to first unread message

Andrew Helwer

unread,
Dec 17, 2024, 2:25:23 PM12/17/24
to tlaplus
Hello all,

As part of work funded by the TLA+ Foundation I have written up a newsletter on various community developments over the past month or two. This is hoped to be a monthly publication. Here is the post for December 2024: https://foundation.tlapl.us/blog/2024-12-dev-update/index.html

Since this is the first newsletter published it's inevitable I missed some things; so if you wrote a blog post about TLA+ or made a contribution to the TLA+ tools that I missed or are working on a side-project of your own related to TLA+, please let me know by replying directly to me in this thread or opening an issue here! No need to be humble or shy.

Andrew Helwer

Andrew Helwer

unread,
Jan 17, 2025, 10:39:17 AMJan 17
to tlaplus
The January 2025 edition has now been posted: https://foundation.tlapl.us/blog/2025-01-dev-update/index.html

Andrew Helwer

unread,
Feb 16, 2025, 2:54:26 PMFeb 16
to tlaplus
The February 2025 edition has now been posted: https://foundation.tlapl.us/blog/2025-02-dev-update/

Andrew Helwer

unread,
Mar 17, 2025, 2:32:37 PMMar 17
to tlaplus
March TLA+ development update: a bad month for tuple-except expressions, another formal methods use paper from AWS after 10 years, a new TLA+ formatter written in Rust, and more!

https://foundation.tlapl.us/blog/2025-03-dev-update/

Andrew Helwer

unread,
Apr 15, 2025, 1:14:46 PMApr 15
to tlaplus
April 2025 update: creator of P specification language joins the board, a new TLA+ parser written in Python, two first-time contributors, and a PlusCal transpilation bug featured in the newbie corner!

Message has been deleted

Andrew Helwer

unread,
Jun 15, 2025, 12:01:40 PMJun 15
to tlaplus
May 2025 update: TLA⁺ Community Event talk recordings posted, a contest with a NVIDIA RTX 5090 as the grand prize, GraalVM native image builds, and a big focus on improving usability this month.

Andrew Helwer

unread,
Jun 15, 2025, 12:05:07 PMJun 15
to tla...@googlegroups.com
June 2025 update: AI contest submission deadline is July 4th, Spectacle gets GraphViz animation support, VS Code extension gets MCP support, and a new research grant for synthesizing inductive invariants!


Also seeking volunteers to help expand this newsletter with various features, as suggested by the Outreach Committee:
  • Monthly feature from industry adopters on recent TLA⁺ success stories
  • Monthly featured TLA⁺-related academic paper of the month
  • Monthly analysis of TLC usage statistics

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/5326e424-cb35-4f4b-b98c-51cb45c205bdn%40googlegroups.com.

Andrew Helwer

unread,
Jul 21, 2025, 2:52:39 PMJul 21
to tla...@googlegroups.com
July 2025 update: GenAI challenge submission deadline passed, TLAPM updated to use Isabelle 2025, TLA+ proofs fixed, critical chapter published on guide to writing your own TLA+ modelchecker!


Still seeking a volunteer to help expand the newsletter with a monthly highlighted academic paper that uses TLA+ - can be historical!

Andrew Helwer

unread,
Aug 20, 2025, 12:10:52 PMAug 20
to tla...@googlegroups.com
August 2025 update: GenAI challenge winners announced, a startup paying people to write TLA⁺ spec examples, and efforts to make the tools less file-dependent!

https://foundation.tlapl.us/blog/2025-08-dev-update/index.html
Reply all
Reply to author
Forward
0 new messages