Skip to content

Verification and gates

Every mini-ork run ends in a verdict. The verdict is not a summary written by a model: it is the result of gates that executed, and it carries the evidence that produced it. This page explains what a verdict means, what evidence backs it, and what to do with each outcome.

The one rule

A model may propose a check or veto a result. It may never approve one.

The source of truth is what the code did when it ran. A reviewer that says "looks good" cannot turn a failing test into a pass; it can only turn a passing run into a refusal.

That rule is why the verdict vocabulary is closed:

Verdict Meaning What to do
PROVEN The required evidence was produced and holds Review the diff, then ship
REFUTED The evidence contradicts the claim, and the evidence is attached Read the failing gate; fix and re-run
UNVERIFIED The evidence could not be established — an abstention Do not ship; make the check runnable
VACUOUS The run passed nothing with discriminating power Treat as a failure

UNVERIFIED is deliberately not a soft pass. "We could not tell" and "we checked and it is fine" are different outcomes, and the system keeps them apart.

What a gate is

A gate is a named evaluator that receives artifacts and a context and returns a decision with evidence. Gates are registered by type, so a recipe can require one by name:

default_gates:
  - scope_gate
  - budget_gate
  - deployment_gate
Gate family Typical question
Scope Did the change touch only the declared surface?
Budget Did the run stay inside its cost and time caps?
Deployment Is the artifact in a shippable state?
Test Does the command run and pass?
Behavioral Does the observable contract hold under the declared equivalence operator?
Suite adequacy Could the suite have caught a defect at all?

A rejection must cite evidence. A gate that cannot name the artifact, command and observed result does not get to refute a run.

The five correctness levels

A single green test does not imply correctness. The level vector makes the difference explicit — each level is derived independently from execution artifacts, never from reviewer output:

Level Evidence PROVEN when
applies implementer summary Implemented, with a non-empty file list
executes test verifier The runner reached test outcomes
target test verifier The suite is green and the replay proves it exercises the change
preserve test verifier No regression, and the suite is not adequacy-unverified
contract behavioral verifier The behavioral contract is PROVEN (or n/a when absent)

Missing evidence makes a level UNVERIFIED, never PROVEN. The publisher requires its recipe's levels — code-fix, for example, requires applies, executes, target and preserve:

  • all required levels PROVEN → publish;
  • any REFUTED → fail the run and compensate;
  • anything else → withhold the commit without rolling back the fix.

That last case is intentional: an abstained fix stays in the tree for a human to inspect, instead of being silently discarded.

MO_LEVEL_VECTOR controls the feature (on by default).

Suite adequacy

A green suite is only evidence if the suite can detect faults. mini-ork seeds deterministic AST mutants into the files a candidate changed — comparison flips, arithmetic swaps, boolean negation, off-by-one constants, return None — and reruns the suite against a temporary copy. The score is killed / total.

Result Effect
ADEQUATE The green stands
INADEQUATE The green becomes UNVERIFIED
UNVERIFIED Downgraded as above; the instrument applied but could not measure
NOT_APPLICABLE No relevant source changed; the green stands

The full report lands in suite_adequacy.json in the run directory, with each survivor named as file:line operator original -> mutated. That list is the most actionable artifact a weak suite produces.

Knobs: MO_SUITE_ADEQUACY, MO_SUITE_ADEQUACY_MAX_MUTANTS (12), MO_SUITE_ADEQUACY_MIN_SCORE (0.6), MO_SUITE_ADEQUACY_TIMEOUT_S (300).

The oracle terms

mini-ork certify adds two terms that attack the "special-case the test" hole:

  • Metamorphic relations — a transform and a relation that must hold for both the original and the transformed input. A patch that special-cases the reported input breaks the relation.
  • Differential check — one input suite split into a bug_domain and a preserve group. A correct fix diverges only inside the bug's domain.

Both only veto a would-be PROVEN; neither can rescue a failure. See Certifying a change and Architecture: verification stack.

Reading a verdict

Start with run-verdict.json in the run directory:

.mini-ork/runs/<run-id>/
  verifier-test.log        the test command's raw output
  verifier-*.log           one per gate
  suite_adequacy.json      the mutation report, when it ran
  run-verdict.json         verdict, reasons, levels

A minimal verdict carries the decision, the reasons, and the level vector:

{
  "verdict": "REFUTED",
  "reasons": ["target: replay found no test exercising the change"],
  "levels": {"applies": "PROVEN", "executes": "PROVEN", "target": "UNVERIFIED"}
}

Then answer these in order:

  1. Which level or gate produced the decision? The reason names it.
  2. What was the evidence? The named log or JSON file contains the command and its output.
  3. Was the evidence trustworthy? A harness error, a missing dependency or a timeout is UNVERIFIED, not REFUTED.

Calibrating the verifier

Verifier mistakes are ground truth about the verifier, and they are recorded:

mini-ork verifier list
mini-ork verifier annotate <result-id> --false-positive
mini-ork verifier annotate <result-id> --false-negative

Label a result when you find one in review. The annotations feed abstention-gate calibration; a verifier that refutes correct fixes is a bug in the verifier, and without labels it looks like rigor.

Turning verification off

Each term has a master knob. Setting it to 0 restores the pre-feature behaviour byte for byte:

MO_ASSAY_RELATIONS=0 MO_ASSAY_DIFFERENTIAL=0 mini-ork certify --base main --head fix --issue "..."
MO_SUITE_ADEQUACY=0 MO_LEVEL_VECTOR=0 mini-ork run code-fix ./kickoff.md

Use this for debugging a suspected false refusal — and turn it back on.

Decision table

Situation Action
PROVEN, all required levels PROVEN Review the diff; merge
PROVEN, contract is n/a Fine if the recipe does not require it
REFUTED on target The replay did not exercise the change; add or scope a failing test
REFUTED on preserve A regression; inspect the named test
UNVERIFIED with a harness error Fix the environment, re-run; do not treat as failure of the change
VACUOUS The run proved nothing; add a discriminating check
INADEQUATE suite Strengthen the suite; the survivors name what is untested

Next