Issues

• Align TLA+ trifecta: Apalache, TLAPM, and TLC on a shared resolution of CASE semantics

  enhancementquestion
  tlaplus/rfcs#26 · Filter by author lemmy opened on May 22, 2026
  8

• Proposal: remove multi-line strings from the language

  tlaplus/rfcs#25 · Filter by author ahelwer opened on May 21, 2025
  5

• Provide the content of https://lamport.azurewebsites.net/tla/tla2-guide.pdf in a more accessible, web-friendly format

  documentationenhancementhelp wanted
  tlaplus/rfcs#24 · Filter by author lemmy opened on May 14, 2025
  5

• Adopting changes to the TLA+ language and standard modules

  tlaplus/rfcs#21 · Filter by author muenchnerkindl opened on Mar 10, 2025

• Proposal: Remove []ASSUME/[]PROVE construct from the language

  tlaplus/rfcs#20 · Filter by author ahelwer opened on Feb 27, 2025
  3

• Proposal: remove decimal syntax with no leading zero from language (.1234)

  tlaplus/rfcs#19 · Filter by author ahelwer opened on Feb 10, 2025
  3

• Proposal: remove INSTANCE and BY MODULE proof types from language

  tlaplus/rfcs#18 · Filter by author ahelwer opened on Feb 6, 2025

• Proposal: standardize allowing multiple sequential modules in a file

  tlaplus/rfcs#17 · Filter by author ahelwer opened on Dec 29, 2024
  7

• Proposal: Standardize human-usable error codes for reference & testing

  tlaplus/rfcs#15 · Filter by author ahelwer opened on Nov 25, 2024
  3

• Proposal: add tuple destructuring definition in LET/IN blocks

  tlaplus/rfcs#14 · Filter by author ahelwer opened on Nov 18, 2024
  2

• Proposal (PlusCal): action keyword to write any TLA+ expressions WITHOUT generating an UNCHANGED statement.

  enhancement
  tlaplus/rfcs#12 · Filter by author lemmy opened on Jul 1, 2024
  1

• Proposal: allow Unicode alternatives for module delimiters

  tlaplus/rfcs#11 · Filter by author ahelwer opened on Jun 15, 2024

• Proposal: combine set filter and set map language constructs

  tlaplus/rfcs#10 · Filter by author ahelwer opened on May 8, 2024
  10

• Support |S| as alternative to Cardinality(S)

  enhancement
  tlaplus/rfcs#9 · Filter by author lemmy opened on Apr 26, 2024
  11

• Proposal to add Unicode support to the TLA+ language standard and tools

  enhancement
  tlaplus/rfcs#5 · Filter by author ahelwer opened on Oct 6, 2021
  9

• Remove CHOOSE and recursive operators from TLA+ in favor of new FoldSet language primitive

  wontfix
  tlaplus/rfcs#3 · Filter by author lemmy opened on Jun 29, 2021
  1

• [tool] Pretty Print to HTML

  enhancement
  tlaplus/rfcs#2 · Filter by author lemmy opened on May 25, 2021
  5