Installation

The fastest way to get started with ImandraX is through the VS Code extension, which provides an integrated editing, proving and proof-exploration experience. For CI/CD pipelines and advanced workflows, you can also install the standalone CLI.

VS Code Extension (Recommended)

The VS Code extension is the primary way to use ImandraX. It includes:

• Full LSP integration with syntax highlighting and error reporting
• Goal state viewer — see proof obligations and walk through proofs interactively
• Incremental proof checking — only re-verify what changed
• Integrated counterexample display
• One-click installation of the ImandraX CLI

Step 1: Install the extension

Open VS Code and install the ImandraX extension from the marketplace:

1. Open the Extensions panel (Cmd+Shift+X on macOS, Ctrl+Shift+X on Linux/Windows)
2. Search for "ImandraX"
3. Click Install

Alternatively, install directly from the VS Code Marketplace.

Step 2: Set your API key

ImandraX requires an Imandra Universe API key. Get one at universe.imandra.ai (free tier available).

Save your key to the config file:

mkdir -p ~/.config/imandrax
echo "your-key-here" > ~/.config/imandrax/api_key

Alternatively, you can set it as an environment variable (more common for Python libraries and CI environments). The following environment variables are checked in order: IMANDRA_UNI_KEY, IMANDRAX_API_KEY, IMANDRA_KEY.

export IMANDRAX_API_KEY="your-key-here"

Python libraries and agents will also look for config files in this order: ~/.config/imandra/api_key, then ~/.config/imandrax/api_key.

Step 3: Create your first file

Create a new file with the .iml extension (e.g., hello.iml). The extension will automatically activate and connect to the ImandraX reasoning engine.

(* hello.iml — your first ImandraX file *)
 
let double x = x + x
 
verify (fun x -> double x >= x)

You should see ImandraX process the file and report the verification result inline.

Standalone CLI (Advanced)

The imandrax-cli tool provides a command-line interface for non-interactive verification, useful for CI/CD pipelines and scripting.

Installation

The CLI can be installed alongside the VS Code extension, or independently:

# The VS Code extension can install the CLI for you.
# For manual installation, download from:
# https://universe.imandra.ai

Basic usage

Check a file:

imandrax-cli check myfile.iml

This verifies all theorems, lemmas, and verification goals in the file and reports results to stdout. The exit code is 0 if all goals succeed, non-zero otherwise — making it ideal for CI pipelines.

Start the HTTP API server:

imandrax-cli serve-http -p 8000

This launches an HTTP server that exposes the ImandraX reasoning engine for programmatic access from Python, OCaml, or any HTTP client. See the API Reference for details.

System Requirements

• Operating system: macOS (Apple Silicon or Intel) or Linux (x86_64)
• VS Code: Version 1.85 or later (for the extension)
• Network: Internet connection required for API key validation

Next steps

Now that ImandraX is installed, head to Your First Proof to write and verify your first theorem.