Open Issues Need Help
View All on GitHub [FEATURE] Interval analysis to improve a..b 2 days ago
help wanted usability
APALACHE: symbolic model checker for TLA+ and Quint
Scala
#apalache#model-checking#quint#smt#tla#tlaplus#verification
Typechecking crashes with `IllegalArgumentException: Unsupported expression` on unbounded quantification (e.g., `\A x: P`). about 1 month ago
bug help wanted usability impact-medium
APALACHE: symbolic model checker for TLA+ and Quint
Scala
#apalache#model-checking#quint#smt#tla#tlaplus#verification
ADR015 is using very old type annotations about 1 year ago
AI Summary: Update the type annotations in ADR015 (a document describing how to produce parseable counterexamples for the Apalache model checker) to reflect the current type system used by Apalache. This involves migrating from older annotation styles to the newer, documented style.
Complexity:
3/5
help wanted doc good-first-issue
APALACHE: symbolic model checker for TLA+ and Quint
Scala
#apalache#model-checking#quint#smt#tla#tlaplus#verification