Claude Integration

Calor is designed specifically for AI coding agents. This guide explains how to use Calor with Claude and other AI assistants.

Quick Setup

Initialize your project for Claude Code with a single command:

calor init --ai claude

This creates:

You can run this command again anytime to update the Calor documentation section in CLAUDE.md without losing your custom content.

MCP Server Integration

The init command also configures an MCP (Model Context Protocol) server that gives Claude direct access to the Calor compiler. This enables Claude to:

• Type check code and get semantic errors
• Verify contracts using the Z3 SMT solver
• Navigate code with goto-definition and find-references
• Analyze code for bugs and migration potential

How It Works

When you open the project in Claude Code, the MCP server starts automatically. Claude can then use tools like:

calor_check         - Diagnose, lint, type check, or validate
calor_verify        - Verify function contracts
calor_navigate      - Definitions, references, symbols, and scope
calor_structure     - Outlines, call graphs, and impact

Example: Contract Verification

Claude can verify your contracts are correct:

You: Does this function have any contract violations?

§F{f001:Divide:pub}
  §I{i32:a}
  §I{i32:b}
  §O{i32}
  §E{}
  §Q (!= b 0)
  §R (/ a b)

Claude: [Uses calor_verify]
The precondition is satisfiable and excludes b = 0 for valid callers.
It is assumed while verifying the body; the runtime precondition check remains.

Available Tools

See calor mcp for the complete 18-tool surface.

Calor-First Enforcement

When you initialize with --ai claude, hooks are configured that automatically block Claude from creating .cs files. This ensures all new code is written in Calor.

What Happens

When Claude tries to create a C# file:

BLOCKED: Cannot create C# file 'UserService.cs'

This is an Calor-first project. Create an .calr file instead:
  UserService.calr

Use /calor skill for Calor syntax help.

Claude will automatically retry with an .calr file - no user intervention required.

Allowed Files

The hook allows:

• .calr files - All Calor source files
• .g.cs files - Generated C# output from Calor compilation
• obj/ directory - Build artifacts

Disabling Enforcement

If you need to temporarily allow .cs file creation, remove or rename .claude/settings.json. Re-run calor init --ai claude to restore enforcement.

Available Skills

Claude automatically consults the installed skills when needed. You can also invoke them explicitly for specific tasks:

The /calor Skill

Invoke /calor when you want Claude to focus specifically on Calor syntax or see detailed templates:

/calor

What's the syntax for a while loop with a condition?

The /calor-convert Skill

Invoke /calor-convert when converting C# files to Calor:

/calor-convert

Convert src/Services/UserService.cs to Calor

Note: For most tasks, you don't need to invoke skills explicitly. Just describe what you want and Claude will write Calor automatically.

How Claude Learns Calor

When you run calor init --ai claude, three components work together to enable Claude to write Calor code automatically:

1. CLAUDE.md - Project Instructions

The CLAUDE.md file is read by Claude Code at the start of every conversation. It contains:

• Mandatory rules - "All new code MUST be written in Calor"
• Workflow guidance - When to create .calr files vs. convert existing .cs files
• Syntax highlights - Quick reference for Calor syntax
• Type mappings - How C# types map to Calor types (int → i32, string → str)

Claude reads this file automatically - you don't need to reference it in your prompts.

2. Skills - Syntax Reference

Two skills are installed in .claude/skills/:

Claude consults these skills when it needs detailed syntax information. You can also invoke them explicitly with /calor or /calor-convert if you want Claude to focus on a specific task.

3. Hooks - Enforcement

The .claude/settings.json file configures a PreToolUse hook that runs before Claude creates any file. If Claude tries to create a .cs file, the hook:

1. Blocks the operation - The file is not created
2. Returns guidance - Tells Claude to create a .calr file instead
3. Claude retries - Automatically creates the correct file type

This means even if Claude "forgets" the CLAUDE.md instructions, the hook ensures Calor-first compliance.

The Result

You simply ask Claude to write code:

Write a function that validates email addresses

