codelogician CLI

The codelogician CLI brings the CodeLogician reasoning platform to your terminal. It is designed to pair with CLI coding agents (Claude Code, Codex, Gemini CLI, …): a fast, file-system-friendly feedback loop for building and analyzing IML models.

It provides:

  • doc — built-in IML/ImandraX documentation, guides, and reference
  • eval — evaluate IML models with the ImandraX reasoning engine (syntax, verification goals, region decomposition, test generation)

Installation

Install CodeLogician CLI (includes Python 3.13):

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

Or install with pip (requires Python 3.12+):

pip install codelogician

Set your Imandra Universe API key:

export IMANDRA_UNI_KEY=your_api_key_here

Then explore the command surface:

$ codelogician --help
                                                                                               
 Usage: codelogician [OPTIONS] COMMAND [ARGS]...                                               
                                                                                               
 CodeLogician helps AI coding agents reason about complex software using math and logic. 🚀    
                                                                                               
 LLM-based coding assistants are excellent at generating code, but their reasoning is          
 fundamentally statistical.                                                                    
 CodeLogician makes the agent build a mathematical model of the system and uses automated      
 reasoning to analyze behavior before software is deployed.                                    
                                                                                               
 With CodeLogician, agents can:                                                                
 - discover edge cases                                                                         
 - verify invariants                                                                           
 - explore behavioral boundaries                                                               
 - generate high-coverage tests                                                                
 - produce concrete counterexamples when assumptions fail                                      
                                                                                               
 To run CodeLogician, obtain an Imandra Universe API key at https://universe.imandra.ai        
 and make it available in your environment as `IMANDRA_UNI_KEY`.                               
                                                                                               
 Typical workflow:                                                                             
 - use `doc` to learn the basics                                                               
 - formalize ideas from specifications, PRD, source code, agent plan, and etc. into IML        
 - run `eval` commands to analyze the model                                                    
 - use the reasoning results to refine code, models, and tests                                 
                                                                                               
 Learn more at https://www.codelogician.dev!                                                   
                                                                                               
╭─ Options ───────────────────────────────────────────────────────────────────────────────────╮
│ --version             -V        Show version and exit                                       │
│ --install-completion            Install completion for the current shell.                   │
│ --show-completion               Show completion for the current shell, to copy it or        │
│                                 customize the installation.                                 │
│ --help                          Show this message and exit.                                 │
╰─────────────────────────────────────────────────────────────────────────────────────────────╯
╭─ Commands ──────────────────────────────────────────────────────────────────────────────────╮
│ update     Check version and show upgrade guide                                             │
│ rec        Suggest next step based on IML code and eval result                              │
│ changelog  Show changelog entries (optionally between two versions)                         │
│ doc        Dump and search documentation, guides and ImandraX reference.                    │
│ eval       Evaluate IML file via ImandraX API.                                              │
╰─────────────────────────────────────────────────────────────────────────────────────────────╯

Documentation — doc

Access built-in IML/ImandraX documentation directly from the terminal, designed for both humans and coding agents. Dump the full documentation set to disk with codelogician doc dump ./docs, or search it in place:

$ codelogician doc search md "region decomposition"
SKILL.md
  name: codelogician
  desc: Use IML (Imandra Modeling Language) / ImandraX to reason about software engineering (programs and specifications) - formal verification, theorem proving, counter-example generation, region decomposition / test-case generation, etc. Read me whenever you see mentioning of IML / Imandra / CodeLogician.
  (fuzzy match, use `doc search md "codelogician"` for full content)
 
advanced/region-decomp-advanced-features.md
  name: region-decomp-advanced-features
  desc: Advanced features in Region Decomposition, including composition operators and refiners
  (fuzzy match, use `doc search md "region-decomp-advanced-features"` for full content)

See the doc reference for all subcommands.

Evaluation — eval

The eval commands invoke the ImandraX reasoning engine on an IML model. Start with check, which admits every definition in a file and reports syntax or logical errors:

type payment_method =
  | Card
  | BankTransfer
 
let calculate_fee m amount =
  match m with
  | Card -> 0.029 *. amount +. 0.30
  | BankTransfer -> 0.008 *. amount +. 1.50
$ codelogician eval check fee.iml
Eval succeed

Add a verification goal with verify, then check it with eval check-vg. ImandraX either proves the goal or returns a concrete counterexample:

(* A verification goal: the fee should always be smaller than the amount paid. *)
verify (fun m amount ->
  amount >. 0.0 ==>
  calculate_fee m amount <. amount
)
$ codelogician eval check-vg fee.iml
eval_res: Success
vg_res_list:
- vg_req_index: 0
  kind: verify
  src: |-
    fun m amount ->
      amount >. 0.0 ==>
      calculate_fee m amount <. amount
  vg_res:
    refuted:
      model:
        m_type: Counter_example
        src: |
          module M = struct
 
            let amount = 1.0
            let m = BankTransfer
 
          end
    errors: []
    task: <hidden>

Here ImandraX refutes the goal: with BankTransfer and an amount of 1.0, the fixed transfer fee exceeds the amount. eval also covers region decomposition (check-decomp) and test generation (gen-test) — see the eval reference.

Next steps — rec

codelogician rec FILE reads a model (and, optionally, a saved eval result) and suggests what to do next — useful both interactively and for coding agents deciding the next action.

codelogician rec fee.iml

See the rec reference.

Version management — changelog and update

  • codelogician changelog shows changelog entries, optionally between two versions (--since / --until).
  • codelogician update checks for a newer release and shows the upgrade guide.

When to use the CLI

Use the CLI when:

  • pairing CodeLogician with a terminal coding agent
  • running one-off checks or verifications from the shell
  • building scriptable, automated reasoning pipelines

For editor-native and MCP-based workflows, see the MCP server and VS Code extension.

Previous← Interfaces
NextMCP Server →