Reasoning about the context

Building a formal model is only half the story. The other half is reasoning about it — checking that the model is internally consistent, that it covers the behavior space, and that its scenarios connect in the ways you expect.

SpecLogician delegates all formal reasoning to ImandraX, a symbolic reasoning engine based on the Imandra theorem prover. Every analysis is automatic — you don't write proofs or configure solvers. You build the model; ImandraX reasons about it.

The reasoning pipeline

When a change is applied to the model, SpecLogician runs a targeted analysis pipeline. Only the components affected by the change are rechecked:

1. Consistency checking — Is the IML valid? Are predicates satisfiable? Are scenarios free of contradictions?
2. Coverage and gaps — What parts of the state/action space are not covered by any scenario?
3. Reachability — Can every scenario be reached from the initial state? Are safety and liveness properties maintained?
4. Conflict detection — Do any two scenarios overlap or subsume each other?
5. Trace matching — Do concrete test traces and log traces align with the formal scenarios?

Each analysis produces structured results that feed into diffs, recommendations, and the next iteration of the model.

The following pages describe each kind of reasoning in detail.