Counterexamples

When the solver cannot prove an obligation, it returns sat on the negated goal — a concrete assignment of values that violates the claim. Verum turns those raw models into actionable counterexamples that point at real values in the user's code.

Counterexamples are the proof system's equivalent of a test failure with a recorded input. Understanding what's in one, how it's extracted, and how it's minimized is the difference between a quick fix and a morning spent squinting at raw solver model dumps.

---

1. When a counterexample is emitted

Any of these strategies produce counterexamples on failure:

Strategy	On failure emits counterexample?
Runtime	No — runtime assertion panics with the violating value directly.
Static	Yes — build error with counterexample.
Formal	Yes — build error with counterexample.
Fast	Yes — but minimization is skipped (keep build times low).
Thorough	Yes — with minimization and hypothesis-reduction pass.
Certified	Yes — with minimization and a note indicating which backends agreed.
Synthesize	The synthesizer returns no candidate; "counterexample" is a class of inputs for which no closed-form body exists.

Obligations that return unknown (solver timed out or hit its resource limit) do NOT produce counterexamples — the solver could not decide, so no violating instance was constructed. A unknown outcome is reported separately with a diagnostic distinguishing it from sat.

---

2. Anatomy of a counterexample

A full counterexample (at --counterexample=full) contains:

error<E500>: contract violation — ensures clause failed
  --> core/math/arith.vr:42:5
   |
40 | fn safe_div(a: Int, b: Int) -> Int
41 |     requires b != 0
42 |     ensures result == a / b
   |     ^^^^^^^^^^^^^^^^^^^^^^^ this ensures clause is falsifiable
43 | {
44 |     a / b
45 | }
   |

Counterexample:
    a = -3
    b = 2
    result = -1   (expected: -2 for floor division, got -1 for truncation)

Contradiction:
    a / b computes via truncation: -3 / 2 == -1
    The ensures clause reads a / b symbolically as floor: -3 / 2 == -2
    The two disagree at negative dividends.

Source chain:
    - `result == a / b`   at line 42:13 (ensures clause)
    - body evaluates `a / b` via Int.div(a, b)  at line 44
    - Int.div is truncating; floor_div available as separate intrinsic

Suggested fixes:
  1. Use `a.floor_div(b)` if you meant floor division.
  2. Weaken the ensures to `a / b == result && (a < 0 && b > 0 ⇒ result * b >= a)`.
  3. Extract a pure helper that models truncation correctly, so it
     reflects.

help: run `verum verify --counterexample=minimal core/math/arith.vr`
      for the single-page version without source-chain detail.

The four fields (free-variable assignments, contradiction, source chain, suggested fixes) are produced in order by distinct pipeline stages; see §4 for the implementation path.

---

3. Modes

3.1 none

Suppresses counterexample printing; still emits the error. Use for CI pipelines where artefacts are collected separately.

3.2 minimal (default in Fast)

Only the free-variable assignments. One or two lines per variable:

Counterexample:
    a = -3, b = 2, result = -1

3.3 standard (default in Static, Formal)

Free-variable assignments + a one-line contradiction statement. No source chain, no fix suggestions.

3.4 full (default in Thorough, Certified)

All four fields as shown in §2.

3.5 json

Machine-readable. The shape is stable across versions (schema versioned). Useful for IDE integrations and CI dashboards.

{
  "schema_version": 1,
  "file": "core/math/arith.vr",
  "span": { "start": { "line": 42, "col": 5 }, "end": { "line": 42, "col": 28 } },
  "clause": "ensures",
  "assignments": [
    { "name": "a", "value": -3, "type": "Int" },
    { "name": "b", "value": 2, "type": "Int" },
    { "name": "result", "value": -1, "type": "Int" }
  ],
  "contradiction": "a / b computes via truncation; ensures reads a / b as floor division",
  "source_chain": [
    { "file": "core/math/arith.vr", "line": 42, "col": 13, "reason": "ensures clause body" },
    { "file": "core/math/arith.vr", "line": 44, "col": 5,  "reason": "body evaluates via Int.div" }
  ],
  "suggested_fixes": [ "use .floor_div", "weaken ensures", "extract a pure helper" ]
}

---

4. Extraction pipeline

A counterexample is built in three steps. Everything in this section lives in verum_smt::counterexample.

4.1 Steps 1 and 2 — Model extraction and naming

When the SMT layer returns sat, CounterExampleExtractor::new takes the solver's model and extract(var_names, constraint) walks it once, keeping the constants whose declaration name matches one of the variables asked for and converting each interpretation into a CounterExampleValue (Int, Bool, Float, Text, arrays).

