Modeling the context

SpecLogician builds a mathematical context — a precise, machine-checkable model of your system's behavior. The context is assembled from four layers, each building on the one before it:

1. Domain base — IML types that define the shape of state and actions
2. Predicates — boolean classifications over state and actions
3. Transitions — pure functions that define how state evolves
4. Scenarios — given / when / then compositions that capture behavioral paths

Together, these form a Spec: a structured formal model that can be analyzed, verified, and refined incrementally.

Why layer it this way?

Each layer is small, local, and independently checkable. This matters because:

• LLMs work well with small targets. An LLM can propose a predicate or edit a transition without needing to understand the entire spec.
• The reasoning engine handles global consistency. ImandraX checks that all the pieces fit together — satisfiability, conflicts, reachability — so no single edit needs to be globally correct on its own.
• Progress is measurable. Every change produces a typed diff with quantified metrics. You always know whether the model improved or regressed.

The following pages walk through each layer in detail.