mcp

Start a Model Context Protocol (MCP) server for AI agent integration.

Bash

calor mcp [options]

Overview

The mcp command starts an MCP server that exposes Calor compiler capabilities to AI agents like Claude. This enables agents to:

Compile and verify Calor code
Type check source for semantic errors
Navigate code with goto-definition and find-references
Analyze code for bugs and migration potential
Convert between C# and Calor

The server communicates via newline-delimited JSON (NDJSON) over stdio, following the MCP specification.

Quick Start

Bash

# Start the MCP server
calor mcp

# With verbose logging (for debugging)
calor mcp --verbose

Options

Option	Short	Default	Description
`--verbose`	`-v`	`false`	Enable verbose logging to stderr

Claude Code Integration

When you run calor init --ai claude, the MCP server is automatically configured in ~/.claude.json:

JSON

{
  "projects": {
    "/path/to/your/project": {
      "mcpServers": {
        "calor": {
          "command": "calor",
          "args": ["mcp"]
        }
      }
    }
  }
}

Claude Code will automatically start the MCP server when you open the project.

Gemini CLI Integration

When you run calor init --ai gemini, the MCP server is automatically configured in .gemini/settings.json alongside hooks:

JSON

{
  "mcpServers": {
    "calor": {
      "command": "calor",
      "args": ["mcp", "--stdio"]
    }
  },
  "hooks": {
    "BeforeTool": [ ... ]
  }
}

Unlike Claude Code, Gemini CLI's MCP config does not require a type field, and configuration is project-level (.gemini/settings.json) rather than user-level.

GitHub Copilot Integration

When you run calor init --ai github, the MCP server is automatically configured in .vscode/mcp.json:

JSON

{
  "servers": {
    "calor": {
      "command": "calor",
      "args": ["mcp", "--stdio"]
    }
  }
}

Copilot will use the MCP server when Agent mode is enabled in VS Code.

Note: The Copilot config format differs from Claude — it uses servers (not mcpServers), is project-level (not user-level), and does not require a type field.

Available Tools

The MCP server exposes 33 tools organized by category:

Compilation & Verification

Tool	Description
`calor_compile`	Compile Calor source to C#
`calor_typecheck`	Type check source code, returns categorized errors
`calor_verify`	Verify contracts with Z3 SMT solver
`calor_verify_contracts`	Alias for verify with improved discoverability
`calor_diagnose`	Get syntax diagnostics for a file

Tool	Description
`calor_goto_definition`	Find definition of symbol at position
`calor_find_references`	Find all usages of a symbol
`calor_symbol_info`	Get type, contracts, and signature for a symbol
`calor_document_outline`	Get hierarchical structure of a file
`calor_find_symbol`	Search symbols by name across files
`calor_scope_info`	Get everything in scope at a given position

Analysis & Migration

Tool	Description
`calor_analyze`	Advanced verification (dataflow, taint, bug patterns)
`calor_assess`	Score C# files for migration potential
`calor_analyze_convertibility`	Analyze C# code for Calor conversion likelihood
`calor_convert`	Convert between C# and Calor
`calor_convert_validated`	Full validated conversion pipeline (convert → fix → diagnose → compat)
`calor_compile_check_compat`	Check compatibility of generated C#
`calor_impact_analysis`	Compute what would be affected by changing a symbol
`calor_call_graph`	Get callers/callees with effect annotations
`calor_edit_preview`	Preview effects of an edit before committing

Code Quality

Tool	Description
`calor_lint`	Check agent-optimized format issues
`calor_format`	Format source to canonical style
`calor_validate_snippet`	Validate incremental code snippets

Tool	Description
`calor_obligations`	Generate and verify refinement type obligations
`calor_suggest_fixes`	Suggest ranked fix strategies for failed obligations
`calor_discover_guards`	Discover Z3-validated guards for failed obligations
`calor_suggest_types`	Analyze parameter usage and suggest refinement types
`calor_diagnose_refinement`	All-in-one repair tool with ranked patches

Syntax & Help

Tool	Description
`calor_syntax_help`	Get syntax documentation for a feature
`calor_syntax_lookup`	Look up Calor syntax for a C# construct
`calor_explain_error`	Explain an error code or message with fix patterns
`calor_ids`	Check/assign declaration IDs
`calor_self_test`	Run compiler self-test against golden files

Tool Details

calor_typecheck

Type check Calor source and return categorized errors.

