Owner

tlaplus

9 indexed repositories · View on GitHub

tlaplus
TLC is a model checker for specifications written in TLA+. The TLA+Toolbox is an IDE for TLA+.

Java · 3058 stars
Examples
A collection of TLA⁺ specifications of varying complexities.

TLA · 1570 stars
vscode-tlaplus
TLA+ language support for Visual Studio Code

TypeScript · 435 stars
CommunityModules
TLA+ snippets, operators, and modules contributed and curated by the TLA+ community

TLA · 315 stars
tlapm
The TLA⁺ Proof Manager

OCaml · 124 stars
foundation
TLA+ Foundation

HTML · 34 stars
tla-by-example

TypeScript · 10 stars
model-checker-hardening
Hardening TLC and Apalache through systematic, differential, fuzz, and regression testing to improve the reliability of TLA+ model checking

Java · 7 stars
ValidationTestSuite
Tool qualification tests and reports for the TLA+ model checker

Python · 6 stars

Beginner friendly Everything

Open All

A label on a top-level `[][A]_v` property makes TLC reject a formula it otherwise checks Open

finding tlc

Difficulty 3/5 1-2 days Newbie friendliness 68/100

tlaplus/model-checker-hardening#180 · Opened Sep 19, 2026
A fold whose combinator returns `SUBSET` evaluates to the empty set Open

apalache finding

Difficulty 4/5 3-5 days Newbie friendliness 45/100

tlaplus/model-checker-hardening#176 · Opened Sep 19, 2026
`PrettyWriter` does not delimit a set-map body wrapped in a one-argument conjunction or disjunction Open

apalache finding

Difficulty 3/5 1-2 days Newbie friendliness 58/100

tlaplus/model-checker-hardening#169 · Opened Sep 17, 2026
An evaluation error under a bounded `\E` around a temporal formula is reported as "TLC cannot handle the temporal formula" Open

finding tlc

tlaplus/model-checker-hardening#161 · 1 comment · 1 assignee · Opened Sep 15, 2026
`ENABLED UNCHANGED e` fails with a `WF_v(A)` message when `e` is not a variable or tuple Open

finding tlc

tlaplus/model-checker-hardening#162 · 1 assignee · Opened Sep 15, 2026
A function constructor with two bound variables under `~>` crashes the renamer Open

apalache finding

Difficulty 3/5 1-2 days Newbie friendliness 55/100

tlaplus/model-checker-hardening#159 · Opened Sep 15, 2026
A quantifier around a temporal formula leaves its bound variable unassigned Open

apalache finding

Difficulty 3/5 1-2 days Newbie friendliness 70/100

tlaplus/model-checker-hardening#158 · Opened Sep 15, 2026
Warn when TLA+ specifications directly use `TLC!Assert` Open

enhancement SANY

Difficulty 4/5 3-5 days Newbie friendliness 58/100

tlaplus/tlaplus#1437 · 1 comment · Opened Sep 15, 2026
An evaluation error while checking liveness escapes as TLC error 1000 Open

finding tlc

tlaplus/model-checker-hardening#152 · 1 assignee · Opened Sep 15, 2026
A leads-to nested in a leads-to fails `TemporalPass` with an empty diagnostic Open

apalache finding

Difficulty 3/5 1-2 days Newbie friendliness 55/100

tlaplus/model-checker-hardening#153 · Opened Sep 15, 2026
A nested one-conjunct list in a fold lambda fails type checking under `--temporal` Open

apalache finding

Difficulty 3/5 1-2 days Newbie friendliness 56/100

tlaplus/model-checker-hardening#154 · Opened Sep 15, 2026
IntervalValue enumeration wraps after MaxInt Open

bug soundness \/ completeness Tools

Difficulty 3/5 1-2 days Newbie friendliness 72/100

tlaplus/tlaplus#1433 · Opened Sep 14, 2026
Empty interval-domain functions disagree on compareTo and equals Open

bug soundness \/ completeness Tools

Difficulty 4/5 3-5 days Newbie friendliness 52/100

tlaplus/tlaplus#1432 · Opened Sep 14, 2026
`ENABLED` in the guard of a `CASE` without `OTHER` makes a false invariant pass Open

apalache finding

Difficulty 4/5 3-5 days Newbie friendliness 48/100

