Skip to content

Pull requests: tlaplus/tlaplus

New pull request New
35 Open 370 Closed
35 Open 370 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Milestones
Filter by milestone
Loading
Reviews
Filter by reviews
No reviews Review required Approved review Changes requested
Assignee
Filter by who’s assigned
Assigned to nobody Loading
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Pull requests list

Trim whitespace from pre-comments text in XMLExporter test.
#1310 opened Feb 13, 2026 by sabjohnso Loading…
2
XML Exporter: add EXTENDS info to ModuleNode enhancement Lets change things for the better TLAPS Toolbox functionality related to the TLA proof system/manager Tools The command line tools - TLC, SANY, ...
#1309 opened Feb 12, 2026 by ahelwer Loading…
1
5
XML Exporter: expose LOCAL tag on definitions enhancement Lets change things for the better SANY Issues involving SANY's analysis TLAPS Toolbox functionality related to the TLA proof system/manager Tools The command line tools - TLC, SANY, ...
#1308 opened Feb 12, 2026 by ahelwer Loading…
1
XML Exporter: expose proof level enhancement Lets change things for the better SANY Issues involving SANY's analysis TLAPS Toolbox functionality related to the TLA proof system/manager Tools The command line tools - TLC, SANY, ...
#1307 opened Feb 12, 2026 by ahelwer Loading…
7
XML Exporter: skip linting & PlusCal validation in SANY enhancement Lets change things for the better Tools The command line tools - TLC, SANY, ...
#1305 opened Feb 11, 2026 by ahelwer Loading…
15
Add stdio-based MCP server with TLA+ tools and knowledge base AI Work related to TLAi+ enhancement Lets change things for the better
#1296 opened Feb 2, 2026 by lemmy • Draft
1 of 2 tasks
@lemmy
7
Add comprehensive corpus test for XMLExporter to validate TLA+ module exports. bug error, glitch, fault, flaw, ... help wanted We need your help Tools The command line tools - TLC, SANY, ...
#1295 opened Feb 2, 2026 by lemmy • Draft
1
fix: Allow simultaneous use of -loadTrace and -dumpTrace options
#1293 opened Feb 2, 2026 by Qian-Cheng-nju Loading…
3
TLC: Add x' \subseteq S support enhancement Lets change things for the better Tools The command line tools - TLC, SANY, ...
#1287 opened Jan 26, 2026 by ahelwer Loading…
1
7
TLC: Add support for EXPECT statement in model config file
#1269 opened Dec 15, 2025 by ahelwer • Draft
1
1
Refactor pcal package to use java.util.ArrayList instead of Vector
#1261 opened Nov 22, 2025 by younes-io Loading…
1
Refactor custom Vector usage to java.util.ArrayList
#1260 opened Nov 22, 2025 by younes-io Loading…
2 tasks done
2
Refactor NamedInputStream to facilitate reading TLA+ modules from non-file sources
#1225 opened Aug 6, 2025 by ahelwer Loading…
16
Using -dumptrace option to produce state dumps in machine readable format. enhancement Lets change things for the better good first issue Your entry point to contributing to TLA+ help wanted We need your help Tools The command line tools - TLC, SANY, ...
#1218 opened Jul 26, 2025 by just-now Loading…
@just-now
24
Using -dumptrace option to produce state dumps in machine readable format. enhancement Lets change things for the better good first issue Your entry point to contributing to TLA+ help wanted We need your help Tools The command line tools - TLC, SANY, ...
#1217 opened Jul 24, 2025 by lemmy • Draft
5
When an invariant is violated, show the values of any \A-bound names enhancement Lets change things for the better Tools The command line tools - TLC, SANY, ...
#1180 opened Apr 30, 2025 by Calvin-L • Draft
26
Move Value.isEmpty() to Enumerable
#1178 opened Apr 28, 2025 by Calvin-L Loading…
LazyValue no longer inherits from Value
#1148 opened Feb 19, 2025 by Calvin-L Loading…
5
Lasso-Shaped counterexample fails to reconstruct when VIEW present. bug error, glitch, fault, flaw, ... Tools The command line tools - TLC, SANY, ...
#1111 opened Jan 8, 2025 by lemmy • Draft
Bogus Error: The configuration file substitutes constant C with non-constant C2 when C2 is in fact constant. bug error, glitch, fault, flaw, ... help wanted We need your help Tools The command line tools - TLC, SANY, ...
#1110 opened Jan 7, 2025 by lemmy • Draft
Add unicode support to state / value serialization bug error, glitch, fault, flaw, ... Tools The command line tools - TLC, SANY, ... Unicode Unicode support for TLA
#1079 opened Nov 20, 2024 by fhackett Loading…
1
55
Add a :help command to the REPL
#1000 opened Aug 20, 2024 by Calvin-L Loading…
12
Show the changed variables as part of the transition if -difftrace is given and the successor has previously been added to the GraphViz graph. enhancement Lets change things for the better Tools The command line tools - TLC, SANY, ...
#985 opened Jul 6, 2024 by lemmy • Draft
4
Replace sun.misc.Unsafe with the new Java 22 FFM API
#951 opened Jun 15, 2024 by ahelwer • Draft
1
20
Supress SecurityManager deprecation warnings
#950 opened Jun 14, 2024 by ahelwer • Draft
1
3
ProTip! Find all pull requests that aren't related to any open issues with -linked:issue.