Verification Commands

ImandraX provides five core commands for reasoning about your code. Each serves a distinct purpose in the verification workflow.

verify

The verify command checks whether a property holds for all inputs. If it doesn't, ImandraX synthesizes a concrete counterexample. Goals in ImandraX are boolean-valued functions, and with verify you simply pass an anonymous lambda or the name of a defined function:

(* Does this hold for all x? *)
verify (fun x -> x + 1 > x)
(* Proved *)

(* Does this hold for all x? *)
verify (fun x -> x * x > 0)
(* Counterexample: x = 0 *)

verify is a primary tool for checking conjectures. Use it to:

• Validate properties before committing to a theorem
• Find edge cases in your definitions
• Explore the behavior of functions

Like theorem and lemma, verify supports the [@@by tactic] annotation to guide the proof:

verify (fun x y -> (x @ y) @ [] = x @ y) [@@by auto]

With hypotheses

Use ==> (implication) to add preconditions:

verify (fun x -> x > 0 ==> x * x > 0)
(* Proved *)

With multiple variables

verify (fun x y -> List.length (x @ y) = List.length x + List.length y)
(* Proved *)

Bounded verification with [@@upto n]

The [@@upto n] attribute (available only for verify) performs bounded verification up to unrolling depth n, producing an actual bounded theorem as its result. It uses a version of unrolling that is complete for counterexample finding in a precise sense — if a counterexample exists within the bound, it will be found:

verify (fun (xs : int list) ->
  List.length xs = List.length (List.rev xs))
[@@upto 100]

This is valuable when a property is true but requires induction to prove in general. Bounded verification with [@@upto] gives you strong evidence before investing in a full proof.

With type annotations

When ImandraX needs help inferring types:

verify (fun (xs : int list) -> List.rev (List.rev xs) = xs)

instance

The instance command finds a concrete input that satisfies a property. It answers: "Give me an example where this is true."

instance (fun x -> x * x = 144)
(* Instance found: x = 12 *)

instance (fun (xs : int list) ->
  List.length xs = 3 && List.for_all (fun x -> x > 0) xs)
(* Instance found: xs = [1; 1; 1] *)

instance is invaluable for:

• Generating test cases
• Finding inputs satisfying complex constraints
• Exploring the space of valid inputs for a function

Combining constraints

instance (fun x y ->
  x > 0 && y > 0 && x + y = 10 && x * y > 20)
(* Instance found: x = 5, y = 5 *)

theorem

The theorem command states and proves a named result. Once proved, a theorem is available for use in subsequent proofs.

theorem append_nil xs =
  xs @ [] = xs
[@@by auto]

Theorems differ from verify in that they:

• Have a name that can be referenced later
• Can be installed as rewrite rules, forward-chaining rules, etc.

With tactics

The [@@by ...] annotation specifies how to prove the theorem:

theorem rev_rev xs =
  rev (rev xs) = xs
[@@by auto]

As rewrite rules

Install a theorem as a rewrite rule with [@@rw]:

theorem append_nil xs =
  xs @ [] = xs
[@@by auto] [@@rw]

Now whenever the simplifier sees <expr> @ [], it will rewrite it to <expr>.

As forward-chaining rules

Install as a forward-chaining rule with [@@fc]:

theorem length_non_neg xs =
  (List.length xs [@trigger]) >= 0
[@@by auto] [@@fc]

The [@trigger] annotation tells the simplifier which term to match on.

lemma

The lemma command is syntactically identical to theorem. It's conventionally used for intermediate results — stepping stones toward a bigger theorem:

(* A helper lemma *)
lemma insert_preserves_sorted a xs =
  is_sorted xs ==> is_sorted (insert a xs)
[@@by auto] [@@rw]
 
(* The main theorem, which uses the lemma *)
theorem insertion_sort_sorts xs =
  is_sorted (insert_sort xs)
[@@by auto]

The distinction between theorem and lemma is purely stylistic — they have identical behavior.

axiom

The axiom command asserts a property without proof. The assertion is accepted unconditionally and can be used in subsequent reasoning.

axiom hash_deterministic x =
  hash x = hash x
 
axiom hash_range x =
  hash x >= 0 && hash x < 1000000

When to use axioms

• Modelling external systems whose implementation you don't control
• Constraining [@@opaque] functions with known properties
• Temporarily assuming a property to focus on the rest of a proof

Summary