Skip to main content

Gradual Verification

A single program spans the verification spectrum — runtime checks for prototypes, static analysis for ordinary code, formal proofs for critical invariants, certified cross-validated proofs for the kernel.

Verification in Verum is semantic, not backend-specific. You pick how much you want proved (the intent); the compiler picks the technique (the implementation). This lets the in-house solver improve without changing user code, and it lets a single project mix strategies file by file.

The nine strategies​

The grammar admits these nine surface keywords (the seven distinct behaviours plus two historical aliases):

StrategyWhat it doesWhen to use
runtimeruntime assertion check only; no formal proofprototyping, dev builds
staticstatic type-level verification only; no solverthe default fast path
formalformal verification with the default strategyproduction code
proofalias of formal — emphasises proof extractionwhen you want to look at the term
fastoptimise for fast verification; may give up on hard goalsiterative development
thoroughmaximum completeness — races several strategies, takes the first successhard obligations
reliablealias of thorough — emphasises result reliabilitycritical code
certifiedindependently cross-verified; required for exporting proof certificates (Coq / Lean / Dedukti / Metamath)security-critical, external audit
synthesizesynthesis — generate a term satisfying the spec instead of checking oneprogram synthesis, hole filling

formal is the recommended default. It's what @verify without an argument selects.

Requesting a strategy​

@verify(runtime)    fn prototype()  { ... }
@verify(static)     fn ordinary()   { ... }
@verify(formal)     fn critical()   { ... }
@verify(thorough)   fn safety()     { ... }
@verify(certified)  fn kernel()     { ... }
@verify(synthesize) fn synth()      { ... }

At the project level, set a default and per-module overrides in the [verify] section of verum.toml:

[verify]
default_strategy  = "formal"
solver_timeout_ms = 10000
enable_telemetry  = true        # write .verum/state/smt-stats.json
persist_stats     = true

[verify.modules."crypto.signing"]
strategy          = "certified"
solver_timeout_ms = 60000

Strategy-specific timeout multipliers apply: fast 0.3×, thorough 2×, certified 3×, synthesize 5×.

What each strategy actually does​

runtime​

Refinements become assert calls. ensures clauses become post-return checks. A failure panics the current task. Useful for rapid iteration.

static​

  • Dataflow: narrows types by control flow. if x > 0 { ... } strengthens x inside the branch.
  • CBGR: generation-check elision, escape analysis, reference-tier promotion (documented in cbgr internals).
  • Refinement typing: predicates checked via subtyping rules; no solver calls on the fast path.

formal / proof​

When a refinement or contract cannot be discharged syntactically, the compiler translates it to SMT-LIB and dispatches through the capability router (see SMT routing). The router picks the SMT backend based on the obligation's theory mix.

Results are cached keyed on the SMT-LIB fingerprint — a proof stays valid until the function or its dependencies change. Compile time scales linearly with the number of new obligations.

fast​

Like formal but the solver timeout is reduced to 30 % of the base, and non-trivial strategies (portfolio, proof extraction) are skipped. Goals that need more than a few hundred milliseconds are returned as "unknown" rather than blocking the build.

thorough / reliable​

Races the available strategies in parallel — direct SMT, SMT with quantifier hints, proof search, congruence closure — and accepts the first success. Timeout is 2× the base.

certified​

Runs thorough and cross-validates the result with an orthogonal verification technique. A disagreement between the two pipelines is a hard build error. The resulting proof is embedded in the VBC archive as a certificate exportable to Coq, Lean, Dedukti, or Metamath. Use this for code that will be externally audited.

synthesize​

Treats the goal as a synthesis problem: given a specification, generate a term (function body, witness, tactic) that satisfies it. Useful for filling in proof obligations or stubbing out code against a contract.

Proof obligations​

When the compiler cannot discharge an obligation syntactically it produces an obligation that looks like:

obligation binary_search/postcond at src/search.vr:25:5
  context:
    xs: List<Int>
    key: Int
    result: Maybe<Int>
  goal:
    result is Some(i) => xs[i] == key

The obligation is dispatched through the capability router and fed to the SMT backend, the portfolio executor, or the tactic evaluator based on the selected strategy.

Telemetry and stats​

Telemetry is opt-out via [verify] enable_telemetry. After a build that touched any verification:

$ verum smt-stats
  Strategy                      Goals   Median (ms)   p95     Hit rate
  formal                        14221   34           210     92.4 %
  thorough                         68  2840         9210      —
  certified                         4  7500        16400     100 %
$ verum smt-stats --json        # machine-readable
$ verum smt-stats --reset       # clear after printing

Stats persist in .verum/state/smt-stats.json when [verify] persist_stats = true (the default).

Moving up the ladder​

There is no flag-day — functions upgrade independently:

  1. Write at @verify(runtime).
  2. Annotate invariants; the compiler reports what it proved at @verify(static).
  3. Fill in ensures / refinement types for the invariants you care about, and add @verify(formal).
  4. For hard-to-prove invariants, escalate to @verify(thorough).
  5. For the critical 0.01 %, use @verify(certified) and review the exported proof.

See also​