Key Concepts

This page provides a high-level overview of ImandraX's core concepts. Think of it as a roadmap — each concept is covered in depth in its own section of the documentation.

The Imandra Modelling Language (IML)

ImandraX programs are written in IML, a pure, higher-order subset of OCaml. If you know OCaml, Haskell, F#, or similar languages, IML will feel familiar.

What makes IML special is that it's simultaneously a programming language and a logic:

Every IML function is executable — you can run it, test it, debug it
Every IML function is also a logical definition that ImandraX can reason about formally
All functions must terminate on all inputs (this ensures logical consistency)
There are no side effects — no mutation, no I/O, no exceptions in the logic. This is no real restriction from a modelling perspective: impure aspects of a system can always be moved into the computational model, with state passed around explicitly (monadically)

(* This is both a runnable function AND a logical definition *)
let rec factorial n =
  if n <= 0 then 1
  else n * factorial (n - 1)

Learn more in the IML Language Guide.

Command	Purpose
`verify`	Check if a property holds for all inputs; find counterexamples if not
`instance`	Find an input satisfying a given property
`theorem`	State and prove a theorem (becomes available as a rewrite rule, etc.)
`lemma`	Like `theorem`, but primarily used as a stepping stone for other proofs
`axiom`	Assert a property without proof (use with caution — can introduce inconsistency)

Tactics

When ImandraX can't prove something fully automatically, you guide the proof with tactics. ImandraX has a unified tactic language with 45+ tactics that can be composed using combinators.

(* The waterfall handles most proofs automatically *)
theorem append_assoc x y z =
  (x @ y) @ z = x @ (y @ z)
[@@by auto]
 
(* Supply a lemma, then run auto *)
theorem my_theorem x y =
  some_property x y
[@@by [%use helper_lemma x] @> auto]

Key tactical combinators:

@> — sequence ("then")
<|> — alternative ("or")
@>>| — apply to all subgoals
@>| — apply different tactics to different subgoals

Learn more in Tactics.

The inductive waterfall

The waterfall is ImandraX's automated proof engine, inspired by the pioneering work of Boyer and Moore. When you write [@@by auto], the waterfall orchestrates a sophisticated pipeline:

Simplification — Rewrite using known lemmas and definitions
Unrolling — Bounded model checking (can find counterexamples)
Destructor elimination — Simplify pattern matching
Fertilization — Use inductive hypotheses
Generalization — Strengthen the goal to make induction applicable
Induction — Apply induction schemes derived from recursive definitions

Once you've used bounded verification to gain confidence that a goal is true, [@@by auto] will handle most proofs. When it doesn't, you use tactics to guide specific steps, then let the waterfall handle the rest.

Learn more in The Waterfall.

Counterexample synthesis and the verification workflow

When a property doesn't hold, ImandraX doesn't just say "false" — it synthesizes a concrete counterexample: a specific input that violates the property. Counterexamples are first-class executable values that you can inspect and compute with.

(* ImandraX finds: x = 0, y = 1 *)
verify (fun x y -> x + y > x)

This is powered by ImandraX's unrolling engine, which combines recursive function unrolling with ground decision procedures for arithmetic, datatypes, and congruence closure. Counterexample searching is extremely fast, giving you rapid feedback.

The recommended workflow in ImandraX is:

Start with bounded verification — Write a verify goal and let the default unrolling search for counterexamples
Study and eliminate counterexamples — Fix faulty logic in your models or conjectures, often by adding hypotheses or guards
Increase the bound — Once counterexamples disappear at low bounds, explore further with [@@by unroll 100] or higher
Only then prove — When no counterexamples exist up to a large bound, you have good evidence the goal is true and should attempt a proof with [@@by auto]

Most goals you write will initially be false. Bounded verification catches this quickly, saving you from spending time trying to prove something that isn't true.

Learn more in Counterexamples.

Region decomposition

Region decomposition is one of ImandraX's most distinctive capabilities. Given a function, it exhaustively decomposes the input space into disjoint regions, each with a distinct pattern of behavior.

This is invaluable for:

Test generation — Automatically generate test cases covering every behavioral region
Coverage analysis — Understand exactly how many distinct behaviors a function has
Regulatory compliance — Prove exhaustive coverage of business rules

Learn more in Region Decomposition.

Termination and consistency

Every function admitted into ImandraX's logic must be proved terminating. This isn't just a technicality — it's essential for logical consistency. A non-terminating function could be used to "prove" anything, making the entire logic unsound.

ImandraX uses ordinal-valued measures (ordinals up to ε₀) to prove termination. For simple structural recursions, termination is proved automatically. For more complex recursions, you provide a measure:

(* ImandraX proves termination automatically *)
let rec length = function
  | [] -> 0
  | _ :: xs -> 1 + length xs
 
(* Custom measure needed for non-structural recursion *)
let rec ackermann m n =
  if m = 0 then n + 1
  else if n = 0 then ackermann (m - 1) 1
  else ackermann (m - 1) (ackermann m (n - 1))
[@@measure Ordinal.(pair (of_int m) (of_int n))]

Learn more in Termination.

Incremental and parallel proofs

ImandraX's architecture is designed for large-scale verification:

Incremental checking — Only re-verify definitions and theorems whose dependencies changed
Parallel proof execution — Independent proofs run concurrently across multiple cores
Prior-lemma assumptions — Start using a lemma before its proof is complete

The VS Code extension takes full advantage of this: as you edit a file, only the affected proofs are re-checked, giving you fast feedback even in large projects.

Learn more in Incremental Proofs.

Cloud-native architecture & AI integration

ImandraX is foundational infrastructure for AI reasoning and AI governance, cloud-native from the ground up:

HTTP API — Integrate with any language or tool via REST endpoints
Python & OCaml clients — First-class client libraries for programmatic access
AI agent integration — Expose formal reasoning capabilities directly to LLM-powered agents and automated workflows
MCP server — Seamless integration with AI assistants
CI/CD — Use imandrax-cli check in your build pipeline

ImandraX is part of Imandra Universe, an ecosystem of reasoners and neurosymbolic AI integration. CodeLogician, our neuro-symbolic reasoning agent, demonstrates one way LLMs and formal reasoning combine — and the same APIs power custom AI reasoning workflows.

Learn more in the API Reference.