Differences from Imandra Core

ImandraX is a major evolution of Imandra Core. This page covers the key differences for users migrating from the older system.

User interface

Feature	Imandra Core	ImandraX
Primary interface	Jupyter notebooks, REPL	VS Code extension with LSP
Web interface	Jupyter-based	Native HTML-based
CLI	Limited	Full `imandrax-cli` with `check` and `serve-http`
Proof visualization	Text output	Goal state viewer in VS Code

Runtime and API access

Feature	Imandra Core	ImandraX
API protocol	Socket-based	HTTP REST API
Client libraries	Limited	Python (`imandra-core`) and OCaml
`[@@reflect]`	Available	Removed
`extract`	`Extract` module	Built-in `extract` command with Dune integration
Evaluation	OCaml toplevel	Built-in `eval` evaluator
OCaml runtime integration	Direct	Via HTTP API or extracted OCaml code

ImandraX removes [@@reflect] — you cannot reflect arbitrary OCaml values into the logic. Instead, ImandraX provides:

eval — A built-in evaluator for running IML models directly, without needing a separate "program mode"
extract — Generates OCaml source code from verified IML definitions, with Dune integration for building standalone executables

See Evaluation & Extraction for details.

Prelude and language

`List.fold_right`

In Imandra Core, List.fold_right used named arguments (~base). In ImandraX, it uses positional arguments:

(* Imandra Core *)
List.fold_right f xs ~base:init
 
(* ImandraX *)
List.fold_right f xs init

`Caml` module

The Caml module is removed in ImandraX.

In Imandra Core, Z.t aliased int and Q.t aliased real. In ImandraX, Q.t is not an alias for real — they are distinct types. ImandraX's real type is over the algebraic reals (users write rational constants, but reasoning treats them as algebraic reals).

New functions

Int.pow and Real.pow are now available
Various prelude functions have been refined

Import system

Imandra Core used multiple import mechanisms (use, mod_use, import, require). ImandraX unifies these into [@@@import]:

(* Imandra Core *)
#use "file.ml";;
#mod_use "file.ml";;
#require "package";;
 
(* ImandraX *)
[@@@import "file.iml"]
[@@@import Module, "file.iml"]

The new system supports path-based imports with OCamlFind and Dune package integration.

Unified tactic language

Imandra Core used attributes like [@@auto], [@@induct], [@@simp], [@@blast], [@@apply thm]. ImandraX replaces these with a unified tactic language using [@@by ...]:

(* Imandra Core *)
theorem foo x = P x [@@auto]
theorem bar x = Q x [@@induct x] [@@disable f]
theorem baz x = R x [@@apply (my_lemma x)]
 
(* ImandraX *)
theorem foo x = P x [@@by auto]
theorem bar x = Q x [@@by induction ~vars:["x"] () @>>| auto] [@@disable f]
theorem baz x = R x [@@by [%use my_lemma x] @> auto]

The tactic language is more expressive and composable. See Tactics.

Incremental proofs

Imandra Core processed definitions and proofs sequentially. ImandraX supports:

Parallel proof execution across multiple cores
Incremental checking — only re-verify changed dependencies
Prior-lemma assumptions — start using a lemma before its proof completes
Pervasive caching — avoid redundant work

Features not yet in ImandraX

Some Imandra Core features are not yet available in ImandraX:

upto_bounds for datatype-bounded unrolling
Some [@@blast] functionality (symbolic execution + SAT bit-blasting)
The Imandra Discover module for specification discovery

Check the latest release notes for updates on feature availability.