ImandraX

ImandraX is foundational infrastructure for AI reasoning and AI governance — a cloud-native reasoning engine, programming language, theorem prover and interactive proof assistant that integrates directly into AI agents and automated workflows. It enables developers, researchers and AI agents to prove that code is correct, synthesize counterexamples when it isn't, and decompose complex systems into exhaustive, human-readable regions of behavior.

ImandraX is part of Imandra Universe, an ecosystem of reasoners and neurosymbolic AI integration. CodeLogician, our neuro-symbolic reasoning agent, demonstrates how LLMs and formal reasoning combine to analyze software with mathematical precision — and ImandraX's HTTP API, Python libraries and MCP server make it straightforward to build your own AI-powered reasoning workflows.

Built on decades of research in automated reasoning, drawing from the Boyer-Moore tradition, higher-order logic, and modern decision procedures, ImandraX's logic is a pure, higher-order subset of OCaml with proof-theoretic strength equivalent to computational HOL extended with transfinite induction up to ε₀.

Prove & Refute

Automatically prove theorems about your code — or synthesize concrete counterexamples when properties don't hold. Counterexamples are first-class executable values you can inspect and compute with.

Region Decomposition

Decompose the input space of any function into exhaustive, disjoint regions of behavior. A unique capability for test generation, coverage analysis and regulatory compliance.

Cloud-Native & AI-Ready

A multicore, incremental architecture with an HTTP API, Python and OCaml client libraries, and seamless integration with AI agents and LLM-powered workflows.

Interactive Proof Assistant

A rich tactic language with 45+ tactics, a VS Code extension with goal state visualization, and incremental parallel proof checking for fast feedback.

The Inductive Waterfall

A powerful automated proof pipeline inspired by Boyer-Moore: simplification, unrolling, destructor elimination, fertilization, generalization and induction — all working together.

Battle-Tested

Used in production for verifying financial systems, trading algorithms, regulatory compliance engines and safety-critical infrastructure.

A taste of ImandraX

Here's a quick example showing ImandraX in action. We define a simple function and ask ImandraX to verify a property about it:

(* Define a function that reverses a list *)
let rec rev = function
  | [] -> []
  | x :: xs -> rev xs @ [x]
 
(* Ask: is reversing a list always the identity? *)
verify (fun xs -> rev xs = xs)

ImandraX instantly finds a counterexample: xs = [0; 1]. Indeed, rev [0; 1] = [1; 0] ≠ [0; 1]. This is the power of counterexample synthesis — ImandraX doesn't just say "no", it shows you why.

Now let's prove something true. With a helper lemma, ImandraX can prove that reversing a list twice gives back the original:

(* First, a lemma about rev and append *)
theorem rev_append x xs = rev (xs @ [x]) = x :: rev xs
[@@by auto]
 
(* Now prove: rev (rev xs) = xs *)
theorem rev_rev xs = rev (rev xs) = xs
[@@by auto]

Get started

New to ImandraX?

Start with the Getting Started guide to install ImandraX and write your first proof in under 5 minutes.

Learn the language

The IML Language Guide covers everything about the Imandra Modelling Language — from basic types and pattern matching to termination proofs and the module system.

Master verification

Dive deep into Verification to learn about tactics, the inductive waterfall, region decomposition, and the full power of ImandraX's proof engine.

See it in action

Browse Tutorials for hands-on walkthroughs, or explore the Examples Gallery and the 100 Theorems Project.