HTTP API

ImandraX exposes its reasoning engine via a Twirp RPC API — a protobuf-based protocol over HTTP. Client libraries for Python, TypeScript, Rust, and OCaml are generated from the protobuf definitions in the imandrax-api repository.

Architecture

The API is session-based. You create a session, submit IML code for evaluation, run verification and decomposition commands, and retrieve results — all through typed RPC calls. Sessions maintain state: definitions submitted in one call are available for subsequent calls in the same session.

Services

The API is split into several protobuf services:

`Simple` — High-level API

The primary service for most use cases. Provides a streamlined interface for common operations:

Method	Description
`status`	Get server status
`shutdown`	Ask the server to exit
`create_session`	Create a new reasoning session
`end_session`	Terminate a session
`eval_src`	Evaluate IML source code
`verify_src`	Verify a property given as source code
`verify_name`	Verify a named predicate already in the session
`instance_src`	Find a satisfying instance given source code
`instance_name`	Find a satisfying instance for a named predicate
`qcheck_src`	QuickCheck a property given as source code
`qcheck_name`	QuickCheck a named predicate
`decompose`	Run region decomposition on a named function
`decompose_full`	Region decomposition with composition operators
`typecheck`	Typecheck source code and return inferred types
`get_decls`	Retrieve declarations by name
`oneshot`	Sessionless, self-contained request/response

`Eval` — Low-level evaluation

For more fine-grained control over evaluation and artifact management:

Method	Description
`eval_code_snippet`	Evaluate a code snippet in a session
`parse_term`	Parse and typecheck a term, return as artifact
`parse_type`	Parse and typecheck a type, return as artifact
`list_artifacts`	List available artifact kinds for a task
`get_artifact`	Retrieve an artifact from a task
`get_artifact_zip`	Retrieve an artifact as a zip file

`SessionManager` — Session lifecycle

Method	Description
`create_session`	Create a new session (with optional proof obligation checking)
`open_session`	Reconnect to an existing session
`end_session`	Terminate a session
`keep_session_alive`	Keep a session active

`System` — Server information

Method	Description
`version`	Return the server version
`gc_stats`	Get garbage collection statistics
`release_memory`	Free memory and return stats

Key message types

Verification results

Verification calls (verify_src, verify_name) return a VerifyRes with one of:

Proved — The property holds universally (with optional proof pretty-print)
Refuted — A counterexample was found (with a Model containing IML source code for the counterexample)
Verified_upto — Verified up to a bound but not proved inductively
unknown — The prover could not determine the result
err — An error occurred

Instance results

Instance calls return an InstanceRes with one of:

Sat — A satisfying instance was found (with a Model)
Unsat — No satisfying instance exists
unknown — The solver could not determine the result

Decomposition

The decompose method takes:

Parameter	Description
`name`	Function name to decompose
`assuming`	Optional side-condition function name
`basis`	List of function names to treat as atomic
`rule_specs`	Background axioms for rewriting
`prune`	Remove infeasible regions
`ctx_simp`	Enable contextual simplification
`lift_bool`	Boolean lifting strategy (`Default`, `NestedEqualities`, `Equalities`, `All`)
`timeout`	Timeout in seconds

For complex decompositions with composition operators (merge, compound merge, combine), use decompose_full with its recursive Decomp message type.

Tasks and artifacts

Many operations produce tasks — background computations whose results can be retrieved later. Each task has an ID and a kind (TASK_EVAL, TASK_CHECK_PO, TASK_PROOF_CHECK, TASK_DECOMP). Use list_artifacts and get_artifact to retrieve structured results from completed tasks.

Authentication

Include your API key as a Bearer token in the Authorization header:

Authorization: Bearer <your-api-key>

Place your API key in ~/.config/imandrax/api_key, or set one of the environment variables (IMANDRA_UNI_KEY, IMANDRAX_API_KEY, or IMANDRA_KEY).

Protocol details

The API uses Twirp v7 over HTTP with protobuf serialization. The default server path prefix is /api/v1. All requests include an x-api-version header for version compatibility.

Protobuf definitions

The canonical protobuf definitions are in the imandrax-api repository. Pre-built client libraries are available for Python, TypeScript, Rust, and OCaml.