CLI Reference

The imandrax-cli tool provides command-line access to ImandraX for verification, OCaml extraction, interactive sessions, server management, and CI/CD integration.

Commands overview

imandrax-cli check

Verify all theorems, lemmas, and verification goals in one or more files:

imandrax-cli check myfile.iml
imandrax-cli check src/model.iml src/properties.iml

This is the primary command for CI/CD pipelines — add it to your build process to ensure all proofs pass before merging.

Key options:

Exit codes:

imandrax-cli extract

Extract IML definitions to valid 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
imandrax-cli extract myfile.iml --deriving yojson

This generates OCaml code from your verified IML definitions, suitable for integration with Dune build projects. See Evaluation & Extraction for details on the extraction workflow.

Key options:

imandrax-cli repl

Open an interactive REPL (read-eval-print loop) session:

# Start a fresh REPL
imandrax-cli repl
 
# Load files before starting
imandrax-cli repl -l prelude.iml -l model.iml

The REPL lets you interactively define functions, run verifications, and explore your models. It supports all IML commands including verify, instance, theorem, and eval.

Key options:

imandrax-cli serve-http

Start an HTTP server for exploring existing sessions:

imandrax-cli serve-http -p 8080

Key options:

See HTTP API for details on the API endpoints.

imandrax-cli lsp

Run the Language Server Protocol server. This is used internally by the VS Code extension — you typically don't need to run it directly:

imandrax-cli lsp

imandrax-cli analyze-dune

Analyze a Dune project to discover IML files and their dependencies:

imandrax-cli analyze-dune --from-dir ./my-project

imandrax-cli version

Display the installed version:

imandrax-cli version

CI/CD integration

GitHub Actions

- name: Verify IML files
  run: |
    imandrax-cli check src/model.iml
    imandrax-cli check src/properties.iml
  env:
    IMANDRAX_API_KEY: ${{ secrets.IMANDRAX_API_KEY }}

General CI

#!/bin/bash
set -e
 
# Verify all .iml files
for f in src/*.iml; do
  echo "Checking $f..."
  imandrax-cli check "$f"
done
 
echo "All verifications passed!"

Extract and build

#!/bin/bash
set -e
 
# Extract verified IML to OCaml
imandrax-cli extract src/model.iml -o src/model.ml
 
# Build with Dune
dune build

Environment variables

Common options

These options are available across most commands: