First steps with ImandraX

17 min readMay 8, 2025

This blog entry describes my experience of getting started with ImandraX using the VS Code ImandraX extension. I decided to take some functions and proofs I made when I was learning Agda a couple of years ago, and see
how they translate into ImandraX.

Quick background on ImandraX

ImandraX supports many approaches to formal verification, including a seamless integration of bounded and unbounded verification. Every goal can be attacked first with bounded verification (via the `[@@upto n]` annotation), and then subjected to unbounded verification (e.g., proof by induction with `auto` or via more nuanced tactics) only once all counterexamples found have been eliminated.

We always suggest beginning with bounded verification. Why? (1) Most conjectures one has about code are actually false, and finding counterexamples quickly is much more useful than wasting time trying to prove false goals. In ImandraX, all counterexamples are computable objects which are directly available for inspection, computation and experimentation. (2) In many practical engineering applications, bounded verification is sufficient, and with ImandraX’s `[@@upto n]` these bounded results can be made “first class” verification results which form a key part of safety cases.

In this article, I will explore unbounded verification via `auto` and other nuanced tactics. Here’s the complete model if you’d like to follow along.

Prequisites

It will help if you are familiar with the functional programming language OCaml, upon which Imandra Modelling Language (IML) is closely based.
Install ImandraX by running the install script in the Github repository. You can download and run it, or pipe it directly from the repo like this:
curl https://raw.githubusercontent.com/imandra-ai/imandrax-api/refs/heads/main/scripts/install.sh | bash
Get an ImandraX API key, e.g. by signing up to Imandra Universe at [https://universe.imandra.ai/]. Once you have it, save it in file called $HOME/.config/imandrax/api_key, where $HOME is your home directory.
Install Microsoft VS Code if you don’t have it already.
Install the VS Code ImandraX extension. When installed, it should look like this:

Some code to reason about

First we’ll create ourselves a new file in VS Code, and call it, for example, test.iml . Let’s then introduce a function to play with. We’re going to look at reversing lists. The first list reversing function, rev, is based on a simple structural recursion, where we pattern match on the two possible list constructors. It is sometimes called ‘naive’ reverse because it is (a) easily understood just by looking at it and (b) much slower : O(N²) in the length of the list , rather than the optimal O(N) method we will look at later.

let rec rev = function
 | [] -> []
 | x::xs -> rev xs @ [x]

Proving some properties of reverse

We would like to prove that reversing a list and then reversing the result reproduces the original list, that is, reverse is its own inverse. More formally, we want to prove that for any list x, rev (rev x) = x . From my experiences with Agda, I suspected that it would be useful to have a couple of lemmas available which prove that concatenation (the @ operator in OCaml and IML) is associative and reversal is ‘distributive’ in the sense that the reverse of the concatenation of two lists is the reverse concatenation of the reverses of the lists. However, before introducing the lemmas and exploring how ImandraX can make use of them, let’s see if ImandraX can prove the self-inverse theorem on its own. We encode it like this:

theorem rev_self_inverse x =
   rev (rev x) = x
[@@by auto]

When entered into VS Code, the ImandraX extension should decorate the function with ‘Check’ and ‘Browse’ clickable links. Clicking on ‘Check’ will tell ImandraX to try to prove the theorem below. Alternatively, from the menu, ‘File > Save’ (or Cmd-S) will save the file and check all the lemmas and theorems it contains. The result should look like this:

Successfully proven theorem in the VS Code editor

The little smiley face to the left indicates that the proof was successful. Clicking on the ‘Browse’ link should open another tab in VS Code containing a description of how ImandraX went about proving the theorem and how long it took.

Report on the proof of `rev_self_inverse`

We will examine this proof (by clicking on the triangle next to ‘view’) later, but for now let’s go back and introduce the two lemmas we mentioned earlier, before the main theorem, again relying initially on the automatic proof method that is built in to Imandra.

lemma append_assoc x y z =
   (x @ y) @ z = x @ (y @ z)
[@@by auto]

lemma rev_distrib x y =
   rev (x @ y) = rev y @ rev x
[@@by auto]

theorem rev_self_inverse x =
   rev (rev x) = x
[@@by auto]

Let’s browse the report on the proof of rev_distrib. We won’t go through the description in detail, but notice how long it took ImandraX to prove rev_distrib using the auto method (or ‘tactic’, as it’s called in ImandraX — more on tactics later). When I ran it, it took about 1.5 seconds, which is quite slow in the scheme of things. We will see what we can do to speed that up.

Speeding up the proof using lemmas

If you expand the ‘view’ triangle in the ‘Report’ section of the proof browser for rev_distrib, which lets you view a report of the reasoning done by Imandra’s inductive waterfall (auto) tactic, you might notice something which looks like the associativity proposition for list concatenation (represented by the function List.append here — in ImandraX, the @ operator is an infix macro that expands to an application of the List.append function). Buried in the description there is this:

which is a particular case of associativity for the three lists gen_2 , gen_1 and [x1] . ImandraX then goes on to prove this without using the lemma we carefully prepared above. If we can get it to use the already-proven general form of the lemma, we might save some time, and moreover, effectively ‘teach’ ImandraX how to reason more efficiently in this domain.

The way to do this is to tag the lemma as a ‘rewrite’ rule, which makes it available for use in the auto tactic. We do this by adding [@@rw] to the definition, like this:

lemma append_assoc x y z =
   (x @ y) @ z = x @ (y @ z)
[@@by auto] [@@rw]

We can then click ‘Check’ to refresh the definition and then ‘Check’ and ‘Browse’ again on rev_distrib to see what the effect is. For me, the proof time was reduced to about 450 ms, a distinct improvement!

Report on the sped-up proof of `rev_distrib` after making `append_assoc` a rewrite rule.

Examining the proof, we find this, showing that the automatic tactic did indeed find and use the lemma.

Part of the proof of `rev_distrib`, showing application of `append_assoc` rewrite rule

Looking further up the proof, we can also find this:

Part of the proof of `rev_distrib`, showing use of built-in `List.append_to_nil` rule

It turns out that the proof was already using a lemma defined in the ImandraX List module. This lemma, List.append_to_nil, states that, for any list x, List.append x [] = x . The snippet says that, assuming list x is not of the form _ :: _ , i.e. it’s an empty list [], we can conclude that right hand side (RHS) of the goal rev y @ rev x = rev y @ [] = rev y . Since the LHS, x @ y = [] @ y = y is true from the definition of List.append, ImandraX is able to reduce the goal to rev y = rev y, which is trivially true.

Let’s have a look at the proof of rev_self_inverse— as we noticed before introducing the lemmas, it goes through in about 740 ms without using rev_distrib, not surprisingly because we have not marked rev_distrib as available for rewriting. There is a point where rev_distrib could be applied, here:

Part of the proof of `rev_self_inverse` without using `rev_distrib` lemma

On the LHS of the goal, we have rev (List.append _ _). What happens if we make rev_distrib available for use? We add [@@rw] to the definition:

lemma rev_distrib x y =
   rev1 (x @ y) = rev y @ rev x
[@@by auto] [@@rw]

Saving and reviewing the proof of rev_self_inverse, we find:

Report on sped-up proof of `rev_self_inverse` after enabling use of `rev_distrib` lemma

Success! The proof time is down to about 250 ms, and expanding the report, we find exactly what we were hoping for:

Part of proof of `rev_self_inverse` showing use of `rev_distrib` rewrite rule

Weaning off the ‘auto’ proof tactic

When looking through the proof reports, you may get the impression (correctly) that ImandraX is somehow arriving at a long sequence of steps, often including nontrivial inductions and simplifications, each of which transforms the goals of the proof, until magically, at the end, the goal reduces to something which is trivially true and the proof is done. At each stage, there might be several transformations which could be applied, and ImandraX has to search through or use heuristics to find a sequence of steps which results in success. In this section, we will gradually reduce our reliance on the auto tactic, not because there’s anything wrong with using auto — it is an extremely powerful mechanism that is robust to semantics-preserving changes in the code. Rather, our purpose here pedagogical, and by learning how the various tactics work, we can use them judiciously to improve or direct harder proofs.

When building a proof manually, its very useful to be able to see the ‘state’ of a partial proof, i.e. goals that remain to be proved. To do this, you can either click on the search box at the top of the VS Code window and click on ‘Show and Run Commands’:

or press Shift-Cmd-P. Then type ‘ImandraX’ and choose ‘Open goal state’.

This should open a new panel called goal-state.md:

Now let’s start a new lemma called rev_distrib_manual , but instead of using the auto tactic, we’ll use skip. Important: we must also remove the [@@rw] annotation from our previous version of rev_distrib to prevent ImandraX from using rev_distrib to prove rev_distrib_manual, as this would rather defeat the point of the exercise!

lemma rev_distrib x y =
   rev (x @ y) = rev y @ rev x
[@@by auto] (* REMOVE [@@rw] *)

lemma rev_distrib_manual x y =
   rev (x @ y) = rev y @ rev x
[@@by skip]

Since skip doesn’t advance the proof at all, the proof fails:

However, if we look at the goal state, we see

We have goal to prove below the line and no hypotheses above it. We can reproduce the first step of the automatic proof by using the induction tactic. This will produce two subgoals, one for each case of a structural induction on one of the list arguments. The induction tactic must be composed with two further tactics to handle each of the cases. We are free to use auto for both of these, which results in a sucessful proof:

lemma rev_distrib_manual x y =
   rev (x @ y) = rev y @ rev x
[@@by induction ()
      @>| [auto; auto]]

For reference, this proof took about 425 ms for me.

When we invoke induction () on its own, ImandraX uses its induction heuristics (the same that are used by auto) to analyze the goal and synthesize an appropriate induction scheme. Unlike auto, however, induction () then simply returns the base and inductive cases as subgoals and lets us continue proving the goal manually. We can give induction instructions on which specific induction schemes we want, but in this case (and usually) we are happy to let it synthesize the appropriate induction scheme itself automatically.

By winding this back to just the induction step, we can get to see the two subgoals:

lemma rev_distrib_manual x y =
   rev (x @ y) = rev y @ rev x
[@@by induction ()]

The first subgoal, the base case, assumes the list x is empty, while the second assumes it’s not empty and an inductive hypothesis, which we can write more clearly without type decorations and using the @ operator instead of List.append:

rev (List.tl x @ y) = rev y @ rev (List.tl x)

Crucially, this is just the rev_distrib_manual lemma with x replaced with List.tl x. From now on I’ll illustrate the goal state not as a screenshot, but as text below the lemma code, without type decorations and using the @ operator.

The base case can be dealt with using the tactic simplify (). This can exploit function definitions and rewrite rules, but at this point, using it is no more enlightening than using auto, so let’s see we can do at a lower level. The normalize tactic can expand and simplify a target term using function definitions and hypotheses. We apply it to rev x in the first subgoal: since x = [] and rev [] is defined as [], the term reduces to [].

lemma rev_distrib_manual x y =
   rev (x @ y) = rev y @ rev x
[@@by induction ()
      @>| [ [%normalize rev x]
          ; auto
          ]]

 H0. x = []
|----------------------------------------------------------------------
 rev (x @ y) = rev y @ []

Similarly we can normalize x @ y using x = [] and the definition of List.append, to get x @ y = [] @ y = y . The two normalize steps are combined using the @> operator.

lemma rev_distrib_manual x y =
   rev (x @ y) = rev y @ rev x
[@@by induction ()
      @>| [    [%normalize rev x]
            @> [%normalize x @ y]
          ; auto
          ]]

 H0. x = []
|----------------------------------------------------------------------
 rev y = rev y @ []

We are quite close now. The built in List.append_to_nil lemma we found earlier can be applied with the use tactic to simplify the RHS:

lemma rev_distrib_manual x y =
   rev (x @ y) = rev y @ rev x
[@@by induction ()
     @>| [    [%normalize rev x]
           @> [%normalize x @ y]
           @> [%use List.append_to_nil (rev y)]
         ; auto
         ]]

 H0. x = []
 H1. rev y @ [] = rev1 y
|----------------------------------------------------------------------
 rev1 y = rev1 y @ []

Notice that this does not immediately simplify the goal — rather it inserts the hypothesis associated with the lemma above the line (H1 above). We can use the replace tactic to simplify a term using the hypotheses:

lemma rev_distrib_manual x y =
   rev (x @ y) = rev y @ rev x
[@@by induction ()
     @>| [    [%normalize rev x]
           @> [%normalize x @ y]
           @> [%use List.append_to_nil (rev y)]
           @> [%replace rev y @ []]
         ; auto
         ]]

 H0. x = []
|----------------------------------------------------------------------
 rev y = rev y

Finally, the trivial tactic deals with the final remaining tautology in the goal. If we add trivial to the chain and replace auto with skip for the second subgoal, we’ll complete the first subgoal and see what needs doing for the second.

lemma rev_distrib_manual x y =
   rev (x @ y) = rev y @ rev x
   [@@by induction ()
     @>| [    [%normalize rev x]
           @> [%normalize x @ y]
           @> [%use List.append_to_nil (rev y)]
           @> [%replace rev y @ []]
           @> trivial
         ; skip
         ]]

 H0. x <> []
 H1. rev (List.tl x @ y) = rev y @ (rev (List.tl x))
|----------------------------------------------------------------------
 rev (x @ y) = rev y @ rev x

We’ll start by using normalize on the LHS of the goal. From here on, for brevity, I’ll omit the List. qualifier when referring to the list head and tail functions hd and tl respectively.

lemma rev_distrib_manual x y =
    rev (x @ y) = rev y @ rev x
[@@by induction ()
    @>| [    [%normalize rev x]
          @> [%normalize x @ y]
          @> [%use List.append_to_nil (rev y)]
          @> [%replace (rev y) @ []]
          @> trivial 
        ;    [%normalize rev (x @ y)]
        ]]

 H0. x <> []
 H1. rev1 (tl x @ y) = rev y @ rev (tl x)
|----------------------------------------------------------------------
 rev (tl x @ y) @ [hd x] = rev y @ rev x

Next let’s normalize rev x in the RHS too:

lemma rev_distrib_manual x y =
    rev (x @ y) = rev y @ rev x
[@@by induction ()
    @>| [    [%normalize rev x]
          @> [%normalize x @ y]
          @> [%use List.append_to_nil (rev y)]
          @> [%replace (rev y) @ []]
          @> trivial 
        ;    [%normalize rev (x @ y)]
          @> [%normalize rev x]
        ]]

 H0. x <> []
 H1. rev (tl x @ y) = rev y @ rev (tl x)
|----------------------------------------------------------------------
 rev1 (tl x @ y) @ [hd x] = rev y @ (rev (tl x) @ [hd x])

Notice that we have a term rev (tl x @ y) in the LHS of the goal, and a hypothesis, the induction hypothesis in fact, about this term in H1 above the line. We can use H1 to rewrite the term in the goal using the replace tactic:

lemma rev_distrib_manual x y =
    rev (x @ y) = rev y @ rev x
[@@by induction ()
    @>| [    [%normalize rev x]
          @> [%normalize x @ y]
          @> [%use List.append_to_nil (rev y)]
          @> [%replace (rev y) @ []]
          @> trivial 
        ;    [%normalize rev (x @ y)]
          @> [%normalize rev x]
          @> [%replace rev (List.tl x @ y)]
        ]]

 H0. x <> []
|----------------------------------------------------------------------
 (rev y @ rev (tl x)) @ [hd x] = rev y @ (rev (tl x) @ [hd x])

Nearly there. Looks like all we need to do now is apply the append_assoc lemma to rewrite the LHS of the goal to match the RHS.

lemma rev_distrib_manual x y =
    rev (x @ y) = rev y @ rev x
[@@by induction ()
    @>| [    [%normalize rev x]
          @> [%normalize x @ y]
          @> [%use List.append_to_nil (rev y)]
          @> [%replace (rev y) @ []]
          @> trivial 
        ;    [%normalize rev (x @ y)]
          @> [%normalize rev x]
          @> [%replace rev (List.tl x @ y)]
          @> [%use append_assoc (rev y) (rev (List.tl x)) [List.hd x]]
        ]]

 H0. x <> []
 H1. (rev y @ rev (tl x)) @ [hd x] = rev y @ (rev (tl x) @ [hd x])
|----------------------------------------------------------------------
 (rev y @ rev (tl x)) @ [hd x] = rev y @ (rev (tl x) @ [hd x])

The goal is now the same as the hypothesis, so we can finish the proof by adding the trivial tactic:

lemma rev_distrib_manual x y =
    rev (x @ y) = rev y @ rev x
[@@by induction ()
    @>| [    [%normalize rev x]
          @> [%normalize x @ y]
          @> [%use List.append_to_nil (rev y)]
          @> [%replace (rev y) @ []]
          @> trivial 
        ;    [%normalize rev (x @ y)]
          @> [%normalize rev x]
          @> [%replace rev (List.tl x @ y)]
          @> [%use append_assoc (rev y) (rev (List.tl x)) [List.hd x]]
          @> trivial
        ]]

This time the proof succeeds, taking about 190 ms for me.

There are more things we can do to break down this proof into still smaller steps — for example, the normalize tactic is quite clever in how it exploits function definitions and hypotheses, and can be replaced with a more explicit sequence of operations — but we’ll leave that for now. It is also possible to explore how some of the proof steps can be reordered when they operate independently on different parts of the goal.

A more efficient list reversal method

In this section, we’ll introduce a new function rev_fast, which reverses lists more efficiently than rev. It is defined with the help of a tail recursive function shunt with an accumulator argument that simultanously tears down the input list while building up the reverse list, all in one pass through the elements of the list:

let rec shunt tail = function
    | [] -> tail
    | x::xs -> shunt (x::tail) xs

let rev_fast x = shunt [] x

Let’s see what we can prove about this function. Again, from my previous exploration of this topic in Agda, I knew that there is a useful lemma associated with shunt , which we can encode in ImandraX like this:

lemma shunt_lemma acc items =
   shunt acc items = rev1 items @ acc
[@@by auto] [@@rw]

It states that shunt reverses (according to our now verified and trusted definition of reverse rev) the given items and appends the list in the accumulator. Clearly, this is very close to proving that rev_fast produces the same result as rev. As we’ve already enabled shunt_lemma as a rewrite rule, let immediately try to prove that rev_fast x = rev x for all lists:

lemma rev_fast_eq_rev x =
   rev_fast x = rev x
[@@by auto]

This proof succeeds in about 30 ms, making use of both shunt_lemma and List.append_to_nil . Intuitively, if rev_fast produces the same result as rev , and rev is self-inverse, then rev_fast must be self-inverse. ImandraX can prove this by itself, in about 700 ms if we don’t make rev_self_inverse and rev_fast_eq_rev available as rewrite rules, or about 40 ms if we do. Let’s instead prove it manually:

lemma rev_fast_self_inverse x =
   rev_fast (rev_fast x) = x
[@@by skip]

|----------------------------------------------------------------------
 rev_fast (rev_fast x) = x

Instead of our previous approaches where we start by expanding terms using function definitions, let’s immediately use our rev_fast_eq_rev lemma:

lemma rev_fast_self_inverse x =
   rev_fast (rev_fast x) = x
[@@by [%use rev_fast_eq_rev x]]

 H0. rev_fast x = rev x
|----------------------------------------------------------------------
 rev_fast (rev_fast x) = x

Like when we used the List.append_to_nil lemma in an earlier proof, the goal is left unchanged but the lemma is inserted above the line. We can use replace to consume and apply it below the line:

lemma rev_fast_self_inverse x =
   rev_fast (rev_fast x) = x
[@@by [%use rev_fast_eq_rev x]
   @> [%replace rev_fast x]]
 
|----------------------------------------------------------------------
 rev_fast (rev x) = x

We’ll repeat the process to rewrite rev_fast (rev x):

lemma rev_fast_self_inverse x =
   rev_fast (rev_fast x) = x
[@@by [%use rev_fast_eq_rev x]        
   @> [%replace rev_fast x]
   @> [%use rev_fast_eq_rev (rev x)] 
   @> [%replace rev_fast (rev x)]

|----------------------------------------------------------------------
 rev (rev x) = x

The remaining goal is none other than the proposition of rev_self_inverse, so the proof is completed with a use and a trivial, and completes in under 1 ms:

lemma rev_fast_self_inverse x =
   rev_fast (rev_fast x) = x
[@@by [%use rev_fast_eq_rev x]       @> [%replace rev_fast x]
   @> [%use rev_fast_eq_rev (rev x)] @> [%replace rev_fast (rev x)]
   @> [%use rev_self_inverse x]
   @> trivial]

Note that there are many other ways to do this — for example, if we’d wanted to let ImandraX’s rewriter apply rev_fast_eq_rev automatically, we could have used the simplify or normalize tactics. Nevertheless, it’s useful to see how to do these various steps manually!

Going further

As mentioned at the end of the section on doing manual proofs, there are many ways to break down proofs into more elementary steps, and there are many more tactics that can be used. The best place to find an authoritative list of available tactics is in the ImandraX source code: if you right click on any of the tactics in the code in VS Code, and click on ‘Go to Definition’, VS Code will bring up prelude.iml in a new panel.