Evaluation & Extraction

ImandraX operates in a unified mode — there is no separate "logic mode" and "program mode" as in Imandra Core. Every definition enters the logic and can be reasoned about. ImandraX provides two mechanisms for running and exporting your models.

Evaluation with eval

ImandraX has a built-in evaluator for running your models. Use eval to compute with your definitions:

let double x = x + x
 
eval double 21
(* 42 *)
 
let rec factorial n =
  if n <= 0 then 1
  else n * factorial (n - 1)
 
eval factorial 10
(* 3628800 *)
 
eval List.rev [1; 2; 3]
(* [3; 2; 1] *)

The evaluator runs your IML functions directly, producing concrete values. This is useful for:

• Testing functions before proving properties
• Inspecting computed values and data structures
• Debugging definitions to make sure they behave as expected
• Exploring the standard library

Extraction to OCaml

When you want to use your verified IML code in a real OCaml application, use extract to generate OCaml source code:

# Extract to stdout
imandrax-cli extract myfile.iml
 
# Extract to a file
imandrax-cli extract myfile.iml -o myfile.ml
 
# Add deriving annotations to generated types
imandrax-cli extract myfile.iml --deriving yojson

Extraction produces standard OCaml code that can be compiled with the normal OCaml toolchain and integrates with dune (the OCaml build system). See CLI Reference for all extraction options.

This gives you a powerful workflow:

1. Model in IML — write your core logic
2. Verify with ImandraX — prove it correct
3. Extract to OCaml — get executable, efficient code
4. Integrate with dune — use in your OCaml project

Opaque functions

The [@@opaque] annotation declares a function without providing its definition to the logic. The function exists and has a type, but ImandraX cannot look inside it:

let external_computation (x : int) : int = (* ... *)
[@@opaque]

Opaque functions:

• Require explicit type annotations
• Cannot be unrolled or expanded during proof
• Can be constrained by axioms

This is useful for modelling external systems:

let hash (x : string) : int = (* ... *)
[@@opaque]
 
(* Constrain hash with known properties *)
axiom hash_non_neg x = hash x >= 0

Differences from Imandra Core

In Imandra Core, there were separate logic and program modes, with [@@program] for side-effecting code and [@@reflect] for bridging. ImandraX eliminates this distinction: