Research: TLA+ formal verification language support in semfora

[Kadajett]

Background

Context

A contributor (danrob) suggested adding TLA+ support to semfora-engine. TLA+ is a formal specification language used for verifying concurrent and distributed systems. It's niche but used seriously in industry (AWS, Microsoft, MongoDB).

What to Research

1. Tree-sitter grammar availability — does a TLA+ tree-sitter grammar exist? Quality? Maintenance status? If not, what would it take to write one?

2. TLA+ language structure — what are the key constructs?

   • Modules, extends/instances
   • Operators (like functions), definitions
   • Variables, constants
   • Temporal logic operators ([]P, <>P, P ~> Q)
   • PlusCal algorithm blocks (embedded in TLA+ comments)
   • THEOREM, ASSUME, AXIOM
   • How do these map to semfora's existing symbol types (function, variable, module, etc.)?

3. What semfora features would apply to TLA+ specs?

   • Symbol indexing (operators, variables, constants)
   • Module dependency graph (EXTENDS, INSTANCE)
   • Call graph equivalent (operator references)
   • Duplicate detection (similar operator definitions across specs)
   • Complexity analysis (spec size, temporal logic depth)

4. Public TLA+ repositories for testing — find 3-5 good ones:

   • https://github.com/tlaplus/Examples (official)
   • AWS specs, Cosmos DB specs, etc.

5. Integration points with semfora codebase — where would TLA+ plug in?

   • src/lang.rs — new Lang::Tla variant
   • src/detectors/ — new tla.rs detector
   • Tree-sitter parser integration
   • Symbol extraction patterns

Deliverables

1. A Mermaid diagram showing the architecture of TLA+ support — how it connects to semfora's existing modules. Generate a shareable Mermaid Live Editor link (https://mermaid.live/edit#pako/...) so we can discuss it visually. Stub the connection points to the larger codebase.

2. Post findings as comments on this issue.

3. If viable, create a single implementation ticket in Planning (don't create multiple phases — this is exploratory).

Focus Areas

• tree-sitter grammar
• language constructs mapping
• mermaid architecture diagram
• public test repos