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_API_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 success!

Step 5 — Verification

Now add a property we expect to hold:

(* fees.iml — add a verification goal *)
let () =
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 success!
 
=====VG=====
 
1: verify (fun m amount ->
  amount >. 0.0 ==>
  calculate_fee m amount <. amount)
refuted:
  model:
    m_type: Counter_example
    src: |
      module M = struct
 
        let m = BankTransfer
        let amount = 1.0
 
       end

CodeLogician reveals that when payment method is BankTransfer with amount 1.0, the 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
Discovering Edge Cases
Behavioral Decomposition