Differences with Imandra Core

Imandra and ImandraX share a common heritage as formal verification and theorem-proving tools. Both use an OCaml-based syntax, share a foundational logic, and feature powerful reasoning techniques.

However, ImandraX introduces several significant enhancements that address the limitations of its predecessor.

Imandra primarily relied on a REPL-based interface, whereas ImandraX offers a suite of modern tools for enhanced usability:

  • Native HTML-based user interface for visualizing the state of ImandraX sessions.
  • VSCode plugin tightly integrated with the HTML UI and optimized for interactive development.
  • Command-line interface (CLI) for non-interactive use.
  • HTTP-based API server with companion OCaml and Python libraries.

CLI

The CLI allows users to check all theorems in a file using:

imandrax-cli check file.iml

This functionality is particularly useful for CI integration and general non-interactive workflows.

VSCode Plugin

The VSCode plugin utilizes an LSP server to interface with ImandraX.

Unlike Imandra, ImandraX implements pervasive caching and incremental proofs. Theorems are only rechecked when necessary, significantly improving performance and ergonomics in multi-file projects. Users can choose to validate individual theorems on demand or all theorems upon saving a file.

These improvements streamline development by:

  • Reducing redundant proof computations.
  • Accelerating the feedback loop during proofs.
  • Enhancing usability in large codebases.

ImandraX departs from Imandra by removing support for OCaml runtime integration and reflection features (e.g., [@@reflect] and Extract modules). Instead, it provides API access via a first-class HTTP server and Python/OCaml libraries with built-in serialization/deserialization for binary-encoded artifacts.

This shift improves modularity and promotes a cleaner separation between the reasoning engine and application logic.

To start the API server, use:

imandrax-cli serve-http -p 8000

The Python library can connect to the server as follows:

>>> import imandrax_api
>>> c = imandrax_api.Client('http://localhost:8000')
>>> c.eval_src('let f x = List.rev (List.rev x)')
success: true

>>> res = c.verify_src('fun x -> x = f x', hints='[@@by auto]')
>>> res
proved {
  proof_pp: "..omitted."
}
>>> res = c.instance_src('fun (x, y) -> x > y')
>>> res
sat {
  model {
    m_type: Instance
    src: "module M = struct\n\n  let _x_1_18 = (1, 0)\n\n end\n"
    artifact {
      kind: "cir.model"
      data: "..omitted.."
      api_version: "v8"
    }
  }
}

Artifacts can be decoded into first-class values. For example, an AST representation of the extracted model can be obtained as follows:

>>> import imandrax_api.lib as xtypes
>>> artifact = res.sat.model.artifact
>>> xtypes.read_artifact_data(data=artifact.data, kind=artifact.kind)
Model(tys=[], consts=[(Cir_Applied_symbol(sym=Cir_Typed_symbol(id=Uid(name='_x_1_18', view=Uid_view_Generative(id=6899, gen_kind=Uid_gen_kind_Local())), ty=Cir_Type_schema(params=[], ty=Cir_Type(view=Ty_view_view_Tuple(arg=[Cir_Type(view=Ty_view_view_Constr(args=(Uid(name='int', view=Uid_view_Builtin(kind=Builtin_data_kind_Logic_core(logic_core_name='mk_s_int'))), []))), Cir_Type(view=Ty_view_view_Constr(args=(Uid(name='int', view=Uid_view_Builtin(kind=Builtin_data_kind_Logic_core(logic_core_name='mk_s_int'))), [])))])))), args=[], ty=Cir_Type(view=Ty_view_view_Tuple(arg=[Cir_Type(view=Ty_view_view_Constr(args=(Uid(name='int', view=Uid_view_Builtin(kind=Builtin_data_kind_Logic_core(logic_core_name='mk_s_int'))), []))), Cir_Type(view=Ty_view_view_Constr(args=(Uid(name='int', view=Uid_view_Builtin(kind=Builtin_data_kind_Logic_core(logic_core_name='mk_s_int'))), [])))]))), Cir_With_ty(view=Cir_Term_view_Tuple(l=[Cir_With_ty(view=Cir_Term_view_Const(arg=Const_Const_z(arg=1)), ty=Cir_Type(view=Ty_view_view_Constr(args=(Uid(name='int', view=Uid_view_Builtin(kind=Builtin_data_kind_Logic_core(logic_core_name='mk_s_int'))), [])))), Cir_With_ty(view=Cir_Term_view_Const(arg=Const_Const_z(arg=0)), ty=Cir_Type(view=Ty_view_view_Constr(args=(Uid(name='int', view=Uid_view_Builtin(kind=Builtin_data_kind_Logic_core(logic_core_name='mk_s_int'))), []))))]), ty=Cir_Type(view=Ty_view_view_Tuple(arg=[Cir_Type(view=Ty_view_view_Constr(args=(Uid(name='int', view=Uid_view_Builtin(kind=Builtin_data_kind_Logic_core(logic_core_name='mk_s_int'))), []))), Cir_Type(view=Ty_view_view_Constr(args=(Uid(name='int', view=Uid_view_Builtin(kind=Builtin_data_kind_Logic_core(logic_core_name='mk_s_int'))), [])))]))))], funs=[], representable=True, completed=True, ty_subst=[])

The OCaml API offers to_iml and of_cir deriving drivers that, together with the imandrax-cli extract command, emulate Imandra’s [@@reflect] and Extract.

Example

For a file model.iml:

type t = { x : string; y : int }

