Imandra CLI and API client library

Imandra is a cloud-native automated reasoning engine for analysis of algorithms and data.

This package contains the imandra Python library for interacting with Imandra's web APIs. It includes:

imandra.core, which provides programmatic access to Imandra X, Imandra's core reasoning engine.
imandra.u.reasoners.*, bindings to Imandra Universe Reasoners.
imandra.ipl, tools for analysing Imandra Protocol Language (IPL) files.

If you're interested in developing Imandra X or IPL models, you may also want to see the Imandra documentation.

The imandra python API reference documentation is available here.

Authentication

First obtain an API key from https://universe.imandra.ai.

The Python library will read the API key from the first of:

The api_key parameter passed when instantiating a Client.
The IMANDRA_API_KEY environment variable.
The file $HOME/.config/imandra/api_key (MacOS and Linux) or %USERPROFILE%\AppData\Local\imandra\api_key (Windows)

Example: Imandra Core

First, ensure dependencies for the core module are installed. Note that imandra.core requires Python >= 3.12.

$ pip install 'imandra[core]'

$ ipython
...
In [1]: from imandra.core import Client

In [2]: client = Client()

In [3]: client.eval_src('let f x = if x > 0 then if x * x < 0 then x else x + 1 else x')
Out[3]: success: true

In [4]: result = client.verify_src('fun x -> x > 0 ==> f x > 0')

In [5]: result
Out[5]:
proved {
  proof_pp: "..."
}

In [6]: print(result.proved.proof_pp)
{ id = 1; concl = `|- x > 0 ==> f x > 0`;
  view =
  T_deduction {
    premises =
    [("p",
      [{ id = 0; concl = `|- x > 0 ==> f x > 0`;
         view = T_deduction {premises = []} }
        ])
      ]}
  }

In [7]: result = client.instance_src('fun x -> f x = 43')

In [8]: result
Out[8]:
sat {
  model {
    m_type: Instance
    src: "module M = struct\n\n  let x = 42\n\n end\n"
    artifact {
      kind: "cir.model"
      data: "..."
      api_version: "v8"
    }
  }
}

In [9]: print(result.sat.model.src)
module M = struct

  let x = 42

 end

In [10]: result = client.decompose('f')

In [11]: result
Out[11]:
artifact {
  kind: "cir.fun_decomp"
  data: "..."
  api_version: "v8"
}
regions_str {
  constraints_str: "not (x > 0)"
  invariant_str: "x"
  model_str {
    k: "x"
    v: "0"
  }
}
regions_str {
  constraints_str: "not (x * x < 0)"
  constraints_str: "x > 0"
  invariant_str: "x + 1"
  model_str {
    k: "x"
    v: "1"
  }
}
task {
  id {
    id: "task:decomp:rE3VSX-t5kbrrAksQ4saBrMUs2uHTXfu-CqeZunV9aE="
  }
  kind: TASK_DECOMP
}

Example: Imandra Universe reasoners

$ pip install imandra

$ ipython

In [1]: from imandra.u.reasoners.prover9 import Client

In [2]: client = Client()

In [3]: input = "formulas(sos).\n\n  e * x = x.\n  x'\'' * x = e.\n  (x * y) * z = x * (y * z).\n\n  x * x = e.\n\nend_of_list.\n\nformulas(goals).\n\n  x * y = y * x.\n\nend_of_list ...: ."

In [4]: result = client.eval(input)

In [5]: print(result['results'][0])
============================== Prover9 ===============================
Prover9 (64) version 2009-11A, November 2009.
Process 18 was started by universe on localhost,
Mon Jan  6 14:52:26 2025
The command was "/imandra-universe/prover9/bin/prover9 -t 45".
============================== end of head ===========================

============================== INPUT =================================

