Your First Proof

In this walkthrough, you'll experience the core of ImandraX: defining functions, discovering counterexamples, and proving theorems. We'll work through a series of small examples that build on each other.

Defining functions

Create a new file called first.iml and open it in VS Code. Let's start with some simple functions:

(* A function that doubles its input *)
let double x = x + x
 
(* A function that computes the absolute value *)
let abs x = if x >= 0 then x else -x

ImandraX will process these definitions and check that they terminate (more on this in the Language Guide). You'll see green indicators in VS Code confirming the definitions were accepted.

Finding counterexamples with verify

The verify command asks ImandraX to check whether a property holds for all inputs. If it doesn't, ImandraX will find a concrete counterexample.

(* Is double always positive? *)
verify (fun x -> double x > 0)

ImandraX quickly responds with a counterexample: x = 0. Indeed, double 0 = 0, which is not greater than 0. This is the power of counterexample synthesis — ImandraX doesn't just say "no", it shows you exactly why.

Let's try another:

(* Is double always at least as large as its input? *)
verify (fun x -> double x >= x)

This time ImandraX responds with a counterexample: x = -1. When x is negative, double x = 2x < x. We need to be more precise about what we're claiming.

Proving theorems

When a property really is true, ImandraX can prove it — establishing that it holds for every possible input, not just the ones it happened to test.

(* For non-negative x, double x is at least x *)
theorem double_geq x =
  x >= 0 ==> double x >= x

ImandraX proves this automatically. The ==> operator is logical implication: "if x >= 0, then double x >= x".

Working with data structures

ImandraX really shines when reasoning about recursive functions over data structures. Let's define a list reversal function and reason about it:

(* Reverse a list *)
let rec rev = function
  | [] -> []
  | x :: xs -> rev xs @ [x]
 
(* Is reversing a list the identity? *)
verify (fun xs -> rev xs = xs)

ImandraX finds a counterexample: xs = [0; 1]. Of course — reversing [0; 1] gives [1; 0].

But reversing twice does give back the original list. To prove this, we need a helper lemma:

(* A key lemma about how rev distributes over append *)
theorem rev_append x xs =
  rev (xs @ [x]) = x :: rev xs
[@@by auto]
 
(* Now we can prove: rev (rev xs) = xs *)
theorem rev_rev xs =
  rev (rev xs) = xs
[@@by auto]

Here we see tactics for the first time. The [@@by ...] annotation tells ImandraX how to prove the theorem. In this case, auto invokes the full inductive waterfall — ImandraX's flagship automated proof procedure. It handles simplification, induction, forward-chaining and more, all automatically.

Finding instances with instance

Sometimes you want to find an input that satisfies a property, rather than checking if all inputs satisfy it. The instance command does this:

(* Find a list that's a palindrome of length 3 *)
instance (fun (xs : int list) ->
  List.length xs = 3 && rev xs = xs)

ImandraX finds a satisfying instance, such as xs = [0; 0; 0].

Higher-order counterexample synthesis

One of ImandraX's most striking capabilities is its ability to synthesize counterexamples involving unknown functions. This goes far beyond what traditional SMT solvers can do — ImandraX can be seen as a lifting of SMT to a typed, higher-order setting with recursion and induction.

(* Can we find a function f and a list xs such that
   mapping f over the reverse of xs gives [1; 2; 3]? *)
instance (fun f (xs : int list) ->
  List.map f (rev xs) = [1; 2; 3])

ImandraX synthesizes both a concrete list xs and a concrete function f satisfying the constraint:

Instance (satisfiable):
  f = fun x -> if x = 3 then 1 else if x = 2 then 2 else 3
  xs = [3; 2; 1]

The synthesized function f is fully executable — you can copy it, apply it to other inputs, and compute with it directly:

(* We can use the synthesized values to verify the result *)
let f x = if x = 3 then 1 else if x = 2 then 2 else 3
eval List.map f (rev [3; 2; 1])
(* Result: [1; 2; 3] *)

This is a key difference from systems that only report "satisfiable" or "proof failed" — ImandraX gives you concrete, computable witnesses that you can interact with, test, and build upon. In VS Code, every counterexample and instance comes with Copy and Interact buttons, letting you paste the synthesized values directly into your development.

Let's try something more ambitious — finding a function and list satisfying multiple constraints simultaneously:

(* Find f and xs where mapping f produces a specific pattern *)
instance (fun f (xs : int list) ->
  List.length xs >= 3
  && List.map f xs = List.map (fun x -> x * 2) xs
  && List.hd xs > 5)

ImandraX finds concrete values for both f and xs, synthesizing a function that agrees with doubling on the relevant inputs. This higher-order reasoning works with polymorphism too — in a system where every proposition is a computable function, counterexample synthesis naturally extends to finding functional witnesses.

Exploring the goal state viewer

If you're using the VS Code extension, click on a theorem to open the Goal State Viewer. This shows you:

• The current proof obligations (goals)
• The hypotheses available in each goal
• How tactics transform the proof state step by step

Try clicking on rev_rev and stepping through the induction. You'll see how ImandraX breaks the proof into a base case (xs = []) and an inductive step, then applies the rev_append lemma automatically.

What's next?

You've just experienced the core workflow of ImandraX:

1. Define functions in a pure subset of OCaml
2. Verify properties — get counterexamples when they fail
3. Prove theorems — with automation and tactics
4. Find instances — synthesize inputs satisfying constraints

From here, you can:

• Learn the IML language in depth
• Explore verification techniques — tactics, the waterfall, induction
• Work through tutorials with real verified algorithms
• Browse the examples gallery for inspiration