Adoption Playbook

Adopt Calor one module at a time, review what remains unproven, and keep a tested exit path

Calor adoption is deliberately incremental: place a .calr module beside your C# sources, let the MSBuild SDK compile it, and expand only after the verification and effect reports are useful to your team.

The project has not established a qualifying adopter, independent adopter handoff, economic advantage, or safety advantage over protected C#. Read the research evidence status before treating repository benchmarks as an adoption result.

Read This Before Adopting

• Calor is pre-1.0. Syntax and semantics are versioned, but there is no broader compatibility promise yet.
• The project has one maintainer. The mitigation is a tested eject path: generated C# is yours and can be built without continuing to author Calor.
• Refinement types are not runtime-enforced. Their obligations are compile-time analysis. Contracts (§Q and §S) are the constructs that can emit runtime checks.
• Waivers void guarantees. --permissive-effects assumes unknown calls are pure. --contract-mode off removes contract checks. A review packet produced with either option says so on its first line.
• Workflow savings are unmeasured. The project has not established that Calor reduces total review/repair cost versus ordinary or strongly protected C#. No qualifying adopter or independent handoff was established.

Start with pure, contract-dense modules and first-order effect-checked code. Delegate-heavy or reflection-heavy service layers are a poor first target. Treat the first module as your own bounded pilot: record translation, compiler, review, repair, and eject-path costs before expanding.

1. Install the MSBuild SDK

Pin the package in global.json:

{
  "msbuild-sdks": {
    "Calor.Sdk": "<version>"
  }
}

Reference it from the project that contains your Calor modules:

<Project Sdk="Microsoft.NET.Sdk">
  <Sdk Name="Calor.Sdk" />
  <PropertyGroup>
    <TargetFramework>net10.0</TargetFramework>
    <CalorVerify>true</CalorVerify>
  </PropertyGroup>
</Project>

The package contains the build task, compiler/runtime dependencies, and Z3 natives. CalorVerify=true runs the contract verification gate during the build. Type checking and effect enforcement are on by default; the explicit MSBuild opt-outs are CalorTypeCheck=false and CalorEnforceEffects=false. For converted code, CalorPermissiveEffects=true is the gentler step — it keeps effect checking on but goes easy on calls the compiler cannot look up. The full list of build settings is on the calor init page.

2. Add a Small Module

§M{m001:Pricing}
  §F{f001:ClampToCap:pub} (i32:amount, i32:cap) -> i32
    §Q (>= cap 0)
    §S (<= result cap)
    §IF{if1} (> amount cap)
      §R cap
    §R amount

• §Q preconditions and §S postconditions receive one of the documented proof statuses where verification is requested. Only a clean, non-vacuous, assumption-free proven result can authorize guard removal; runtime checks also depend on contract mode and supported lowering.
• §E{...} declares effects; §E{} is explicitly pure.
• A missing declared effect is an error with its call chain.

3. Import Dependency Effects

calor import Serilog --project .
calor import path/to/Some.Assembly.dll

calor import classifies every public member into three tiers:

Nothing generated by import is labeled verified. Mechanical facts synthesized from nullable metadata or unsigned parameters go into a .calor-contracts.json sidecar with assumed provenance. The verifier does not consume that sidecar as trusted input.

See calor import for all options.

4. Query the Project Before Editing

Before editing an established module, ask the project index what the edit can affect:

calor query callers ClampToCap
calor query effects ClampToCap
calor query impact ClampToCap

For a proposed effect change, include the new row:

calor query impact ClampToCap --effects --row "cw"

Read any PARTIAL residual before trusting the count. MCP clients can ask the same questions with calor_query, then compile the result with options.crossModule: true. See Project Intelligence for Agents for the complete workflow.

5. Review the Unproven Remainder

calor review-packet src/Pricing.calr --baseline-ref origin/main

The packet leads with every contract that is not cleanly proven, grouped by the seven proof statuses. It includes assumption lists, vacuity flags, counterexamples, interop and waiver fractions, and the direct callers of changed declarations. --json emits the same information in the command envelope.

The claim is intentionally narrow: proven means proven under the modeled semantics. Everything else remains visible with its reason.

6. Keep the Eject Path Open

calor convert Module.calr produces standalone C#. The eject suite compiles and executes the result to pin these degradation rules:

Ejecting costs the proof and effect discipline, not ownership of the generated code.

Next Steps

• Adding Calor to Existing Projects — Detailed setup and migration mechanics
• Verification Guarantees — Exactly what each proof status means
• Effect Manifests — External effect coverage
• Review Packet — Per-change review output