Installation

CodeLogician ships in three flavours. They are complementary rather than alternatives: most setups install the CLI plus the agent skill, and add the MCP server when the client prefers tools over a terminal.

Prerequisites

All three need an Imandra Universe API key (free tier available). Generate one at universe.imandra.ai and export it:

export IMANDRA_UNI_KEY=your_api_key_here

Add the line to your shell profile (~/.zshrc, ~/.config/fish/config.fish) so it persists across sessions.

CodeLogician CLI

The CLI brings the reasoning platform to your terminal: doc for built-in IML/ImandraX documentation, eval for running the ImandraX reasoning engine, and rec for next-step recommendations.

Install

The install script bundles its own Python 3.13, so no system Python is required. It installs uv if missing, then installs codelogician into an isolated environment:

curl -fsSL codelogician.dev/codelogician/install.sh | sh

If you already manage Python yourself (3.12+):

uv tool install codelogician

pip install codelogician

Verify

codelogician --version
codelogician --help

For an end-to-end check that the API key works, admit an IML file with ImandraX:

echo 'let f (x: int) = if x > 0 then x else -x' > /tmp/abs.iml
codelogician eval check /tmp/abs.iml

Update

codelogician update      # checks for a newer release and offers to install it
codelogician changelog   # what changed (--since / --until to bound the range)

See the command reference for the full command surface.

CodeLogician Agent Skill

The agent skill teaches a coding agent how to use IML and ImandraX: the language guide, verification and region-decomposition workflows, an error-fix corpus, and worked examples. It is documentation the agent loads on demand and performs no reasoning by itself, so pair it with the CLI or the MCP server.

The skill content can be found in CodeLogician Agent Skill (or its source at imandrax-tools). It is plain Markdown, so install it whichever way suits your agent: copy the directory in by hand, vendor it into a repository, or use one of the shortcuts below.

Install with npm

npx skills add imandra-ai/imandrax-tools/packages/codelogician-skill/skill

This pulls the skill from the repository and places it where your agent expects to find it.

Get the same material from the CLI

The CLI ships a vendored copy of the same skill, so you can get it without the repository or npm. Agents discover skills by location, so dump it directly into the agent's skills directory. For Claude Code that is ~/.claude/skills/<skill-name>/ to install it for yourself, or .claude/skills/<skill-name>/ to commit it with a project:

codelogician doc dump ~/.claude/skills/codelogician

doc dump refuses to write into an existing directory, so remove or rename an earlier copy before re-running it. Other agents keep skills elsewhere, so check your agent's documentation for the location it scans and dump into that instead.

Verify

The skill is registered under the name codelogician. In Claude Code, /codelogician invokes it directly, and it also loads on its own when a prompt mentions IML, Imandra, or CodeLogician. If it does not appear, start a new session so the agent rescans its skills directory.

You can also read the same material straight from the terminal:

codelogician doc help --agent
codelogician doc search md "region decomposition"

CodeLogician MCP server

The MCP server is not a separate install. It ships inside the codelogician package and starts with codelogician mcp, so install the CLI first; the extra setup is registering that command with your MCP client.

It exposes the eval analyses as MCP tools: check, list_vg / check_vg, list_test / check_test, and list_decomp / check_decomp.

Setup Common Coding Agents

Claude Code:

claude mcp add codelogician \
  --env IMANDRA_UNI_KEY=$IMANDRA_UNI_KEY \
  --transport stdio \
  -- codelogician mcp

Codex:

codex mcp add codelogician --env IMANDRA_UNI_KEY=$IMANDRA_UNI_KEY -- codelogician mcp

OpenCode:

opencode mcp add
# Then follow the interactive prompts by setting MCP server type to "Local" and command to be "codelogician mcp"

Other MCP clients

For clients not listed above, refer to their documentation for how to configure MCP servers. Most clients support configuring servers through a JSON file. Add:

{
  "mcpServers": {
    "codelogician": {
      "command": "codelogician",
      "args": ["mcp"],
      "env": {
        "IMANDRA_UNI_KEY": "your_api_key_here"
      }
    }
  }
}

If codelogician is not on the client's PATH (GUI apps often don't inherit your shell environment), use the absolute path from which codelogician.

Transports

stdio is the default and what editors and coding agents launch. For a long-running server, pick a network transport:

codelogician mcp --transport streamable-http
codelogician mcp --transport sse

Configuration

The server reads the same environment variables as the CLI: