Frequently Asked Questions

General

What is ImandraX?

ImandraX is a cloud-native reasoning engine, programming language, theorem prover, and interactive proof assistant. It lets you write code in IML (a pure subset of OCaml), prove properties about your code, synthesize counterexamples when properties don't hold, and decompose function behavior into exhaustive regions.

How is ImandraX different from testing?

Testing checks specific inputs. ImandraX proves properties for all inputs — infinitely many of them. When you prove theorem sort_sorts xs = is_sorted (sort xs), you've verified correctness for every possible list, not just the ones you thought to test.

When a property is false, ImandraX goes beyond test failure messages: it synthesizes a concrete counterexample showing you exactly why.

How is ImandraX different from Lean, Coq, or Isabelle?

ImandraX has a more restricted logic equivalent to the computational subset of these systems — in which all models and goals are executable. Every function is a terminating program, and every theorem is a boolean-valued function that must return true for all inputs. There are no opaque existential quantifiers, no non-computable definitions, no proof-irrelevant terms.

This restriction is the key to ImandraX's automation. By giving up the generality of dependent type theory or full higher-order logic, ImandraX gains:

Automated inductive proofs — ImandraX's Boyer-Moore-style inductive waterfall means most true goals succeed with [@@by auto], with no manual tactic guidance
Counterexample synthesis — since every goal is executable, ImandraX can run it on symbolic inputs to find concrete counterexamples when properties fail. This powers the recommended workflow: first use fast bounded verification to find and eliminate counterexamples, then prove once you have confidence the goal is true. Most proof assistants only report "proof failed"
Region decomposition — automatic enumeration of all distinct behaviors of a function, a unique feature for exhaustive state-space analysis
Computational validation — every theorem can be tested on concrete inputs before attempting a proof

The mathematical content of ImandraX theorems is portable across foundational frameworks — see Logical Foundations for details.

What languages does ImandraX support?

ImandraX's native language is IML (Imandra Modelling Language), a pure subset of OCaml. The HTTP API and client libraries allow integration from Python, OCaml, and any language that can make HTTP requests.

Is ImandraX free?

ImandraX requires an Imandra Universe API key. There is a free tier available at universe.imandra.ai.

Language

Why can't I use mutation in IML?

IML is a logic — every function is a mathematical definition. Mutable state would make functions non-deterministic (f(x) could return different values at different times), breaking the ability to reason equationally.

Why must all functions terminate?

If a non-terminating function were accepted, its defining equation could derive contradictions (0 = 1), making the entire logic unsound. See Termination.

Can I use OCaml libraries?

IML can use the built-in prelude (List, Option, Map, Set, etc.) and any .iml files you import. You can extract verified IML code to OCaml and integrate it with OCaml libraries via dune.

Verification

My proof doesn't go through with `auto`. What do I do?

Common approaches:

Add rewrite lemmas — Prove helper lemmas with [@@rw] that guide simplification
Use [%use ...] — Explicitly supply a lemma instance
Guide induction — Specify the induction scheme with induction ~id:[%id f] ()
Break it up — Extract the hard part as a separate lemma

See the Interactive Proofs tutorial.

What does "Unknown (verified up to depth 100)" mean?

This means ImandraX's unrolling engine checked the property for inputs up to a certain complexity (roughly, recursive structures up to depth 100) and found no counterexample, but couldn't prove it for all inputs. You likely need induction — use theorem with [@@by auto] (which includes induction) or explicitly control it with [@@by induction () @>>| auto].

Can ImandraX prove properties about floating-point arithmetic?

ImandraX's real type represents the algebraic reals, not IEEE 754 floating-point. Users write rational constants as members of the type, but all reasoning treats them as algebraic reals. This is sound and complete for reasoning modulo polynomial constraints, since the theory of real closed fields (RCF) admits quantifier elimination and is a complete theory — you can't tell algebraic reals apart from actual reals. This avoids rounding and overflow issues entirely. For reasoning about actual IEEE 754 floating-point behavior, specialized techniques may be needed.