Guides

Practical guides for common Calor workflows and tasks.

Available Guides

Adoption Playbook

The v0.12 adopter workflow: package setup, dependency import, review packets, waiver disclosure, and the tested C# eject path.

Verification Guarantees and Limits

How to read the seven proof statuses, which v0.12 soundness boundaries force an assumed or unsupported result, and when runtime checks remain.

Adding Calor to Existing Projects

A comprehensive guide for integrating Calor into an existing C# codebase. Covers:

• Analyzing your codebase for migration candidates
• Setting up tooling and MSBuild integration
• Converting files gradually
• Using Claude Code for assisted migration

Dependent Types Tutorial

A progressive tutorial on refinement types and the MCP-guided agent repair loop. Covers:

• API parameter validation with inline refinements vs. C# boilerplate
• Financial calculations with proof obligations and Z3 verification
• The MCP agent workflow: suggest types → check obligations → discover guards → diagnose and repair

Effect Manifests: .NET Ecosystem Coverage

How Calor knows the effects of .NET framework and ecosystem library calls. Covers:

• What's covered: ~170 types across BCL, framework interfaces, and ecosystem libraries
• How resolution works: short name mapping, variable type tracking, priority layers
• Adding custom manifests for your own types
• Effect code reference and CLI tools

Cross-Assembly IL Analysis

Automatic effect discovery through referenced .NET assemblies. Covers:

• How the compiler traces SaveChanges → db:w through your data access layer
• What it finds (concrete call chains, async, delegates) and what it doesn't (interfaces, reflection)
• Enabling IL analysis with one MSBuild property
• Performance, diagnostics, and interaction with manifests

Cross-Module Effect Propagation

How Calor verifies effect declarations stay consistent across files in a multi-file project. Covers:

• The contract model: declared effects propagate between modules
• Bare-name vs. qualified calls and ambiguity handling
• The Calor0417 warning for undeclared public functions
• Warm-build correctness via cached effect summaries
• Multi-file CLI and MSBuild integration

Telemetry and Privacy

The opt-in default, exact metadata inventory, and the data Calor never sends.

Getting Started

If you're new to Calor, start with the Getting Started section instead. These guides assume familiarity with Calor basics.