tlaplus/model-checker-hardening#140 · Opened Sep 14, 2026
An evaluation error in an eventuality of the initial state exits with status 0 Open

finding tlc

tlaplus/model-checker-hardening#137 · 1 comment · 1 assignee · Opened Sep 14, 2026
An evaluation error in a constant eventuality escapes as TLC error 1000 Open

finding tlc

tlaplus/model-checker-hardening#138 · 1 comment · 1 assignee · Opened Sep 14, 2026
`UNCHANGED` of an assigned variable is rejected as an assignment Open

apalache finding

Difficulty 3/5 1-2 days Newbie friendliness 68/100

tlaplus/model-checker-hardening#139 · Opened Sep 14, 2026
An invariant evaluation error is reported with the call stack and exit status of a different error Open

finding tlc

tlaplus/model-checker-hardening#135 · 1 comment · 1 assignee · Opened Sep 14, 2026
A computed empty co-domain crashes `CherryPick` on a function set Open

apalache finding

Difficulty 3/5 1-2 days Newbie friendliness 62/100

tlaplus/model-checker-hardening#131 · Opened Sep 13, 2026
Bounded `CHOOSE` and `\E` materialize an interval bound, ignoring the enumeration limit Open

finding tlc

tlaplus/model-checker-hardening#130 · 1 comment · 1 assignee · Opened Sep 13, 2026
Action decomposition materializes a quantifier bound, ignoring the enumeration limit Open

finding tlc

tlaplus/model-checker-hardening#116 · 2 comments · 1 assignee · Opened Sep 11, 2026
A computed empty function-set domain loses every initial state Open

apalache finding

Difficulty 4/5 3-5 days Newbie friendliness 50/100

tlaplus/model-checker-hardening#117 · Opened Sep 11, 2026
`PrettyWriter` lets a nested `CASE` absorb the enclosing `CASE`'s later arms Open

apalache finding

Difficulty 3/5 1-2 days Newbie friendliness 68/100

tlaplus/model-checker-hardening#113 · Opened Sep 10, 2026
`\union` with `Int` or `Nat` silently drops the infinite operand Open

apalache finding

Difficulty 4/5 3-5 days Newbie friendliness 45/100

tlaplus/model-checker-hardening#111 · Opened Sep 10, 2026
Parser rejects a RECURSIVE definition of the prefix `-.` operator applied to itself Open

bug SANY

tlaplus/tlaplus#1418 · 2 comments · 1 reaction · 2 assignees · Opened Sep 9, 2026
A function over an infinite domain gets an empty `DOMAIN` Open

apalache finding

Difficulty 4/5 3-5 days Newbie friendliness 45/100

tlaplus/model-checker-hardening#110 · Opened Sep 9, 2026
`SetMapRule` throws `NotImplementedError` for a powerset Open

apalache finding

Difficulty 3/5 1-2 days Newbie friendliness 55/100

tlaplus/model-checker-hardening#109 · Opened Sep 9, 2026
Proof fails depending on surrounding unrelated context Open

Difficulty 4/5 3-5 days Newbie friendliness 52/100

tlaplus/tlapm#291 · 2 comments · Opened Sep 7, 2026
Skolemizable `\E` over an expression that evaluates to `Int` crashes `QuantRule` Open

apalache finding

Difficulty 3/5 1-2 days Newbie friendliness 48/100

tlaplus/model-checker-hardening#101 · Opened Sep 6, 2026
`ApaFoldSet` feeds a raw arena cell into `x \in {y}`, crashing `SetInRule` Open

apalache finding

Difficulty 3/5 1-2 days Newbie friendliness 25/100

tlaplus/model-checker-hardening#102 · Opened Sep 6, 2026
A function application makes a bounded CHOOSE keep its set elements lazy and exhaust the heap Open

finding tlc

Difficulty 4/5 3-5 days Newbie friendliness 48/100

tlaplus/model-checker-hardening#98 · 1 comment · Opened Sep 5, 2026
`UNION` rejects a powerset-valued `CHOOSE` during bounded checking Open

apalache finding

Difficulty 4/5 3-5 days Newbie friendliness 45/100

tlaplus/model-checker-hardening#96 · Opened Sep 5, 2026
`LazyEquality` asserts on a function set with an undefined domain value Open

apalache finding