Extraction and naming are the SAME pass, not two: extract_value finds a constant BY ITS VERUM NAME in the model's declarations, so there is no separate raw stage to translate back from.

Implementation: verum_smt::counterexample::CounterExampleExtractor — new(&model) then extract(&var_names, constraint).

4.2 Step 3 — The contradiction line

CounterExample::new derives its description from the assignments and the violated constraint: an empty assignment map yields Constraint '<c>' is always false, and otherwise the description lists name = value pairs in sorted order alongside the constraint.

This is a formatting step over the model, not an abstract interpretation of the goal.

Implementation: CounterExample::new (its private generate_description); rendered for the user by CounterExample::format_with_suggestions.

4.4 Stage 4 — Minimization

Verum applies minimization in two phases — one pure, one solver-backed:

Phase 4a: syntactic minimization (always applied). Pure zero-callback pass that drops every assignment whose variable name doesn't appear in the violated constraint string. SMT solvers frequently report helper-predicate constants the user never wrote; the syntactic pass removes those so the counterexample mentions only the variables the violation actually depends on.

Word-boundary matching: x is kept only when the constraint contains x as a whole identifier token — substring match in xyz does NOT count. This keeps the pruner conservative on false negatives (false positives are cheap — we keep an unused variable; false negatives are bugs — we'd hide a relevant one).

Phase 4b: delta-debugging minimization (CounterExampleMinimizer::minimize, reached through CounterExampleAnalyzer::minimize). It takes a caller-supplied is_failing predicate and drops assignments one at a time, keeping a variable only when removing it stops the obligation failing. The predicate is where a re-solve happens, so the cost belongs to the caller rather than to this pass.

Pipeline composition: extract → minimize_syntactic → minimize. The syntactic pass reduces the input domain for the delta-debugging pass; a caller that supplies no predicate runs only the syntactic one (no re-solve cost).

The reductions are per-ASSIGNMENT (drop a variable and retest). Value-narrowing inside a variable — binary-searching an integer toward zero, shrinking a List<T> element by element — is not implemented, and neither is a timeout on the pass.

4.5 Step 4 — Suggestions

verum_smt::counterexample::generate_suggestions(counterexample, constraint) reads the CONSTRAINT TEXT and the assignments and emits plain-language advice. The rules it has today:

• a numeric comparison whose witness violates it — "Add precondition: require x > 0", naming the variable and the bound taken from the constraint;
• a constraint containing / — check for division by zero;
• a constraint mentioning length or size — verify indices are within bounds;
• otherwise a single fallback: "Add stronger preconditions to rule out this case".

The output is rendered by CounterExample::format_with_suggestions.

The rule base is a fixed if-chain over the constraint string, not a plugin surface and not AST-driven; there is no rule module to extend.

4.6 Failure-category classification

Every counterexample carries a structured FailureCategory tag that classifies the runtime-safety failure mode. The category drives IDE quick-fix dispatch, telemetry counters, and documentation links — consumers branch on the category rather than parsing the human-readable contradiction string.

The taxonomy is closed (six tags, additions are language-version events) and partitions into three orthogonal axes via classifier flags. The full table:

Category	is_arithmetic_failure	is_memory_failure	has_quickfix_pattern	is_catch_all
DivisionByZero	✓		✓
ArithmeticOverflow	✓		✓
IndexOutOfBounds		✓	✓
NullDereference		✓	✓
NegativeValue	✓		✓
Other				✓

Two cross-cutting invariants are pinned by the meta_pin_failure_category_round_trip_and_partitions drift-test in verum_smt::counterexample and surface as a test failure if they ever diverge:

• Arithmetic ⊕ memory — a category is arithmetic, memory, or neither (the catch-all), never both. Pinned so a future hybrid category (e.g. "pointer arithmetic overflow") forces an explicit reclassification.
• has_quickfix_pattern ⇔ ¬is_catch_all — exact equality. Every named category has a structured guard the IDE can offer (x != 0 for DivisionByZero, bounds check for IndexOutOfBounds, etc.); only the catch-all Other doesn't. Adding a new named category that lacks a quick-fix pattern surfaces here.

Each variant carries a display_name field (e.g. "Division by Zero", "Index Out of Bounds") that the JSON wire and the human emitter share — single source of truth for the human-readable category label. The legacy Display impl that previously hardcoded the six display strings inline now reduces to one line that reads from the FailureCategory::meta() table.

The category is exposed in the JSON wire as the category field alongside the per-variant flag set:

{
  "schema_version": 1,
  "category": {
    "name": "division_by_zero",
    "display_name": "Division by Zero",
    "is_arithmetic_failure": true,
    "is_memory_failure": false,
    "has_quickfix_pattern": true,
    "is_catch_all": false
  },
  ...
}

IDE plugins that want to render a "show only memory-safety failures" filter, or a CI dashboard that wants to count arithmetic-domain regressions separately, branch on the classifier flags rather than enumerating variant names. New categories ship with their classifier-flag answers pre-decided in core_metadata-style fact-pack tables, which means consumers never need to handle "unknown category" fallback paths — every FailureCategory value the runtime emits has a complete fact-pack.

---

5. Counterexamples for quantified obligations

Universal claims (forall x in domain. P(x)) need special care. The solver returns a single x that falsifies P; the counterexample framework elaborates:

Counterexample (universal):
    forall x in 0..n. sorted[x] <= sorted[x+1]

    Falsifying x = 3, n = 5
    sorted[3] = 7
    sorted[4] = 2
    Contradiction: 7 <= 2 is false.

Source chain:
    - sorted comes from quicksort(arr)  at line 12
    - arr had no partial-order invariant on input

Existential claims (exists x. P(x)) report "no witness found within search depth" with the search depth used; the claim may still be true beyond that depth — the report says so explicitly.

---

6. Counterexamples and framework axioms

If the proof uses a @framework(id, "citation") axiom, and the proof fails, the diagnostic lists the framework dependency:

error<E500>: theorem proof failed
    bridge_to_n_7
    proof required framework axiom: baez_dolan_hda::aut_o_is_g2

  note: the framework axiom itself was trusted;
        the failure is in the non-axiom portion of the proof.

This helps the user distinguish "I'm missing a step" from "I cited the wrong axiom."

See Framework axioms.

---

7. When the solver returns unknown

Not a counterexample: the solver could not decide. Typical causes and diagnostics:

Cause	Mitigation
Timeout	--timeout 120 (or Thorough strategy).
Nonlinear arithmetic explosion	Switch to a stronger adapter via --solver smt-backend; or decompose manually.
Unbounded quantifier instantiation	Add @trigger to help the solver pick patterns.
Predicate never reflected	Check the reflection warnings — a skipped entry names the leaf.
Theory combination at a hard boundary	Use the Certified strategy to race both backends.

The diagnostic for unknown is distinct from a counterexample — it does NOT assert the claim is false, only that the solver could not conclude either way.

---

8. Interactive counterexample exploration

verum verify --interactive scans the project, lists the files with verification issues, and offers a small prompt over them:

  Welcome to Verum interactive verification!
  Scanning project for functions with verification issues...

  Files with verification issues:

    1. core/math/arith.vr
       Issue: <the verifier's message>

  Commands:
    1-N:  Re-verify file with increased timeout
    help: Show proof tactics
    quit: Exit interactive mode

  >

So the loop is per-FILE re-verification with a longer budget, plus a tactics reminder. Per-obligation commands over a counterexample — show failed, explain <n>, reduce <var>, trace — are not implemented; an earlier revision of this page documented them as though they were.

Implementation: verum_cli::commands::verify::execute_interactive.

---

9. What counterexamples are NOT

• Not tests. Running the function on the counterexample value may or may not crash; the counterexample is a logical counterexample to the specification, not necessarily a runtime crash.
• Not guaranteed minimal. Minimization is bounded (30s default). For large obligations the reported instance may still be reducible.
• Not a proof of P(x) for all other x. A counterexample proves ¬∀ P, i.e. there exists one falsifier. It does NOT say "almost all inputs falsify."
• Not stable across solver versions. Different solver adapters may pick different models for the same unsat query; the reported counterexample is whichever came first in the portfolio race.

---

10. Extensions

• Delta-debugging at the AST level: minimize the program, not just the inputs, to isolate the contradiction.
• Counterexample diffing: when a proof starts failing, diff the new counterexample against the last-known-good one.
• Counterexample replay: treat the counterexample as a property-test seed; plug it into cargo run / verum run to exercise the concrete machine.
• Counterexamples for quantifier-heavy goals: improved Skolemization reporting so "exists x" failures name the quantifier bound rather than a synthetic Skolem constant.
• IDE integration: counterexamples as inline hover tooltips in VS Code (see LSP).

---

See also

• SMT routing — which backend produced the sat verdict.
• Proofs — when you write a proof, the failing tactic and its residual goal are shown instead.
• Performance tuning — how to profile and accelerate verification.
• CLI workflow — counterexample flags in context.