Why it works for LLMs

SpecLogician is designed from the ground up to give LLMs mathematical context they can actually use. This isn't an afterthought — it's a core design constraint.

The context problem

LLMs reason over whatever fragments fit in the prompt. For large systems, this means:

No visibility into cross-module interactions
No way to check if a proposed change preserves correctness
No stable reference for what the system actually does

SpecLogician solves this by building a shared semantic model that both humans and LLMs can reference.

Playing to LLM strengths

Every interaction with SpecLogician is:

Small — one scenario, one predicate, one transition at a time
Typed — the CLI enforces structure, preventing malformed changes
Machine-checkable — ImandraX catches logical errors the LLM misses
Measurable — diffs tell the LLM whether its change helped or hurt

The LLM handles local creativity (proposing scenarios, translating code to predicates). The reasoning engine handles global consistency (checking all scenarios together, finding uncovered regions).

Structured change format

Changes are JSON batch operations — the format LLMs produce most reliably:

[
  {
    "kind": "PredicateAdd",
    "pred_type": "action",
    "pred_name": "qty_ok",
    "pred_src": "a.qty <= 10000"
  },
  {
    "kind": "ScenarioAdd",
    "scenario_name": "accept_small",
    "when": { "add": ["qty_ok"] },
    "then": { "add": ["on_order"] }
  }
]

Feedback-driven convergence

After every change, the LLM receives:

Diff outcomes — IMPROVED, DECLINED, or NO_CHANGE for each metric
Recommendations — prioritized suggestions for what to do next
Complement regions — concrete examples of uncovered behavior
Reachability gaps — scenarios that can't be reached from initial states

This transforms the LLM from a one-shot generator into an iterative collaborator that converges on a complete, verified specification — building mathematical context for the project one scenario at a time.