Issues

• Yices backend: yices -tc is given SMT-LIB 2 with logic UFNIA, which Yices 2 rejects

  wontfix
  tlaplus/tlapm#313 · Filter by author arvindcr4 opened on Oct 25, 2026
  1

• Zipper: later obligation gets an empty THF file after an earlier set-theory Zipper obligation

  translator
  tlaplus/tlapm#312 · Filter by author arvindcr4 opened on Oct 25, 2026
  1

• Spass/Tptp backends receive SMT-LIB instead of TPTP FOF with the default encoder

  wontfix
  tlaplus/tlapm#311 · Filter by author arvindcr4 opened on Oct 25, 2026
  1

• Soundness: abstracted terms and LS4 atoms are named by 20 bits of a hash with no collision check, and the hashed print does not distinguish a bound variable from a constant of the same name

  bugsoundness
  tlaplus/tlapm#310 · Filter by author scottcochran opened on Oct 18, 2026

• Soundness: a term under a binder that tlapm does not translate is abstracted as a nullary constant, so false theorems prove

  soundness
  tlaplus/tlapm#309 · Filter by author scottcochran opened on Oct 18, 2026

• Old SMT encoding proves false equalities between CASE expressions

  bugsoundness
  tlaplus/tlapm#306 · Filter by author lemmy opened on Oct 14, 2026
  2

• Enable private vulnerability reporting

  tlaplus/tlapm#305 · Filter by author NoneSilva opened on Oct 13, 2026
  1

• SMT soundness: overlapping CASE arms are lowered to ordered IF

  bugsoundness
  tlaplus/tlapm#304 · Filter by author McHersheys opened on Oct 13, 2026
  2

• Integer exponentiation with negative exponents

  soundness
  tlaplus/tlapm#300 · Filter by author agouglidis opened on Oct 4, 2026

• Equivalence of common operators in parent and instantiated modules

  tlaplus/tlapm#298 · Filter by author Calvin-L opened on Oct 2, 2026

• Proof fails depending on surrounding unrelated context

  tlaplus/tlapm#291 · Filter by author letFunny opened on Sep 7, 2026
  2

• Feature request: CLI flag to filter obligations by lemma/theorem name, not line number

  enhancement
  tlaplus/tlapm#290 · Filter by author Calvin-L opened on Aug 31, 2026

• tlapm scales poorly on INSTANCE/refinement-heavy specs (large per-obligation contexts)

  tlaplus/tlapm#286 · Filter by author qdelamea-aneo opened on Jul 27, 2026
  6

• --line should fail when no proof obligation is selected

  enhancement
  tlaplus/tlapm#276 · Filter by author lemmy opened on Jun 7, 2026

• Learnings AI+TLAPS (TLAiPS)

  documentation
  tlaplus/tlapm#272 · Filter by author lemmy opened on May 14, 2026
  5

• tlapm ending abnormally with File "src/expr/e_levels.ml", line 933, characters 12-18: Assertion failed

  bug
  tlaplus/tlapm#270 · Filter by author lemmy opened on May 14, 2026
  2

• tlapm ending abnormally with Tlapm_lib__Util.Internal_timeout

  tlaplus/tlapm#269 · Filter by author lemmy opened on May 13, 2026
  1

• LSP: Proof decomposition should push ' down

  enhancement
  tlaplus/tlapm#261 · Filter by author kape1395 opened on Apr 15, 2026
  

• New warning ld: warning: ignoring duplicate libraries: '-lc++', '-lpthread'

  tlaplus/tlapm#259 · Filter by author ahelwer opened on Apr 13, 2026

• TLAPM library modules depend on community modules

  tlaplus/tlapm#252 · Filter by author ahelwer opened on Mar 1, 2026
  2

• Can't solve even when conclusion matches assumption exactly

  tlaplus/tlapm#247 · Filter by author talex5 opened on Dec 19, 2025
  3

• When run from a different directory, TLAPM cannot handle leading text on modules imported using EXTENDS

  syntax parser
  tlaplus/tlapm#245 · Filter by author ahelwer opened on Dec 16, 2025

• Tuple quantification should not be supported in ASSUME NEW <<x, y>> \in S statements

  bugsyntax parser
  tlaplus/tlapm#242 · Filter by author ahelwer opened on Oct 31, 2025
  2

• TLAPM parser incorrectly allows LAMBDA as expression

  bugsyntax parser
  tlaplus/tlapm#238 · Filter by author ahelwer opened on Sep 4, 2025

• TLAPM parser incorrectly accepts recursive operator when it is a function literal

  bugsemantic checkersyntax parser
  tlaplus/tlapm#237 · Filter by author ahelwer opened on Sep 4, 2025