A modern specification language and model checker for concurrent and distributed systems. Faster than TLA+/TLC.
active 2026-02-11 → 2026-04-18 (UTC)
Activity over time
Daily event counts in the loaded window
Line chart, 67 days from 2026-02-11 to 2026-04-18. Pushes: 91 total, peak 13 in a day. Pull requests: 3 total, peak 2 in a day. Issues: 51 total, peak 13 in a day. Comments: 25 total, peak 9 in a day. Stars: 4 total, peak 2 in a day.
- Pushes
- Pull requests
- Issues
- Comments
- Stars
Stars, PRs, issues and forks are under-captured in the later part of this window. GH Archive progressively stopped capturing non-push events during 2026 — −95% or worse by the end of the window. Every series here except Pushes fades for that reason, so a decline above reflects the archive, not this repository. Pushes stay reliable throughout, so read them, and the contributor counts derived from them, as the real signal. Data health has the measurements.
Top contributors
Pushes, PRs, issues, reviews and comments — stars and forks excluded, so this is contribution rather than popularity
| Contributor | Contributions | Pushes | PRs | Comments |
|---|---|---|---|---|
| danwt | 170 | 91 | 3 | 25 |
Recent activity
Latest issues, pull requests and releases
- Releasegithub-actions[bot]2026-03-06 19:56v3.1.1
- Issue comment#84danwt2026-03-06 14:38soundness: drive TLA+ parser differential mismatches to zero
- Issue#75danwt2026-03-06 14:37perf: swap to SmallVec for action parameter combinations (H2)
- Issue#85danwt2026-03-06 12:39feat: machine-readable JSON output for AI-first workflow
- Issue#83danwt2026-03-06 12:39ci: test suite exceeds 1-minute target
- Releasegithub-actions[bot]2026-02-24 19:33v3.0.1
- Issue#74danwt2026-02-24 11:59fix len .. in syntax
- Issue#68danwt2026-02-24 00:03BFS evaluator panics on forall with range exceeding map domain
- Issue comment#68danwt2026-02-24 00:03BFS evaluator panics on forall with range exceeding map domain
- Issue#65danwt2026-02-24 00:02Specl check tla panic
- Issue#72danwt2026-02-23 17:45Parser: `not in` binary operator cannot be parsed
- Issue#69danwt2026-02-23 17:41Parser: membership `in` operator not allowed in quantifier/fix bodies
- Issue#69danwt2026-02-23 17:25Parser: membership `in` operator not allowed in quantifier/fix bodies
- Issue comment#64danwt2026-02-20 11:43docs: ensure examples and docs use {:} for empty dict and demonstrate Set[T] usage
- Issue#62danwt2026-02-20 11:43symbolic unbounded set int cannot infer range forces bfs
- Issue#60danwt2026-02-20 11:43POR auto-optimization hides invariant violation in kaspa.specl
- Issue#59danwt2026-02-20 11:43bug: Dict range type mismatch when parameter range doesn't match Dict key range
- Issue comment#59danwt2026-02-20 11:43bug: Dict range type mismatch when parameter range doesn't match Dict key range
- Issue#58danwt2026-02-20 11:43bug: portfolio mode hangs on all tested specs
- Issue#57danwt2026-02-20 11:43bug: --check-only flag incompatible with --symbolic
- Issue comment#63danwt2026-02-20 11:42impl symbolic rename or vscode and lang server
- Issue comment#48danwt2026-02-20 11:42feat: add sum types and pattern matching [low prio - do not implement]
- Issue comment#35danwt2026-02-20 11:42symbolic: support Set[Seq[T]] (needed for message-passing protocols)
- Issue#41danwt2026-02-20 09:25Replace `choose` keyword with `fix` as the primary syntax
- Issue#51danwt2026-02-20 09:24feat: support nondet in init blocks
Totals cover only the window loaded into ClickHouse and count events, not GitHub's lifetime totals — 4 stars here means stars gained during the window, not the repo's star count.