Input:

JSON

{
  "source": "§M{m001:Test}...",
  "filePath": "optional/path.calr"
}

Output:

JSON

{
  "success": false,
  "errorCount": 1,
  "warningCount": 0,
  "typeErrors": [
    {
      "code": "Calor0200",
      "message": "Type mismatch: expected i32, got str",
      "line": 5,
      "column": 10,
      "severity": "error",
      "category": "type_mismatch"
    }
  ]
}

Error Categories:

type_mismatch - Incompatible types
undefined_reference - Unknown symbol
duplicate_definition - Symbol already defined
invalid_reference - Invalid use of symbol
other - Other errors

calor_verify_contracts

Verify function contracts using Z3 SMT solver.

Input:

JSON

{
  "source": "§M{m001:Test}\n§F{f001:Div:pub}\n§I{i32:a}\n§I{i32:b}\n§O{i32}\n§Q (!= b 0)\n§R (/ a b)\n§/F{f001}\n§/M{m001}",
  "timeout": 5000
}

Output:

JSON

{
  "success": true,
  "summary": {
    "total": 1,
    "proven": 1,
    "unproven": 0,
    "disproven": 0,
    "unsupported": 0,
    "skipped": 0
  },
  "functions": [
    {
      "functionId": "f001",
      "functionName": "Div",
      "contracts": [
        {
          "type": "precondition",
          "index": 0,
          "status": "proven"
        }
      ]
    }
  ]
}

Contract Statuses:

proven - Z3 proved the contract holds
unproven - Could not prove or disprove
disproven - Found counterexample (includes counterexample field)
unsupported - Contract uses unsupported features
skipped - Verification skipped

calor_goto_definition

Find the definition location of a symbol.

Input:

JSON

{
  "source": "...",
  "filePath": "optional/path.calr",
  "line": 10,
  "column": 15
}

Output:

JSON

{
  "found": true,
  "filePath": "path.calr",
  "line": 3,
  "column": 1,
  "symbolName": "MyFunction",
  "symbolKind": "function",
  "preview": "§F{f001:MyFunction:pub}"
}

calor_find_references

Find all references to a symbol.

Input:

JSON

{
  "source": "...",
  "line": 5,
  "column": 10,
  "includeDefinition": true
}

Output:

JSON

{
  "success": true,
  "symbolName": "calculateTotal",
  "referenceCount": 3,
  "references": [
    {
      "line": 5,
      "column": 10,
      "isDefinition": true,
      "kind": "function",
      "context": "§F{f001:calculateTotal:pub}"
    },
    {
      "line": 15,
      "column": 5,
      "isDefinition": false,
      "kind": "reference",
      "context": "§C{calculateTotal} §A items §/C"
    }
  ]
}

calor_document_outline

Get a hierarchical outline of all symbols in a file.

Input:

JSON

{
  "source": "...",
  "includeDetails": true
}

Output:

JSON

{
  "success": true,
  "moduleName": "Calculator",
  "moduleId": "m001",
  "symbols": [
    {
      "name": "add",
      "kind": "function",
      "line": 2,
      "detail": "(a: i32, b: i32) -> i32",
      "children": [
        {"name": "a", "kind": "parameter", "detail": "i32"},
        {"name": "b", "kind": "parameter", "detail": "i32"}
      ]
    }
  ],
  "summary": {
    "functionCount": 2,
    "classCount": 1,
    "interfaceCount": 0,
    "enumCount": 0,
    "delegateCount": 0
  }
}

calor_obligations

Generate and verify refinement type obligations using Z3.

Input:

JSON

{
  "source": "§M{m001:Test} §RTYPE{r1:NatInt:i32} (>= # INT:0) ...",
  "timeout": 5000,
  "function_id": "f001"
}

Output:

JSON

{
  "success": true,
  "summary": {
    "total": 2,
    "discharged": 1,
    "failed": 0,
    "timeout": 0,
    "boundary": 1
  },
  "obligations": [
    {
      "id": "obl_0",
      "kind": "RefinementEntry",
      "function_id": "f001",
      "description": "x must satisfy (>= # INT:0)",
      "status": "Boundary",
      "line": 5,
      "column": 3
    }
  ],
  "compilation_errors": []
}

Obligation Statuses:

Discharged — Z3 proved the condition
Failed — Z3 found a counterexample (includes counterexample field)
Timeout — Solver exceeded time limit
Boundary — Public API entry point, can't verify callers
Unsupported — Contains unsupported Z3 constructs

