Issues

• soundness: IC3 reports OK on a spec with a real violation (DieHard)

  bug
  danwt/specl#96 · Filter by author danwt opened on Jun 26, 2026
  1

• bug: partial dict init panics with out-of-bounds index instead of erroring

  bug
  danwt/specl#95 · Filter by author danwt opened on Jun 26, 2026

• soundness: add a cross-tool differential oracle (vs TLC)

  danwt/specl#94 · Filter by author danwt opened on Jun 26, 2026

• symbolic: encode sum() over collections

  danwt/specl#92 · Filter by author danwt opened on Jun 26, 2026

• Module composition: EXTENDS / INSTANCE

  enhancement
  danwt/specl#91 · Filter by author danwt opened on Jun 26, 2026

• Liveness checking: evaluate temporal operators and fairness

  enhancement
  danwt/specl#90 · Filter by author danwt opened on Jun 26, 2026

• Toolchain: annotation-driven model generation for model-checking business logic (LLM + standard tooling + Specl)

  enhancement
  danwt/specl#89 · Filter by author danwt opened on Jun 26, 2026

• Range-typed const won't widen into a wider range type

  danwt/specl#88 · Filter by author danwt opened on Jun 26, 2026
  1

• fmt deletes all comments

  danwt/specl#87 · Filter by author danwt opened on Jun 26, 2026
  1

• let x = EXPR in BODY: membership in in value position requires parentheses

  danwt/specl#71 · Filter by author danwt opened on Feb 23, 2026

• feat: support string-keyed maps

  enhancement
  danwt/specl#50 · Filter by author danwt opened on Feb 17, 2026
  1

• symbolic: support Set[Seq[T]] (needed for message-passing protocols)

  danwt/specl#35 · Filter by author danwt opened on Feb 17, 2026
  1