formulas(sos).
e * x = x.
x''' * x = e.
(x * y) * z = x * (y * z).
x * x = e.
end_of_list.

formulas(goals).
x * y = y * x.
end_of_list.

============================== end of input ==========================

...

============================== PROOF =================================

% Proof 1 at 0.01 (+ 0.00) seconds.
% Length of proof is 16.
% Level of proof is 7.
% Maximum clause weight is 11.000.
% Given clauses 12.

1 x * y = y * x # label(non_clause) # label(goal).  [goal].
2 e * x = x.  [assumption].
3 x''' * x = e.  [assumption].
4 (x * y) * z = x * (y * z).  [assumption].
5 x * x = e.  [assumption].
6 c2 * c1 != c1 * c2.  [deny(1)].
7 x''' * (x * y) = y.  [para(3(a,1),4(a,1,1)),rewrite([2(2)]),flip(a)].
8 x * (x * y) = y.  [para(5(a,1),4(a,1,1)),rewrite([2(2)]),flip(a)].
9 x * (y * (x * y)) = e.  [para(5(a,1),4(a,1)),flip(a)].
11 x'''''' * e = x.  [para(3(a,1),7(a,1,2))].
13 x''' * e = x.  [para(5(a,1),7(a,1,2))].
15 x''' = x.  [back_rewrite(11),rewrite([13(8)])].
16 x * e = x.  [back_rewrite(13),rewrite([15(3)])].
19 x * (y * x) = y.  [para(9(a,1),8(a,1,2)),rewrite([16(2)]),flip(a)].
24 x * y = y * x.  [para(19(a,1),8(a,1,2))].
25 $F.  [resolve(24,a,6,a)].

============================== end of proof ==========================

============================== STATISTICS ============================

Given=12. Generated=122. Kept=23. proofs=1.
Usable=8. Sos=3. Demods=12. Limbo=2, Disabled=14. Hints=0.
Kept_by_rule=0, Deleted_by_rule=0.
Forward_subsumed=99. Back_subsumed=0.
Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0.
New_demodulators=21 (0 lex), Back_demodulated=9. Back_unit_deleted=0.
Demod_attempts=770. Demod_rewrites=156.
Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0.
Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0.
Megabytes=0.06.
User_CPU=0.01, System_CPU=0.00, Wall_clock=0.

============================== end of statistics =====================

============================== end of search =========================

THEOREM PROVED

Example: IPL

$ pip install imandra

$ ipython

In [1]: from imandra.ipl import Client

In [2]: client = Client()

In [3]: job_id = client.unsat_analysis('/path/to/model.ipl')

In [4]: client.status(job_id)
Out[4]: 'processing'

In [5]: client.wait(job_id)
Out[5]: 'done'

In [6]: data = client.data(job_id)

In [7]: print(data['content'].decode('ascii'))
For message flow `simple_orders_one`, unsat cores: []

CLI

The imandra package also adds an entry point called imandra-cli which exposes the imandra library functionality in a more discoverable way:

$ python3 -m venv ./my/venv
...
$ ./my/venv/pip install imandra
...
$ ./my/venv/bin/imandra-cli --help
usage: imandra [-h] auth,ipl,core,rule-synth,cfb ...

Imandra CLI

positional arguments:
  {auth,ipl,core,rule-synth,cfb}

optional arguments:
  -h, --help            show this help message and exit

On Windows, the entry point can be found as .\my\venv\Scripts\imandra-cli.exe.

CLI Authentication

This is the first step to start using the Imandra CLI. Our cloud environment requires a user account, which you can setup like this:

$ ./my/venv/bin/imandra-cli auth login

and follow the prompts to authenticate. This will create the relevant credentials in ~/.imandra (or %APPDATA%\imandra on Windows).

You should now be able to invoke CLI commands that require authentication.

Metadata

Release files for imandra 2.10.0

For a detailed explanation of source distributions (sdists) and built distributions (wheels), please see the package formats documentation.

Source distribution (sdist)

Source distribution for imandra 2.10.0
File	Size	Uploaded	Provenance
imandra-2.10.0.tar.gz	82.7 kB	Oct 6, 2026	Without provenance	Details

Built distribution (wheel)

Table of built distributions (wheels) for imandra 2.10.0
File	Interpreter	ABI	Platform	Reset
imandra-2.10.0-py3-none-any.whl 154.1 kB Oct 6, 2026 Without provenance	Python 3	none	any	Details

Total release size: 236.9 kB

Release files / imandra-2.10.0.tar.gz

Download URL	imandra-2.10.0.tar.gz
Size	82.7 kB
Tags	Source
SHA-256 checksum How to use checksums	`e85be603976b0174d7fca0ad835cdcf0b8fda4f24569f510bb7f6096c6539776`
BLAKE2b-256 checksum How to use checksums	`a3515c3a8aa5965a9b7f3466c8eb0ca980742dfe146b7108aaae3519b8f2bedf`
Upload date	Oct 6, 2026
Uploaded using Trusted Publishing? What is trusted publishing?	No
Uploaded via	`uv/0.8.22`

Release files / imandra-2.10.0-py3-none-any.whl

Download URL	imandra-2.10.0-py3-none-any.whl
Size	154.1 kB
Tags	Python 3
SHA-256 checksum How to use checksums	`5f1b14fd2462e4c805e1c96a2356108408c61b634f0cfe5fdf75d04fb102f370`
BLAKE2b-256 checksum How to use checksums	`e3302b817e4fcdf965879bf3fc2833d3c641f47e035eca2f4d158f1f7bb0dc7c`
Upload date	Oct 6, 2026
Uploaded using Trusted Publishing? What is trusted publishing?	No
Uploaded via	`uv/0.8.22`

Security for imandra 2.10.0

Report project as malware

Provenance

Provenance describes where a file came from. On PyPI, provenance is shared via attestations, which provide a verifiable record of the build or publishing details. View details, limitations and caveats.

No provenance found

None of the files in this release were uploaded with provenance metadata.

A note on package security

PyPI is a repository for distributing packages, not a service for auditing them. While third-party security researchers and our staff do their best to detect and remove malicious packages, PyPI cannot guarantee the quality, security or suitability of any given package.

To learn more about protecting yourself from malicious actors, visit our package security documentation.