The Verification Workflow

In Your First Proof, you saw the basics: defining functions, finding counterexamples, and proving theorems. Now let's see the full verification workflow in action — the process experienced ImandraX users follow every day.

We'll build a transaction processor, find a real bug, fix it, and then prove it correct — first for bounded inputs (where everything is decidable), and then for arbitrary inputs using induction.

Part 1: The Bounded World

Defining the problem

A transaction is either a deposit or a withdrawal:

type tx =
  | Deposit of int
  | Withdraw of int

Here's our first attempt at processing a transaction:

let apply_v1 bal tx =
  match tx with
  | Deposit n -> bal + n
  | Withdraw n -> bal - n

Straightforward enough. Now let's state the property we care about: if you start with a non-negative balance, it should stay non-negative.

verify (fun bal tx -> bal >= 0 ==> apply_v1 bal tx >= 0)

The counterexample

ImandraX instantly finds a counterexample:

Counter-model:
  bal = 0
  tx = Deposit (-7720)

Wait — a negative deposit? We never considered that. This is the power of counterexample synthesis: ImandraX doesn't just test the cases you thought of, it systematically searches for any input that violates your property.

Let's use eval to understand the problem:

eval (apply_v1 0 (Deposit (-100)))
(* Result: -100 *)
 
eval (apply_v1 100 (Withdraw 200))
(* Result: -100 *)

There are actually two bugs:

1. Deposits with negative amounts decrease the balance
2. Withdrawals aren't checked against the available balance

Fixing the function

let apply bal tx =
  match tx with
  | Deposit n  -> if n > 0 then bal + n else bal
  | Withdraw n -> if n > 0 && n <= bal then bal - n else bal

Now invalid transactions are simply rejected — the balance stays unchanged. Let's verify this is correct:

eval (apply 0 (Deposit (-100)))
(* Result: 0 — negative deposit rejected *)
 
eval (apply 100 (Withdraw 200))
(* Result: 100 — overdraft rejected *)
 
eval (apply 100 (Withdraw 50))
(* Result: 50 — valid withdrawal *)
 
eval (apply 100 (Deposit 25))
(* Result: 125 — valid deposit *)

Bounded verification

Now let's verify our property again:

verify (fun bal tx -> bal >= 0 ==> apply bal tx >= 0)

Proved! With a single transaction, there are only finitely many cases to consider (two variants of tx, each with a few branches), so ImandraX's unrolling engine handles this entirely automatically. No induction needed — this is a decidable property.

What about multiple transactions? Since the inputs are still finite, these are all decidable too:

(* Two transactions *)
verify (fun bal t1 t2 ->
  bal >= 0 ==> apply (apply bal t1) t2 >= 0)
 
(* Three transactions *)
verify (fun bal t1 t2 t3 ->
  bal >= 0 ==> apply (apply (apply bal t1) t2) t3 >= 0)

All proved automatically — no tactics or induction needed.

Note that "bounded" here is nuanced. These functions still involve integers, which are unbounded. But the computation over those integers is bounded — there's no recursion, just a fixed number of function applications. The arithmetic reasoning itself is handled by efficient decision procedures for theories like Presburger arithmetic (linear integer arithmetic). So the key idea is bounded recursion modulo decidable background theories: ImandraX iteratively expands function definitions with tightly integrated ground decision procedures for arithmetic, datatypes, and equality — combining symbolic expansion and logical reasoning at each step.

Importantly, when we say ImandraX "explores all cases," it doesn't enumerate concrete values or run tests. It reasons symbolically — using logic to cover the entire input space at once. A single symbolic proof covers infinitely many concrete inputs (all integers, both transaction variants, etc.).

Part 2: Going Unbounded

The need for induction

In reality, we need to process an arbitrary number of transactions — not just 1, 2, or 3. Let's define a recursive processor:

let rec process bal txs =
  match txs with
  | [] -> bal
  | tx :: rest -> process (apply bal tx) rest

We can compute with it:

eval (process 100 [Deposit 50; Withdraw 30; Withdraw 20])
(* Result: 100 *)
 
eval (process 100 [Withdraw 200; Deposit 50])
(* Result: 150 — the Withdraw 200 is rejected, then Deposit 50 succeeds *)

Now, does our safety property still hold for any list of transactions? Let's start with a bounded check using [@@upto 100], which verifies the property for all inputs up to unrolling depth 100. This produces a proper bounded theorem — if a counterexample exists within the bound, it will be found:

verify (fun bal txs -> bal >= 0 ==> process bal txs >= 0) [@@upto 100]

This succeeds — the property holds for all transaction lists up to a substantial depth. That's strong evidence it's universally true. But it's still only a bounded result. Can we prove it for all lists, no matter how long?

A plain verify without [@@upto] reaches the default unrolling limit without finding a counterexample or a proof:

unroll failed to prove goal.
Result is: (R_unknown { reason = "max number of steps (100) reached" })

