TLA
Generated by scripts/gen-format-pages.py from docs/data/format-metadata/, FILE_FORMATS.csv and docs/formats-master.csv. Do not edit by hand: change the source, then run the script.
TLA+ Preview.
At a glance
| Purpose | A TLA+ specification module: constants, variables, operator definitions and theorems for specifying concurrent systems. |
| Extensions | .tla |
| Poka parser | poka-tla |
| Viewer | poka-metadata-card-viewer |
| Depth tier | Metadata card (see Depth tiers) |
| Breadth tier | B4 Summary (see Breadth tiers) |
How much Poka reads
B4 Summary. The container and metadata are read and summarised (counts, properties, structure), but the main content is not rendered.
Confidence: medium (the reviewer read the code). Basis: Reviewed 2026-10-26: read parsers/poka-tla/src/main.rs (296 lines) and plugin.json in full. The crate has no unit tests and no tests/samples.rs, and the corpus has no .tla sample, so the tier rests on reading the code. Covers .tla. The output is a metadata card of counts found by matching text line by line: the module name and terminator, EXTENDS, CONSTANTS, VARIABLES, operator definitions, LOCAL, RECURSIVE, INSTANCE, THEOREM, ASSUME and line counts. Judgement: B4, because the structure is summarised but the source itself is never shown.
What Poka does not read
- The source text is not shown: the card carries only counts and a few sample names, with no code view or highlighting
- Constructs are found by matching text line by line, not by parsing, so multi-line declarations, nested or indented definitions and keywords inside strings or comments can be miscounted
- Counts of named items stop where their name list is capped (extends at 16, definitions at 64, theorems at 32), so a larger file under-reports them
- Files over 32 MiB are cut to the first 32 MiB (the card says so)
- Text that is not UTF-8 is decoded with replacement characters; no other encoding is tried
- PlusCal algorithms in comments are not recognised
Libraries
Libraries Poka uses or has assessed for this format, with the status, licence and language the registry records.
- tree-sitter-tlaplus (candidate; MIT; C/JavaScript; https://github.com/tlaplus-community/tree-sitter-tlaplus) — Tree-sitter grammar for TLA+ and PlusCal with Rust, Node and Python bindings; syntax only, tolerant of errors.
- SANY (tlaplus/tlaplus) (candidate; MIT; Java; https://github.com/tlaplus/tlaplus) — Reference TLA+ parser tla2sany.SANY in the TLA+ tools; requires Java 11+; can export parse tree as XML.
- tla-syntax (candidate; MIT; Rust; https://github.com/copyleftdev/tlatools-rs) — Parser, AST and printer for TLA+, with no dependencies; v0.2.0, updated 2026-08-11; matched on lib.rs, not tested
Sources
- parsers/poka-tla/src/main.rs
- parsers/poka-tla/plugin.json