First Steps with CodeLogician

CodeLogician works best when driven by an AI coding agent. This guide shows how to use Claude Code with CodeLogician to reason about Python code.

Step 1 — Teach Claude Code about CodeLogician

Start by asking Claude Code to learn the CodeLogician toolchain:

Learn how to use codelogician by running codelogician doc --help

Claude Code will run codelogician doc --help, which displays the documentation tree. Claude Code can then use doc search to find specific topics.

Step 2 — Write Your Python Code

Create a payment state machine:

from enum import Enum
 
class PaymentState(Enum):
    PENDING = 1
    AUTHORIZED = 2
    CAPTURED = 3
    FAILED = 4
 
def transition(state: PaymentState, action: str) -> PaymentState:
    if state == PaymentState.PENDING:
        if action == "authorize":
            return PaymentState.AUTHORIZED
        elif action == "fail":
            return PaymentState.FAILED
    elif state == PaymentState.AUTHORIZED:
        if action == "capture":
            return PaymentState.CAPTURED
        elif action == "fail":
            return PaymentState.FAILED
    return state

Step 3 — Ask Claude Code to Analyze It

Now ask Claude Code:

Use CodeLogician to formalize this payment state machine and verify that captured payments can never return to pending.

Claude Code will:

Translate the Python code into an IML model
Add a verification goal for the property
Run codelogician eval check to submit it to ImandraX
Report the results back — either a proof or a counterexample

What You Get Back

CodeLogician returns reasoning artifacts such as:

Edge cases — concrete inputs that expose unexpected behavior
Boundary conditions — where behavior changes between regions
Verified invariants — properties proved to hold for all inputs
Behavioral regions — all distinct execution paths through the system
Test inputs — high-coverage test cases derived from the analysis

These artifacts allow Claude Code to refine the implementation with evidence, not guesswork.

Why This Matters

LLMs are optimized for language generation, not exhaustive reasoning.

CodeLogician adds a logical reasoning layer that:

explores all reachable states
proves properties about systems
finds counterexamples automatically

This turns AI coding from:

plausible output

into

verified system behavior.

Next Guides

Continue with: