Model refinement

Counterexample-Guided Abstraction Refinement (CEGAR) is one of the most successful ideas in formal verification. Given a program, a property, and an initial abstraction, CEGAR iteratively refines the abstraction using counterexamples until the property can be proved or a genuine violation is found.

SpecLogician is inspired by the same refinement principle, but applies it at a different level.

From abstraction refinement to model refinement

Classical CEGAR assumes that the underlying system model already exists. The challenge is to find an abstraction that is precise enough to verify the property while remaining tractable.

In practice, however, many teams face an earlier challenge:

The system is only partially understood, the requirements are scattered across documents and code, and no coherent behavioral model exists.

SpecLogician focuses on this stage of the problem.

Rather than refining an abstraction of a fixed model, SpecLogician incrementally refines the model itself. The goal is not simply to eliminate spurious counterexamples, but to improve the fidelity of the behavioral understanding captured by the model.

The classical CEGAR loop

1. Construct an initial abstraction.
2. Verify a property.
3. Analyze any counterexample.
4. Determine whether the counterexample is genuine or spurious.
5. Refine the abstraction.
6. Repeat.

The refinement target is the abstraction. The underlying system semantics remain fixed.

The SpecLogician reasoning loop

1. Gather evidence from requirements, code, tests, logs, traces, incidents, and domain knowledge.
2. Construct an initial behavioral model.
3. Analyze scenarios, queries, and desired properties.
4. Generate explanations, counterexamples, contradictions, and uncovered assumptions.
5. Refine states, transitions, predicates, scenarios, and constraints.
6. Repeat.

The refinement target is the model itself. The representation evolves as understanding evolves.

What makes the analysis distinctive

A defining feature of SpecLogician is how the model is analyzed and refined.

The model is an executable, compositional, scenario-based specification expressed in a full-featured computational logic — the Imandra Modeling Language (IML) — and reasoned about by ImandraX.

Because the model is executable and written in a rich logic, ImandraX can apply region decomposition: it symbolically partitions the model's behavior into a finite set of regions, where each region captures a class of executions together with the constraints that characterize it. Each region comes with a concrete sample point and a precise symbolic description, so the full behavioral space becomes enumerable and inspectable rather than opaque.

This decomposition is what turns refinement into a tractable, evidence-driven activity:

• Coverage analysis — comparing scenarios against the regions of behavior the model admits, exposing regions that no scenario describes.
• Missing scenarios — surfacing reachable behaviors that are real but unaccounted for, expressed in concrete, scenario-shaped terms.
• Contradictions and overlaps — revealing where scenarios conflict, subsume one another, or leave intent ambiguous.
• Targeted refinement — pointing precisely at the states, transitions, predicates, and constraints that need to be added or sharpened.

Region decomposition over executable scenario-based models is what lets the loop above operate on meaningful, reachable behaviors rather than low-level encodings.

Counterexamples as knowledge

In classical CEGAR, a counterexample typically serves one of two purposes:

• demonstrating a real violation, or
• revealing an overly coarse abstraction.

In SpecLogician, a counterexample often reveals something different:

• a missing state,
• an overlooked transition,
• an unstated assumption,
• an ambiguous requirement,
• an incomplete scenario,
• or a misunderstanding of system behavior.

The result is not merely a better abstraction but a richer and more accurate behavioral model.

Living models vs. fixed models

Traditional verification workflows often begin once the model and requirements have been defined.

SpecLogician treats model construction as a first-class activity. Models evolve continuously as new evidence becomes available:

• new requirements,
• new tests,
• production incidents,
• execution traces,
• architectural changes,
• and operational observations.

This allows the model to remain aligned with the system throughout its lifecycle.

Complementary approaches

SpecLogician is not a replacement for CEGAR-based verification techniques. The two approaches address different challenges:

In many workflows they are complementary.

SpecLogician helps teams discover, organize, and refine the behavioral models that make rigorous analysis possible. Once those models exist, classical verification techniques — including CEGAR-based methods — can be applied where appropriate.