let goal (x : t) = x.x = "foo"

Extract it to an OCaml file:

imandrax-cli extract --deriving to_iml --deriving of_cir model.iml > model.ml

A typical Dune stanza for this would look like:

(dialect
 (name imandrax)
 (implementation
  (extension iml)
  (preprocess
   (system "imandrax-cli extract --deriving to_iml --deriving of_cir %{input-file}"))))

Then from an OCaml program compiled against model.ml and Imandrax_api, connect to the server:

module C = Imandrax_api_client_ezcurl
module Artifact = Imandrax_api_artifact.Artifact
let c : C.t = C.create ~tls:false ~auth_token:None ~host:"localhost" ~port:8000 ()
let session = C.get_session c

To simulate [@@reflect], simply instantiate a value of Model.t, invoke to_iml on it and then eval:

let my_val = Model.{ x = "foo"; y = Z.zero }
let iml_s : string = Model.to_iml_string my_val
let eval_res = C.eval_src c ~session ~scr:(Format.sprintf "let my_val = %s" iml_s)

To simulate Extract, manipulate the artifact received from e.g. a sucessful instance call, and instantiate it to a concrete type using of_cir:

let x1 = C.instance_src c ~session ~src:"fun x -> Model.goal x" ();;
let r = match x1.res with | Sat { model = Some { artifact = Some art ; _ } ; _ } -> art | _ -> assert false;;
let m = Imandrakit_twine.Decode.decode_string Artifact.(of_twine Model) (Bytes.unsafe_to_string r.data);;
let t : Model.t option = List.find_map (fun (s, v) -> if s.id.name = "x" then Some (Model.of_cir v) else None) m.consts
  • List.fold_right replaced the named ~base argument with a normal positional one
  • The program-mode Caml module is removed
  • In logic mode, Z.t and Q.t no longer alias to int and real, respectively
  • Int.pow and Real.pow functions are added (with reasoning support) for better numerical operations support
  • [@@opaque] functions require explicit type annotations on the symbol, i.e. let foo : a -> b = fun ..

ImandraX replaces the previous use, mod_use, import and require constructs with a more versatile import system designed to work seamlessly with incremental proofs and the more modern OCaml ecosystem.

This includes:

  • Path Imports with Implicit Module Names: 
    [@@@import "path/to/file.iml"]
  • Path Imports with Explicit Module Names: 
    [@@@import Mod_name, "path/to/file.iml"]
  • Integration with OCamlFind and Dune: 
    [@@@import Mod_name, "findlib:foo.bar"]
[@@@import Mod_name, "dune:foo.bar"]

ImandraX introduces a unified language for tactics and tacticals, based on the by annotation. This approach allows users to structure proofs through a combination of smaller tactics and more sophisticated tacticals, enabling modular, reusable proof strategies. Additionally, ImandraX includes a rich library of built-in tactics and tacticals, encompassing a broad range of proof methods and strategies.

By contrast, Imandra employs a more ad hoc approach, relying on smaller library of custom attributes to define proof behavior.

In Imandra

See https://docs.imandra.ai/imandra-docs/notebooks/verification-attributes/

lemma pos_product m n =
  m >= 0 && n >= 0
  ==> m*n >= 0
[@@induct functional nat_induct]

In ImandraX

The by annotation interprets an expression of Tactic terms.

lemma pos_product m n =
  m >= 0 && n >= 0
  ==> m*n >= 0
[@@by induct ~on_fun:[%id nat_induct] ()]

Fine-Grained Tactics

ImandraX enables fine-grained control over proofs with advanced tactics and tacticals:

Key Features:

  • Monadic Composition: Tactics support monadic operations, enabling clean and modular chaining of reasoning steps.
  • Combinators: Operators like @>, <|>, and @>>| allow for intuitive composition and conditional application of tactics.
  • Wide Array of Built-ins: Tactics such as simp, unroll and induct cover a broad spectrum of reasoning scenarios, but there are dozen more.
lemma test_8 x y =
    x=7 && y=6+1 ==> g x y = 1
  [@@by intros
    @> [%cases (x=y), (x>7)]
    @>| [(expr_simplify
          @> [%replace y]
          @> esimp
          @> [%expand "g"]
          @> [%replace x]
          @> esimp);
          ([%skip "hello from subgoal 2"]
           @> [%skip]
           @> skip
           @> [%skip "hello again from subgoal 2"]
           @> auto);
          (expr_simplify
           @> [%replace x]
           @> [%replace y]
           @> [%expand (g 7 7)]
           @> simp)
          ]
       ]

In Imandra

  • Proofs are performed sequentially, with each statement dependent on the previous one being successfully proven.
  • Errors or timeouts in a lemma block the proofs of all successive lemmas, creating bottlenecks in the proof process.

In ImandraX

  • All statements are proven in parallel, under the assumption that previous lemmas are true.
  • This parallelism enables users to iterate on further lemmas even if their dependencies are not yet proven.
  • However, this approach introduces a new challenge:
    • If a lemma uses a non-terminating function, ImandraX may attempt to prove it assuming termination, potentially resulting in a loop until a timeout occurs.
    • In Imandra, such lemmas would not have been attempted at all, avoiding timeouts but restricting progress on other proofs.

Pervasive Caching and Incremental LSP

ImandraX incorporates pervasive caching and an incremental integrates it with incremental proofs in the Language Server Protocol (LSP).

ImandraX does not yet support features like upto_bounds (Datatype Bounds for Unrolling). These are planned for future releases.