Issues

• arrays encoding reports a spurious invariant violation: element chosen from a set of records has a value that was never added

  bugtriaged
  apalache-mc/apalache#3493 · Filter by author sjmurdoch opened on Oct 4, 2026
  3

• Use LongMap to map UIDs

  optimizationrefactoring
  apalache-mc/apalache#3486 · Filter by author konnov opened on Sep 21, 2026

• Rename getCdm to getRel

  refactoring
  apalache-mc/apalache#3483 · Filter by author konnov opened on Sep 7, 2026
  

• Unsound LazyEquality over function sets with empty domains or co-domains

  bug
  apalache-mc/apalache#3477 · Filter by author konnov opened on Aug 28, 2026
  7

  

• Bind the explorer JSON-RPC server to loopback by default

  featureFserver
  apalache-mc/apalache#3459 · Filter by author konnov opened on Aug 18, 2026
  

• Spurious counterexample for [f \in S |-> Gen(1)] when S contains a Gen key (no error with --smt-encoding=arrays)

  bug
  apalache-mc/apalache#3449 · Filter by author Marghrid opened on Aug 18, 2026
  4

• Replace PrintWriter with BufferedWriter

  refactoring
  apalache-mc/apalache#3448 · Filter by author konnov opened on Aug 11, 2026

• Expanding a powerset under a let-definition

  bug
  Bug

  apalache-mc/apalache#3442 · Filter by author konnov opened on Aug 7, 2026
  2

• Replace kiama with prettier4j

  DevOpsrefactoring
  apalache-mc/apalache#3438 · Filter by author konnov opened on Aug 6, 2026

• Speed-up integration tests and drop mdx and nix

  DevOpstesting
  apalache-mc/apalache#3427 · Filter by author konnov opened on Aug 4, 2026
  2

• Java facade for the intermediate representation

  feature
  apalache-mc/apalache#3426 · Filter by author konnov opened on Aug 4, 2026
  

• Move FineTuningOptions into the configuration framework

  refactoring
  apalache-mc/apalache#3420 · Filter by author konnov opened on Aug 3, 2026
  

• Resolve two remaining issues of options refactoring

  refactoring
  apalache-mc/apalache#3419 · Filter by author konnov opened on Aug 3, 2026
  

• Remove the command test

  refactoring
  apalache-mc/apalache#3412 · Filter by author konnov opened on Jul 31, 2026

• Rename config options

  refactoring
  apalache-mc/apalache#3407 · Filter by author konnov opened on Jul 30, 2026
  

• Add cinit to JsonRpcServer

  featureFserver
  Feature

  apalache-mc/apalache#3406 · Filter by author konnov opened on Jul 30, 2026

• Remove --features=no-rows

  llmrefactoring
  apalache-mc/apalache#3405 · Filter by author konnov opened on Jul 30, 2026

• Optimization pass makes some integration tests fruitless

  testing
  apalache-mc/apalache#3403 · Filter by author konnov opened on Jul 27, 2026
  1

• Identify assignments right in the PrimingPass

  effort-mediumfeatureimpact-low
  apalache-mc/apalache#3356 · Filter by author konnov opened on May 22, 2026

• Return a non-zero exit code when a spec assumption is violated

  featureimpact-low
  apalache-mc/apalache#3349 · Filter by author lemmy opened on May 16, 2026

• Apalache rejects the invariant ENABLED (x') when the body of ENABLED is a primed variable

  bugimpact-low
  apalache-mc/apalache#3275 · Filter by author lemmy opened on Mar 3, 2026
  2

• Fresh variable incorrectly chosen when using CHOOSE to select unique elements out of a set

  bugdeferred
  apalache-mc/apalache#3165 · Filter by author edwardcwang opened on Sep 12, 2025
  1

• Set filter over SUBSET with uninterpreted types not supported

  bugdeferred
  apalache-mc/apalache#3149 · Filter by author edwardcwang opened on Aug 26, 2025
  1

• LET block with temporal checking leads to undeclared operator skolem error crash

  bug
  apalache-mc/apalache#3119 · Filter by author edwardcwang opened on Jul 21, 2025

• Generate SMT from TLA+

  apalache-mc/apalache#3109 · Filter by author Abhinandan-Pal opened on Jun 17, 2025
  7