Formal verification

Formal verification means using mathematical reasoning to establish properties of a system — not by testing examples, but by proving (or disproving) that a property holds for all possible inputs. In SpecLogician, formal verification is performed by ImandraX, a symbolic reasoning engine based on the Imandra theorem prover.

What "formal" means here

SpecLogician's model is written in IML (Imandra Modeling Language), a typed functional language that compiles to executable code and is simultaneously amenable to symbolic reasoning. This dual nature is key:

• IML expressions are executable — they can be evaluated against concrete inputs
• IML expressions are analyzable — ImandraX can reason about them symbolically, considering all possible inputs at once

When ImandraX checks that a predicate conjunction is satisfiable, it's not sampling random inputs. It's solving a constraint satisfaction problem over the full space of possible states and actions. When it reports that two scenarios don't overlap, it has proved that no satisfying assignment exists — not merely failed to find one.

What gets verified

SpecLogician uses formal verification at every layer of the model:

IML validity

Every component (predicate, transition) is type-checked against the domain base. This is the most basic form of verification — it guarantees that the IML compiles and that field references, type comparisons, and return types are correct.

This catches errors like:

• Referencing a field that doesn't exist (s.balnce instead of s.balance)
• Comparing incompatible types (s.status = 42 when status is a variant type)
• Returning the wrong type from a transition (missing a field in the state record)

Satisfiability

For each scenario, ImandraX checks whether the conjunction of predicates is satisfiable — does there exist at least one state/action pair where all the predicates are true simultaneously?

This is a formal proof. If ImandraX reports that a conjunction is unsatisfiable, it means no such input exists — the scenario is logically contradictory. If it's satisfiable, ImandraX provides a witness: a concrete example that satisfies all predicates.

Scenario intersection

For each pair of scenarios, ImandraX checks whether their predicate conjunctions can be simultaneously satisfied. If yes, the scenarios overlap — there exists an input where both could fire. If no, the scenarios are disjoint — they cover non-overlapping regions of the input space.

Scenario implication

ImandraX checks whether one scenario's predicates logically imply another's — whether every input that satisfies scenario B also satisfies scenario A. If so, B is consumed by A.

Reachability

ImandraX checks whether, given a scenario's transition, the resulting state can satisfy another scenario's given predicates. This builds the reachability graph — a formal proof of which scenario-to-scenario transitions are possible.

Complement decomposition

ImandraX decomposes the negation of all scenario conjunctions into disjoint regions, formally characterizing the behavior space that no scenario covers.

Formal verification vs testing

Formal verification doesn't replace testing — it operates at a different level. Testing checks that the implementation behaves correctly for specific inputs. Formal verification checks that the model is internally consistent and has the properties you expect.

SpecLogician bridges the two through trace matching: concrete test traces and log traces are matched against formal scenarios, connecting implementation evidence to the verified model. See Traces and evidence for details.

The role of ImandraX

ImandraX handles all formal reasoning. SpecLogician constructs the queries — "is this conjunction satisfiable?", "do these scenarios intersect?", "what does the complement look like?" — and ImandraX solves them using a combination of:

• SAT/SMT solving — for satisfiability and intersection queries
• Region decomposition — for complement computation
• Symbolic execution — for reachability analysis

The results are deterministic and reproducible. The same model always produces the same analysis results.

What formal verification gives you

In practice, formal verification in SpecLogician provides:

1. Confidence in model correctness — if ImandraX says your scenarios don't overlap, they don't. Not "probably don't" or "don't for the cases I tested."
2. Automatic gap detection — the complement isn't a heuristic estimate of coverage. It's a mathematically precise characterization of what's missing.
3. Proof-backed safety/liveness — when ImandraX reports that a bad scenario is unreachable, it has proved that no sequence of transitions from the initial state can reach it.
4. Generated witnesses — for every satisfiability or intersection check, ImandraX can produce a concrete example. These witnesses serve as automatically generated test cases.