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.

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.

Start with pure, contract-dense modules and first-order effect-checked code. Delegate-heavy or reflection-heavy service layers are a poor first target.

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.

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 are proved where their forms are modeled and otherwise remain runtime checks.
• §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. 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.

5. Keep the Eject Path Open

calor convert Module.calr produces standalone C#. The v0.12 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