Claude automatically:

1. Reads CLAUDE.md and knows to use Calor
2. Consults the calor skill for syntax details
3. Creates a .calr file (hook prevents .cs)

No special prompts or syntax teaching required.

Why Calor Works Well with Agents

1. Unambiguous Structure

Traditional code:

// Which brace closes what?
if (x > 0) {
    for (int i = 0; i < n; i++) {
        if (y > 0) {
            // ...
        }
    }
}

Calor code:

§IF{if1} (> x 0)
  §L{for1:i:0:n:1}
    §IF{if2} (> y 0)
      // ...

Every scope begins with an explicit, stable ID and ends when indentation returns to the parent level. Structural closer tags are intentionally rejected.

2. Precise Edit Targeting

Tell Claude: "Change the loop for1 to start at 1 instead of 0"

// Before
§L{for1:i:0:n:1}

// After
§L{for1:i:1:n:1}

The ID for1 uniquely identifies the target. No confusion with other loops.

3. Explicit Contracts for Verification

§F{f001:CalculateInterest:pub}
  §I{f64:principal}
  §I{f64:rate}
  §I{i32:years}
  §O{f64}
  §Q (> principal 0)
  §Q (>= rate 0)
  §Q (> years 0)
  §S (>= result principal)
  §R (* principal (** (+ 1 rate) years))

Claude can verify:

• All preconditions are satisfied at call sites
• The postcondition is mathematically correct
• No undeclared side effects

4. Effects for Side Effect Analysis

§F{f001:ProcessOrder:pub}
  §I{Order:order}
  §O{bool}
  §E{db,net,cw}
  // ...

Claude knows immediately that this function:

• Writes to database (db)
• Makes network calls (net)
• Writes to console (cw)

No need to analyze the implementation.

Example Prompts

Generate a Function

Prompt:

Write a factorial function with a precondition that n >= 0
and postcondition that result >= 1

Claude generates:

§M{m001:Math}
  §F{f001:Factorial:pub}
    §I{i32:n}
    §O{i32}
    §Q (>= n 0)
    §S (>= result 1)
    §IF{if1} (<= n 1) → §R 1
    §EL → §R (* n §C{Factorial} §A (- n 1) §/C)

Find Bugs

Prompt:

Is there a bug in this code?

§F{f001:Divide:pub}
  §I{i32:a}
  §I{i32:b}
  §O{i32}
  §R (/ a b)

Claude responds:

Yes - missing precondition. Add:

§Q (!= b 0)

Otherwise division by zero is possible.

Refactor Code

Prompt:

Refactor this to extract the calculation into a separate function:

§F{f001:Main:pub}
  §O{void}
  §E{cw}
  §B{x} (* 5 5)
  §P x

Claude generates:

§F{f001:Square:pri}
  §I{i32:n}
  §O{i32}
  §R (* n n)

§F{f002:Main:pub}
  §O{void}
  §E{cw}
  §B{x} §C{Square} §A 5 §/C
  §P x

Best Practices

1. Always include IDs - They enable precise references
2. Declare effects - Even if empty (§E{})
3. Write contracts - They serve as executable documentation
4. Indent consistently - Block boundaries are inferred from indentation; mixing tabs and spaces is rejected
5. Use standard syntax - (+ a b) for expressions

Workflow Tips

Starting a New Feature

Just describe what you need - Claude writes Calor automatically:

I need a payment processing service that:
- Validates the payment amount is positive
- Connects to the payment gateway
- Returns success or failure

Converting Existing Code

Ask Claude to convert specific files:

Convert src/Services/PaymentService.cs to Calor

Refactoring Calor

Reference specific elements by their IDs for precise edits:

In PaymentService.calr:
- Extract the validation logic from f002 into a new private function
- Add a postcondition to f001 ensuring the result is positive

Next Steps

• Syntax Reference - Complete language reference
• Adding Calor to Existing Projects - Migration guide
• calor init - Full init command documentation
• Benchmarking - See how Calor compares to C#