Difficulty 3/5 1-2 days Newbie friendliness 48/100

tlaplus/model-checker-hardening#97 · Opened Sep 5, 2026
Function sets over infinite domains escape as `IllegalArgumentException` Open

apalache finding

Difficulty 4/5 3-5 days Newbie friendliness 45/100

tlaplus/model-checker-hardening#95 · Opened Sep 5, 2026
Set capability diagnostics can escape as TLC error 1000 Open

finding tlc

Difficulty 4/5 3-5 days Newbie friendliness 45/100

tlaplus/model-checker-hardening#93 · 1 comment · Opened Sep 5, 2026
Integer division truncates toward zero for a negative divisor Open

apalache finding

Difficulty 3/5 1-2 days Newbie friendliness 45/100

tlaplus/model-checker-hardening#94 · Opened Sep 5, 2026
`PrettyWriter` does not delimit the `LET` it synthesizes for a lambda argument Open

apalache finding

Difficulty 3/5 1-2 days Newbie friendliness 52/100

tlaplus/model-checker-hardening#88 · Opened Sep 4, 2026
`IsFiniteSet` evaluates to `TRUE` for `Int` and `Nat` Open

apalache finding

Difficulty 4/5 3-5 days Newbie friendliness 48/100

tlaplus/model-checker-hardening#87 · Opened Sep 4, 2026
Diagnosed evaluation errors exit with generic status 255 Open

finding tlc

Difficulty 3/5 1-2 days Newbie friendliness 55/100

tlaplus/model-checker-hardening#86 · Opened Sep 4, 2026
`ConstSimplifier` leaves an undeclared local operator Open

apalache finding

Difficulty 4/5 3-5 days Newbie friendliness 35/100

tlaplus/model-checker-hardening#83 · Opened Sep 4, 2026
`CherryPick` cannot select symbolic-set values from a finite set Open

apalache finding

Difficulty 3/5 1-2 days Newbie friendliness 52/100

tlaplus/model-checker-hardening#82 · Opened Sep 4, 2026
Diagnosed errors exit with generic status 255 Open

apalache finding

Difficulty 4/5 3-5 days Newbie friendliness 48/100

tlaplus/model-checker-hardening#66 · Opened Sep 3, 2026
Quantification over `Int` escapes as `UnsupportedOperationException` Open

apalache finding

Difficulty 4/5 3-5 days Newbie friendliness 35/100

tlaplus/model-checker-hardening#64 · Opened Sep 3, 2026
`TlaCheckedBuilder.build` overflows on a long valid composition Open

apalache finding

Difficulty 3/5 1-2 days Newbie friendliness 55/100

tlaplus/model-checker-hardening#65 · Opened Sep 3, 2026
Equality crashes on symbolic-set arena representations Open

apalache finding

Difficulty 4/5 3-5 days Newbie friendliness 42/100

tlaplus/model-checker-hardening#62 · Opened Sep 3, 2026
Symbolic exponentiation crashes while casting a Z3 real to an integer Open

apalache finding

Difficulty 3/5 1-2 days Newbie friendliness 68/100

tlaplus/model-checker-hardening#63 · Opened Sep 3, 2026
`SetFilterRule` throws `NotImplementedError` for symbolic sets Open

apalache finding

Difficulty 4/5 3-5 days Newbie friendliness 42/100

tlaplus/model-checker-hardening#60 · Opened Sep 3, 2026
Empty-domain function sets violate reflexive equality Open

apalache finding

Difficulty 3/5 1-2 days Newbie friendliness 52/100

tlaplus/model-checker-hardening#61 · Opened Sep 3, 2026
SANY rejects labels inside `EXCEPT` clauses Open

finding sany

Difficulty 4/5 3-5 days Newbie friendliness 45/100

tlaplus/model-checker-hardening#58 · Opened Sep 3, 2026
Function-domain errors inside set filters escape as TLC error 1000 Open

finding tlc

Difficulty 4/5 3-5 days Newbie friendliness 42/100

tlaplus/model-checker-hardening#59 · Opened Sep 3, 2026

Showing the newest 100

This page lists what was indexed most recently. Advanced filter has the whole inventory, narrowed by language, difficulty and how long a task takes.

Open advanced filter

tlaplus

Showing the newest 100

Get new issues in your inbox