This is the fundamental boundary between the bounded and unbounded worlds. Unrolling can check finitely many cases, but a list could be any length. To prove this for all lists, we need induction.

Declarative proof with auto

ImandraX's inductive waterfall (auto) can handle this entirely on its own:

theorem process_safe bal txs =
  bal >= 0 ==> process bal txs >= 0
[@@by auto]

Proved! The waterfall automatically:

1. Identifies that induction on txs is needed
2. Generates a base case (txs = []) and an inductive step (txs = tx :: rest)
3. Simplifies using the definitions and the induction hypothesis
4. Closes both subgoals

This is a universal result: for any starting balance bal >= 0 and any list of transactions txs, the balance never goes negative. No helper lemmas were needed — auto discovered the full proof by itself, including the case analysis on the transaction type in the inductive step.

Interactive proof with tactics

The waterfall is powerful — and it's not a black box. When auto succeeds, it produces a readable proof trace (available in the VS Code goal state viewer) showing every step: which induction scheme it chose, which lemmas it applied, how it simplified each subgoal. But sometimes you need to surgically control the reasoning yourself — instantiating specific lemmas with precise arguments, choosing particular induction schemes, or applying targeted simplification. Interactive tactic-based proofs give you this fine-grained control.

Let's also take this opportunity to extract a reusable lemma — any proved theorem or lemma can be installed as a rewrite rule, forward-chaining rule, or explicitly instantiated in other proofs, regardless of how it was proved.

Let's start by extracting a key insight as a lemma: each individual transaction preserves non-negativity.

lemma apply_non_neg bal tx =
  bal >= 0 ==> apply bal tx >= 0

This captures the core single-step invariant. Now let's prove the theorem interactively, controlling the proof structure ourselves and explicitly supplying this lemma where it's needed. The proof has two parts:

• Base case (txs = []): process bal [] = bal, so the goal becomes bal >= 0 ==> bal >= 0 — a tautology.
• Inductive step (txs = tx :: rest): Assuming the property holds for rest, prove it holds for tx :: rest.

We use induction () to set up the induction, then handle each subgoal with @>|:

theorem process_safe_interactive bal txs =
  bal >= 0 ==> process bal txs >= 0
[@@by
  induction ()
  @>| [
    (* Base case: normalize process on the empty list, then it's a tautology *)
    [%norm process bal txs] @> tauto;
    (* Inductive step: supply the lemma for the head transaction, then auto *)
    [%use apply_non_neg bal (List.hd txs)] @> auto
  ]
]

Let's break this down:

• induction () — ImandraX analyzes the goal, synthesizes an appropriate induction scheme (here, structural induction on txs), and produces two subgoals: the base case and the inductive step.

• @>| — The "split" combinator. It lets you apply a different tactic to each subgoal: the first tactic for the first subgoal, the second for the second.

• [%norm process bal txs] — Normalize the term process bal txs in the current goal. In the base case, txs is empty, so this evaluates process bal [] to bal, making the goal bal >= 0 ==> bal >= 0.

• @> — The "then" combinator. It sequences tactics: do the first, then pass the result to the second.

• tauto — Closes goals that are propositional tautologies. After normalization, the base case is bal >= 0 ==> bal >= 0, which is exactly a tautology.

• [%use apply_non_neg bal (List.hd txs)] — Explicitly instantiate our lemma for the first transaction in the list (List.hd txs), adding it as a hypothesis in the goal. This tells ImandraX: "use the fact that applying the head transaction to a non-negative balance stays non-negative."

• auto — With the lemma available as a hypothesis, the waterfall handles the remaining case analysis on the transaction type, applies the induction hypothesis for the tail, and closes the goal.

Summary

Here's the complete verified file — you can copy this into a .iml file and check it with ImandraX:

type tx =
  | Deposit of int
  | Withdraw of int
 
let apply bal tx =
  match tx with
  | Deposit n  -> if n > 0 then bal + n else bal
  | Withdraw n -> if n > 0 && n <= bal then bal - n else bal
 
let rec process bal txs =
  match txs with
  | [] -> bal
  | tx :: rest -> process (apply bal tx) rest
 
(* Declarative: auto discovers the full proof *)
theorem process_safe bal txs =
  bal >= 0 ==> process bal txs >= 0
[@@by auto]
 
(* A reusable lemma capturing the single-step invariant *)
lemma apply_non_neg bal tx =
  bal >= 0 ==> apply bal tx >= 0
 
(* Interactive: explicit induction with lemma instantiation *)
theorem process_safe_interactive bal txs =
  bal >= 0 ==> process bal txs >= 0
[@@by
  induction ()
  @>| [
    [%norm process bal txs] @> tauto;
    [%use apply_non_neg bal (List.hd txs)] @> auto
  ]
]

You've now seen the full ImandraX workflow:

What's next?

• Key Concepts — A roadmap of all ImandraX capabilities
• Tactics — The full tactic language
• Tutorials — Verified sorting algorithms, compilers, hardware, and more
• Examples Gallery — 20+ verified examples to study and modify