Quickstart

This quickstart shows how to run CodeLogician and discover a real edge case in a few minutes.

CodeLogician works by turning system behavior into logic models and then using the ImandraX reasoning engine to explore all possible behaviors.

Step 1 — Get an API key

CodeLogician requires an Imandra Universe API key to connect to the reasoning engine.

export IMANDRA_UNI_KEY=your_api_key_here

Step 2 — Install

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

Step 3 — Create a simple model

Create a file called fees.iml:

(* fees.iml *)
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

Step 4 — Run CodeLogician

$ codelogician eval check fees.iml
Eval succeed

Step 5 — Verification

Now add a property we expect to hold:

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
 
(* A verification goal (essentially a boolean predicate) checking that the fee is always less than the amount *)
verify (fun m amount ->
  amount >. 0.0 ==>
  calculate_fee m amount <. amount
)

CodeLogician found a counterexample that violates the property:

$ codelogician eval check-vg fees.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>

CodeLogician reveals that when payment method is BankTransfer with amount 1.0, the fixed bank transfer fee dominates the transaction.

What Just Happened

Instead of sampling likely executions like an LLM would, CodeLogician:

explored the entire behavioral space
searched for counterexamples
returned concrete evidence

This is the core of logic‑first AI.

Next Steps

Continue with:

First Steps with CodeLogician — using Claude Code together with CodeLogician
Discovering Edge Cases — automatically discover behavioral edge cases
Behavioral Decomposition — understanding region decomposition