Python Client

The imandrax-api Python package provides both synchronous and asynchronous clients for the ImandraX reasoning engine.

Installation

pip install imandrax-api

Requires Python >= 3.12.

Quick start

import imandrax_api
 
# Connect to a local server
client = imandrax_api.Client(url="http://localhost:8082")
 
# Check server status
client.status()
 
# Evaluate IML definitions
client.eval_src(src="let f x = x + 1")
 
# Evaluate theorems (returns tasks for proof obligations)
result = client.eval_src(src="theorem my_thm x = f x > x")
print(result.tasks)  # Tasks produced during evaluation
 
# Verify a property
result = client.verify_src(src="fun x -> x + 10 <> 21")
# result has .proved, .refuted, .verified_upto, etc.
 
# Find a satisfying instance
result = client.instance_src(src="fun x -> f x = 43")
 
# QuickCheck a property
result = client.qcheck_src(src="fun x -> f x > x", seed=42)
 
# Typecheck source code
result = client.typecheck(src="let g x y = x + y")
print(result.types)  # JSON dictionary of inferred types

Client API

`Client(url, api_key=None, timeout=30, session_id=None)`

Create a client and session. A new session is automatically created on construction and ended when the client is destroyed or used as a context manager.

# Local server
client = imandrax_api.Client(url="http://localhost:8082")
 
# Cloud API with authentication
client = imandrax_api.Client(
    url="https://api.imandra.ai/internal/imandrax/",
    api_key="your-api-key"
)
 
# As a context manager (auto-cleanup)
with imandrax_api.Client(url="http://localhost:8082") as client:
    client.eval_src(src="let f x = x + 1")

`client.eval_src(src, timeout=None)`

Evaluate IML source code in the session. Returns an EvalRes with:

success — Whether evaluation succeeded
messages — Output messages
errors — Any errors
tasks — Tasks started during evaluation (e.g., proof obligations)
po_results — Proof obligation results
eval_results — Eval statement outputs
decomp_results — Decomposition results

result = client.eval_src(src="""
  type color = Red | Green | Blue
 
  let is_warm = function
    | Red -> true
    | _ -> false
""")

`client.verify_src(src, hints=None, timeout=None)`

Verify a property. Returns a VerifyRes with one of:

proved — Property holds universally
refuted — Counterexample found (with model containing IML source)
verified_upto — Verified up to a bound
unknown — Could not determine

result = client.verify_src(src="fun (x : int) -> x * x >= 0")

`client.instance_src(src, hints=None, timeout=None)`

Find a satisfying instance. Returns an InstanceRes with one of:

sat — Instance found (with model)
unsat — No instance exists
unknown — Could not determine

result = client.instance_src(src="fun x -> x * x = 144")

`client.decompose(name, assuming=None, basis=[], rule_specs=[], prune=True, ctx_simp=None, timeout=None, str=True)`

Decompose a function into regions of behavior.

Parameter	Default	Description
`name`	required	Function name to decompose
`assuming`	`None`	Side-condition function name
`basis`	`[]`	Functions to treat as atomic
`rule_specs`	`[]`	Background axioms
`prune`	`True`	Remove infeasible regions
`ctx_simp`	`None`	Contextual simplification
`timeout`	client default	Timeout in seconds
`str`	`True`	Include string representation

client.eval_src(src="""
  let classify age =
    if age < 0 then "invalid"
    else if age < 18 then "minor"
    else "adult"
""")
 
result = client.decompose(name="classify")

`client.qcheck_src(src, seed=None, timeout=None)` / `client.qcheck_name(name, seed=None, timeout=None)`

QuickCheck a property with random testing.

result = client.qcheck_src(src="fun x -> f x > x", seed=42)

`client.typecheck(src, timeout=None)`

Typecheck source code and return inferred types as JSON.

`client.get_decls(names, timeout=None)`

Retrieve declarations by name from the session.

result = client.get_decls(names=["f", "g"])
# result.decls — found declarations
# result.not_found — names not found

Artifact retrieval

# List available artifact kinds for a task
arts = client.list_artifacts(task)
 
# Get an artifact as a zip file
art_zip = client.get_artifact_zip(task, kind="show")

Async client

For async/await usage (requires aiohttp):

import imandrax_api
 
async with imandrax_api.AsyncClient(url="http://localhost:8082") as client:
    await client.eval_src(src="let f x = x + 1")
    result = await client.verify_src(src="fun x -> f x > x")

The AsyncClient has the same API as Client but all methods are async.

Authentication

The client reads API keys from:

api_key parameter passed to Client()
Environment variables (in order): IMANDRA_UNI_KEY, IMANDRAX_API_KEY, IMANDRA_KEY
Config files: ~/.config/imandra/api_key, ~/.config/imandrax/api_key

Cloud endpoints

Environment	URL
Production	`https://api.imandra.ai/internal/imandrax/`
Development	`https://api.dev.imandracapital.com/internal/imandrax/`

Source code

The Python client source is in the imandrax-api repository under src/py/.