verify
Run Z3 contract verification and report the seven-status outcome for every obligation
calor verify <files...> [options]
Examples
calor verify src/Math.calr
calor verify a.calr b.calr --timeout 10000
calor verify src/Math.calr --format json
calor verify old.calr new.calr --weakening-check f001
Options
| Option | Description |
|---|---|
--format, -f | text or json |
--output, -o | Write output to a file instead of stdout |
--verbose, -v | Include detailed verification information |
--timeout, -t | Solver budget per contract in milliseconds; default 5000 |
--no-cache | Disable verification-result caching |
--clear-cache | Clear the verification cache first |
--weakening-check | Compare one declaration across exactly two files for contract weakening |
Status and Exit Contract
The schema 2.0 wire statuses are proven, refuted, assumed, unknown,
timeout, unsupported, and unavailable. assumed carries a named
assumption list. refuted includes structured counterexample bindings when Z3
produces a model. Vacuity is a separate flag.
| Exit | Meaning |
|---|---|
0 | No contract was refuted and compilation succeeded; inconclusive outcomes may still be present |
1 | A contract was refuted, a file was missing, or compilation failed |
2 | Invalid weakening-check invocation |
When the Solver Is Missing
Verification needs the Z3 solver. If the Z3 native library is not installed
next to the compiler, nothing can be proved — so every contract comes back
Skipped, and the command still exits 0, because nothing was refuted.
Through 0.15 the plain text report said none of that: you saw a wall of
Skipped with no reason, and only --format json carried the explanation. New
in 0.16, the text report says it outright, for each file, above the counts it
explains:
File: c.calr
!! NOT VERIFIED: the Z3 solver is unavailable, so nothing below was proved.
Calor0710: Static contract verification skipped: Z3 SMT solver is not available. Install the Z3 native library for static verification support.
Proven: 0
Unproven: 0
Disproven: 0
Unsupported: 0
Skipped: 2
If you gate a build on calor verify, gate it on this line too. A run that
proved nothing exits 0 exactly like a run that proved everything.
Reporting, Not Rewriting
The command compiles its inputs before reporting contract results. Active
receiving-boundary errors (Calor0272–Calor0274) therefore fail verification
with exit 1; enabling verification does not bypass them. The text report
lists their messages under Errors, rather than displaying the root compile
command's diagnostic code and source span. Use the root compile command to
inspect that location. See the
Calor 0.22 nullability guide
for supported shapes and complete examples. A successful compile is not a proof
that all references are non-null. D3/D12/D14 string, array, and user-type proof
demotions remain in force, and #875
remains open.
calor verify reports verdicts; it never rewrites generated code. Guard
elision happens in calor --input file.calr --output file.g.cs --verify, where a clean
proven verdict drops its runtime guard by default; add
--keep-proven-guards there to retain otherwise-emitted guards.
--contract-mode off emits no checks, and enabled checks require supported
runtime lowering. See
Verification Guarantees before using
proof results as a gate.