calor_suggest_types

Analyze parameter usage patterns and suggest refinement types.

Input:

JSON

{
  "source": "§M{m001:Test} ...",
  "function_id": "f001"
}

Output:

JSON

{
  "success": true,
  "suggestions": [
    {
      "function_id": "f001",
      "parameter_name": "b",
      "current_type": "i32",
      "suggested_predicate": "(!= # INT:0)",
      "reason": "used_as_divisor",
      "confidence": "high",
      "calor_syntax": "§I{i32:b} | (!= # INT:0)"
    }
  ]
}

Detection Patterns:

used_as_divisor (high) — Parameter appears as divisor
used_as_index (high) — Parameter used as array index
compared_geq_zero (medium) — Compared against zero
compared_gt_zero (medium) — Compared strictly greater than zero

calor_suggest_fixes

Suggest ranked fix strategies for failed obligations.

Input:

JSON

{
  "source": "...",
  "obligation_id": "obl_0"
}

Output:

JSON

{
  "success": true,
  "fixes": [
    {
      "obligation_id": "obl_0",
      "strategy": "add_precondition",
      "description": "Require callers to satisfy constraint",
      "confidence": "high",
      "template": "§Q (>= x INT:0)"
    }
  ]
}

Strategies:

add_precondition — Require callers to satisfy constraint via §Q
add_guard — Runtime check at function entry
refine_parameter — Change parameter type to use a refinement type
strengthen_precondition — Make existing preconditions stricter
mark_unsafe — Suppress obligation (not recommended)

calor_discover_guards

Discover guards that would discharge failed obligations, validated by Z3.

Input:

JSON

{
  "source": "...",
  "obligation_id": "obl_0"
}

Output:

JSON

{
  "success": true,
  "guards": [
    {
      "obligation_id": "obl_0",
      "description": "Add precondition requiring b != 0",
      "calor_expression": "§Q (!= b INT:0)",
      "insertion_kind": "precondition",
      "confidence": "high",
      "validated": true
    }
  ]
}

Insertion Kinds:

precondition — Add as §Q (...) before function body
if_guard — Wrap in §IF returning error
assert — Use §PROOF{...} (...)

All-in-one repair tool — combines obligations, guards, and type suggestions into ranked patches.

Input:

JSON

{
  "source": "...",
  "policy": "default"
}

Output:

JSON

{
  "success": true,
  "policy": "default",
  "summary": { "total": 2, "discharged": 1, "boundary": 1 },
  "patches": [
    {
      "obligation_id": "obl_0",
      "obligation_status": "Boundary",
      "policy_action": "AlwaysGuard",
      "patch_kind": "precondition",
      "calor_code": "§Q (!= b INT:0)",
      "description": "Add precondition for b",
      "confidence": "high",
      "discharges_obligations": ["obl_0"]
    }
  ],
  "compilation_errors": []
}

Policies:

default — Failed = Error, Timeout = WarnAndGuard, Boundary = AlwaysGuard
strict — All non-discharged = Error
permissive — Failed = WarnAndGuard, never errors

Protocol Details

Request Format

JSON

{"jsonrpc":"2.0","id":1,"method":"tools/call","params":{"name":"calor_typecheck","arguments":{"source":"..."}}}

Response Format

JSON

{"jsonrpc":"2.0","id":1,"result":{"content":[{"type":"text","text":"{...}"}]}}

Supported Methods

Method	Description
`initialize`	Initialize the MCP connection
`tools/list`	List available tools
`tools/call`	Execute a tool
`ping`	Health check

Debugging

To debug MCP communication:

Bash

# Run with verbose logging
calor mcp --verbose 2>mcp.log

# In another terminal, watch the log
tail -f mcp.log

mcp

Overview

Quick Start

Options

Claude Code Integration

Gemini CLI Integration

GitHub Copilot Integration

Available Tools

Compilation & Verification

Code Navigation (LSP-style)

Analysis & Migration

Code Quality

Refinement Types & Obligations

Syntax & Help

Tool Details

calor_typecheck

calor_verify_contracts

calor_goto_definition

calor_find_references

calor_document_outline

calor_obligations

calor_suggest_types

calor_suggest_fixes

calor_discover_guards

calor_diagnose_refinement

Protocol Details

Request Format

Response Format

Supported Methods

Debugging

See Also