Issues

• TLC can miss states due to unnormalized action arguments

  bugsoundness \/ completenessTools
  tlaplus/tlaplus#1445 · Filter by author emilie-oai opened on Sep 23, 2026
  4

  

• Counterexamples differ when using -recover (-workers, -fp, -seed must match the original run)

  enhancementTools
  tlaplus/tlaplus#1444 · Filter by author llamerada-jp opened on Sep 23, 2026
  3

• Warn when TLA+ specifications directly use TLC!Assert

  enhancementSANY
  tlaplus/tlaplus#1437 · Filter by author lemmy opened on Sep 15, 2026
  1

• Parser rejects a RECURSIVE definition of the prefix -. operator applied to itself

  bugSANY
  tlaplus/tlaplus#1418 · Filter by author glondu opened on Sep 9, 2026
  2

  

• XML Exporter (and possibly SANY's semantic model) drops the containment relationship between a module and a module nested in its body

  tlaplus/tlaplus#1410 · Filter by author glondu opened on Sep 2, 2026
  

• SANY throws while formatting a level error for %

  bugSANY
  tlaplus/tlaplus#1406 · Filter by author konnov opened on Aug 25, 2026
  1

• Rev Release on JAR change

  tlaplus/tlaplus#1399 · Filter by author parsnips opened on Aug 7, 2026
  1

• Feature request: TLC should accept named theorems as properties & invariants

  tlaplus/tlaplus#1394 · Filter by author ahelwer opened on Jun 8, 2026

• Feature request: TLC should accept [] properties for INVARIANT

  tlaplus/tlaplus#1393 · Filter by author ahelwer opened on Jun 8, 2026

• TLC Parser throws NullPointerException on ARM64 (Raspberry Pi 5, aarch64)

  tlaplus/tlaplus#1392 · Filter by author dlukt opened on May 23, 2026

• Recursive operators cannot be used to define a property

  enhancementTools
  tlaplus/tlaplus#1389 · Filter by author craft095 opened on May 15, 2026
  7

• TLC -continue reports success despite invariant violations

  soundness \/ completenessTools
  Bug

  tlaplus/tlaplus#1385 · Filter by author younes-io opened on May 3, 2026
  1

• Different message codes for different messages

  enhancementToolsusability
  tlaplus/tlaplus#1382 · Filter by author craft095 opened on Apr 27, 2026
  1

• Version 1.8 reported as damaged when trying to execute Apple Silicon version

  Toolbox
  tlaplus/tlaplus#1381 · Filter by author pautib opened on Apr 26, 2026
  1

• Feature request: SANY should automatically include root spec directory in search path

  tlaplus/tlaplus#1372 · Filter by author ahelwer opened on Apr 5, 2026

• VIEW with SYMMETRY depend on variable naming.

  tlaplus/tlaplus#1368 · Filter by author marco6 opened on Apr 1, 2026

• TLC: replace generic/runtime failures with structured, source-aware diagnostics

  enhancementrefactoringTools
  tlaplus/tlaplus#1363 · Filter by author younes-io opened on Mar 25, 2026
  2

• Simulation trace length statistics are incorrect

  Tools
  tlaplus/tlaplus#1357 · Filter by author apurtell opened on Mar 19, 2026 · 1.8.0
  1

• TLC fails to evaluate ENABLED (x') when the body of ENABLED is a primed variable

  bugTools
  tlaplus/tlaplus#1336 · Filter by author lemmy opened on Mar 3, 2026
  2

• Noteworthy commits, issues, and pull requests not announced or back-ported to 1.7 maintenance branch

  tlaplus/tlaplus#1332 · Filter by author lemmy opened on Feb 25, 2026
  1

• Flaky unit test in tlc2.tool.DumpLoadTraceTest

  bugDevEnvironmentTools
  tlaplus/tlaplus#1325 · Filter by author ahelwer opened on Feb 23, 2026 · 1.8.0
  2

• Feedback & updates to the XML output format from TLAPM work

  refactoringSANY
  tlaplus/tlaplus#1313 · Filter by author ahelwer opened on Feb 16, 2026

• We need to update current-tools.md

  DevEnvironmentenhancementTools
  tlaplus/tlaplus#1311 · Filter by author hwayne opened on Feb 14, 2026
  1

• Add compact output mode to XMLExporter.

  AIenhancementhelp wantedTools
  tlaplus/tlaplus#1299 · Filter by author lemmy opened on Feb 3, 2026

• Include tlc2.REPL class in upcoming stable release

  tlaplus/tlaplus#1272 · Filter by author goyalyashpal opened on Jan 2, 2026
  4