Create TypeScript bindings for TLA+ (@terraphim/tlaplus)
Nobody has claimed this yet.
Assessment
- Difficulty
- 5/5
- Estimated time
- Over a week
- Newbie friendliness
- 25/100
- Issue type
- Feature
- Clarity
- Mostly clear
- Activity status
- Stale
- Tech stack
- java, typescript
Research direction
Read docs/src/research/tlaplus-typescript-bindings.md and docs/src/research/tlaplus-typescript-design.md first, then compare the proposed src/parser, src/ast, src/eval, src/format, src/bridge, and src/cli areas with the eight decomposed Gitea tasks. Done means the @terraphim/tlaplus package and its documented tooling are implemented through the CLI and prepared for npm publication.
Written by the indexing model from the issue text.
Description
Summary
Create a TypeScript library @terraphim/tlaplus providing native TLA+ tooling: parsing via tree-sitter-tlaplus, typed AST, expression evaluation, formatting, and TLC model checking bridge. Implementation will be orchestrated by Symphony on bigbox with output to Gitea.
Research & Design Documents
- Research:
docs/src/research/tlaplus-typescript-bindings.md - Design:
docs/src/research/tlaplus-typescript-design.md
Key Findings
The TLA+ ecosystem already has significant TypeScript/JavaScript implementations:
- tree-sitter-tlaplus (
@tlaplus/tree-sitter-tlapluson npm) - production-ready parser - Spectacle - full JS TLA+ interpreter (~5000 LOC) by Will Schultz
- Quint - TypeScript-native TLA alternative by Informal Systems (1.2k stars)
- vscode-tlaplus - 97% TypeScript VS Code extension
Architecture
@terraphim/tlaplus
src/parser/ - tree-sitter wrapper, CST-to-AST transform
src/ast/ - TypeScript type definitions for TLA+ AST
src/eval/ - Expression evaluator (sets, logic, functions)
src/format/ - Pretty-printer
src/bridge/ - TLC model checking bridge (Java CLI)
src/cli/ - CLI tool (parse|format|validate|check)
Gitea Issue Decomposition (for Symphony)
| # | Title | Dependencies | Wave |
|---|---|---|---|
| 1 | Scaffold TypeScript project with build tooling | None | A |
| 2 | Define TypeScript types for TLA+ AST | None | A |
| 3 | Implement tree-sitter parser wrapper with CST-to-AST | #1, #2 | B |
| 4 | Implement basic expression evaluator | #2, #3 | C |
| 5 | Implement TLA+ formatter (pretty-printer) | #3 | C |
| 6 | Implement TLC CLI bridge for model checking | #1 | B |
| 7 | Create CLI tool (parse, format, validate, check) | #3, #4, #5, #6 | D |
| 8 | Documentation, examples, npm publish prep | #7 | E |
Symphony WORKFLOW.md
tracker:
kind: gitea
endpoint: https://git.terraphim.cloud
api_key: $GITEA_TOKEN
owner: terraphim
repo: tlaplus-ts
agent:
runner: claude-code
max_concurrent_agents: 2
max_turns: 15
claude_flags: "--dangerously-skip-permissions --allowedTools Bash,Read,Write,Edit,Glob,Grep"
settings: ~/.claude/symphony-settings.json
Next Steps
- Create Gitea repo
terraphim/tlaplus-ts - Create 8 Gitea issues with dependencies
- Deploy WORKFLOW.md to bigbox
- Run Symphony to dispatch Claude Code agents
See design document for full issue descriptions and acceptance criteria.
- Dominant language
- Rust
- Stars
- 62
- Forks
- 5
- Avg merge
- 2h 27m
- Merged PRs (30d)
- 1
Contributor guide
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
More from terraphim/terraphim-ai
-
Difficulty 5/5 Over a week Newbie friendliness 25/100
terraphim/terraphim-ai#885 ·
-
Difficulty 4/5 3-5 days Newbie friendliness 55/100
terraphim/terraphim-ai#871 ·
-
enhancement
Difficulty 5/5 Over a week Newbie friendliness 25/100
terraphim/terraphim-ai#810 · 2 comments ·
-
enhancement
Difficulty 5/5 Over a week Newbie friendliness 35/100
terraphim/terraphim-ai#729 ·
-
enhancement
Difficulty 5/5 Over a week Newbie friendliness 35/100
terraphim/terraphim-ai#728 ·
All issues in terraphim/terraphim-ai
Similar issues
-
Difficulty 2/5 1-3 hours Newbie friendliness 86/100
kwakseongjae/auto-hwp#319 ·
-
area:cli bug filter-quality good first issue priority:medium
Difficulty 2/5 1-3 hours Newbie friendliness 84/100
-
Difficulty 1/5 Under an hour Newbie friendliness 72/100
bevyengine/bevy#25861 ·
-
comp-datalake
Difficulty 2/5 1-3 hours Newbie friendliness 88/100
ClickHouse/ClickHouse#121222 ·
-
enhancement remote
Difficulty 2/5 1-3 hours Newbie friendliness 68/100