Counterexamples

When a property doesn't hold, ImandraX doesn't just say "false" — it synthesizes a concrete counterexample: a specific input that violates the property. Counterexamples are first-class executable values that you can inspect, compute with, and use to understand exactly how your specification fails.

How counterexamples work

When you run verify (fun x -> P x) and the property P is false for some input, ImandraX's unrolling engine finds a satisfying assignment to the negation not (P x) using its built-in decision procedures. This assignment is then reflected as a concrete IML value.

let rec sum = function
  | [] -> 0
  | x :: xs -> x + sum xs
 
(* Try: is sum always non-negative? *)
verify (fun xs -> sum xs >= 0)
(* Counterexample: xs = [-1] *)

The counterexample xs = [-1] is not just a diagnostic message — it's an actual IML value you can compute with.

Counterexamples as IML code

Every counterexample and instance is returned as a concrete IML definition — real executable code that defines the witness value. You can use eval to compute with it:

verify (fun x -> x * x <> 144)
(* Counterexample: x = 12 *)
 
(* Use eval to compute with the counterexample *)
eval CX.x           (* 12 *)
eval CX.x * CX.x    (* 144 *)

This is invaluable for debugging: you can trace through your function with the counterexample input to understand why the property fails.

Working with counterexamples in VS Code

In the VS Code extension, counterexamples and instances come with interactive controls:

Copy — Copies the IML definition of the counterexample value into your buffer as a module. You can then use eval to compute with these values alongside your other definitions.
Interact — Opens a REPL session where you can compute with the counterexample value and all your other definitions interactively. This lets you explore the counterexample by calling your functions on it, inspecting intermediate values, and understanding exactly how the property fails.

This workflow — find a counterexample, interact with it, understand the failure, fix the specification or code — is at the heart of productive ImandraX development.

Counterexamples with structured data

Counterexamples work with any IML type — records, algebraic datatypes, lists, nested structures:

type order = {
  price : real;
  quantity : int;
  side : Buy | Sell;
}
 
verify (fun (o : order) ->
  o.quantity > 0 ==> o.price *. Real.of_int o.quantity > 0.0)
(* Counterexample: o = { price = -1.0; quantity = 1; side = Buy } *)

The counterexample reveals a missing assumption: we didn't require price > 0.

Using `instance` for positive examples

The instance command is the positive counterpart of counterexample synthesis — it finds inputs satisfying a property:

instance (fun (xs : int list) ->
  List.length xs = 5
  && List.for_all (fun x -> x > 0 && x < 10) xs
  && sum xs = 25)
(* Instance: xs = [5; 5; 5; 5; 5] *)

This is useful for:

Test case generation — Automatically generate inputs satisfying complex constraints
Feasibility checking — Can this combination of constraints be satisfied at all?
Specification exploration — What do valid inputs actually look like?

Counterexamples in practice

Debugging specifications

Counterexamples are your best friend when developing specifications. Start with a conjecture, let ImandraX find counterexamples, refine your specification, repeat:

(* First attempt — too strong *)
verify (fun xs -> List.rev xs = xs)
(* CX: xs = [0; 1] — of course, most lists aren't palindromes *)
 
(* Second attempt — still wrong *)
verify (fun xs -> List.length (List.rev xs) > List.length xs)
(* CX: xs = [] — reversal doesn't increase length *)
 
(* Third attempt — correct! *)
verify (fun xs -> List.length (List.rev xs) = List.length xs)
(* Proved! *)

Edge case discovery

Counterexamples excel at finding edge cases you might not think of:

let safe_head xs default =
  match xs with
  | [] -> default
  | x :: _ -> x
 
verify (fun xs default ->
  safe_head xs default <> default ==> xs <> [])
(* Counterexample: xs = [0], default = 0 *)

The counterexample reveals: when the first element equals the default, safe_head xs default = default even though xs is non-empty. The specification was too weak.

Counterexamples and the verification workflow

A productive ImandraX workflow often looks like:

Conjecture — Write a verify statement
Counterexample — ImandraX finds a violation → refine your conjecture or fix your code
Unknown — Verified up to a bound but not proved → add lemmas and try theorem with tactics
Proved — The property holds universally → install as a rewrite or forward-chaining rule

Counterexamples are the feedback loop that makes this workflow effective. They turn abstract reasoning into concrete debugging.