jrjsmrtn/tlx

A Spark DSL for writing TLA+/PlusCal specifications in Elixir

10Stars on the repository
7Mods indexed here, across every type
1mo agoLast push, which is what freshness is scored on
MITLicence, which decides whether bodies are shown

spark

01

jrjsmrtn/tlx

Skill Claude CodeCodex

Use this skill when building or modifying the Spark DSL extension. Consult for entity definitions, sections, transformers, and verifiers.

not rated 10 1mo ago A 27 tokens original MIT

formal-spec

02

jrjsmrtn/tlx

Skill Claude CodeCodex

Formal specification workflow for state machines using TLX (TLA+ in Elixir). Covers writing abstract specs from ADRs, generating concrete specs from code, enriching extracted skeletons with invariants and properties, refinement checking, and CI integration. Use when asked to write a spec, formally specify, verify a…

not rated 10 1mo ago A 86 tokens original MIT

spec-audit

03

jrjsmrtn/tlx

Skill Claude CodeCodex

Scan an Elixir/Erlang project for modules that TLX can formally specify. Covers OTP behaviours (GenServer, genstatem, LiveView), framework extensions (Ash.StateMachine), and workflow/pipeline libraries (Reactor, Broadway). Reports spec coverage and suggests where to focus verification effort. Use when asked to audit…

not rated 10 1mo ago A 88 tokens original MIT

spec-drift

04

jrjsmrtn/tlx

Skill Claude CodeCodex

Detect when implementation code has changed but its formal TLX spec has not been updated. Compares git timestamps, re-extracts structure, and diffs against existing specs. Use when asked to check spec drift, detect stale specs, verify specs are up to date, or audit spec freshness.

not rated 10 1mo ago A 63 tokens original MIT

visualize

05

jrjsmrtn/tlx

Skill Claude CodeCodex

Generate state machine diagrams from TLX specs in multiple formats (DOT, Mermaid, PlantUML, D2). Use when asked to visualize a spec, generate a diagram, draw a state machine, create a graph, or render a spec as an image.

not rated 10 1mo ago A 55 tokens original MIT

At most 3 mods per repository are shown here, and a mod shipped inside a plugin is left to that plugin's page — the rest are on their repository pages: