6 · Reading a verdict

Every verification job ends with a verdict: UNSAT, SAT or STALL. This chapter says what each one establishes, what it does not, how the job tells you which part of the engine decided it, and when there is no verdict at all.

Two questions, two fields

A job answers two questions, and they are kept apart:

• Did the run work? That is the job's state: succeeded, failed or cancelled.
• What did it find? That is verdict.status.

Neither is derived from the other. A run that found a bypass worked perfectly: the job is succeeded, the HTTP status is 200, and the verdict is SAT. A finding is an answer, not an error, so nothing in the client raises on it. A pipeline that gates on the HTTP status or the exit code reads every bypass as a pass; gate on verdict.status.

result = client.verify_guardrail("transfers.co", "execute_transfer_funds", "is_authenticated")
print(result.state)        # did the run work: succeeded, failed or cancelled
print(result.status)       # what it found: UNSAT, SAT or STALL; None where the verdict is void
print(result.decided_by)   # which part of the engine decided
if result.status != "UNSAT":
    raise SystemExit("the obligation is not proved")   # gate on the verdict, never on the HTTP status

The three verdicts

Status	Meaning
UNSAT	No assignment of any remaining input makes the action fire with the context false. The bypass is impossible over the whole input space, and the certificate proves it.
SAT	A bypass exists, and the trace names the context assignment that reaches it. Check that it is reachable in reality: context variables are free and independent here, so a witness can describe a configuration that cannot occur.
STALL	Undecided: the solver ran out of degrees of freedom to eliminate. Not a proof of safety, and not a bypass either.

UNSAT: the obligation holds

No situation the inputs can describe makes the action fire with the context false, under the pins you gave. It covers every combination at once. What it does not mean:

• that the policy is safe. It means this one obligation holds; the others are other questions (chapter 4);
• that a certificate exists. Under the default fast profile there is none, and the refutation is the SAT solver's assertion: oracle_dependent is true and the verdict says so. Ask for patch when you need a certificate anyone can check (chapter 10);
• that the context is set correctly at run time. The verdict proves the policy consults the context before the action; whether your systems set the context truthfully is outside the policy.

SAT: the obligation is broken

A situation exists in which the action fires without the context, and the verdict names it: the values of the contexts and intents that reach the action. The witness is checked against the policy's own equations before it becomes a verdict, so it rests on no oracle at all. What it does not mean:

• that the situation can happen in your deployment. Contexts are treated as free and independent, so a witness can describe a combination your systems never produce. Check it against reality before you act on it, and pin away a combination that genuinely cannot occur;
• that there is only one way through. A witness is one; chapter 10 explains how to have every one of them counted.

Under patch or proof a SAT comes with a repair (chapter 8). Under fast it does not: fast decides, and a repair needs a second run under patch.

STALL: the run could not rule it out

The engine ran out of ways to eliminate and found no witness. There is no proof of safety, and no demonstrated bypass either. What it means depends on what is being checked:

• On a policy, a stall is acted on exactly as a SAT. A bypass you failed to rule out calls for the same response as one you proved: make the policy safe rather than wait for the incident that would settle the question. The run supplies the means: the same repair a SAT gets, with its proof (chapter 8). That is why a stall on a hard row of a property table fails it, as a SAT would (chapter 11).
• On a random forest, a stall concludes nothing: not that the property holds, and not that it fails. A deployed model is retrained rather than patched, so there is nothing to fold a repair into, and the question needs a narrower region instead (chapter 14).

A stall names its cause, which says what to do next. closure-fixpoint means the engine's method ran dry: this contradiction is not of the shape it derives, and a longer budget changes nothing. budget-expired, with rows still arriving when it stopped, means the budget was the limit and another run is worth having. The job's verdict.budget_exhausted says which.

Act on a stall second. First check the pins state the obligation: an obligation asked without its conditions can stall on a policy that is correct, and patching that makes the policy worse (chapter 4).

Who decided

verdict.decided_by names the phase that reached the verdict, such as phase0-cdcl (the SAT solver) or phase2-closure (the algebraic expansion). It matters because it says what the verdict rests on: a refutation the SAT solver reached is its assertion unless a proof was logged, while one the algebraic phases reached is a derivation a certificate can carry. The verdict block repeats the facts a consumer needs to branch on without reading the payload:

Field	Why
verdict.status	the verdict itself, and the one field every consumer branches on
verdict.decided_by	which phase decided it, so a consumer can tell a derived refutation from an oracle-asserted one without reading the certificate
verdict.certificate_detail	how much of the refutation was written down, which decides what the artefact can be used for
verdict.origin_class	whether the refutation was derived, asserted internally or handed over by an oracle: the difference between evidence and a claim to trust
verdict.oracle_dependent	true where the refutation rests on an external decision procedure. Reported beside the certificate rather than inside it, so it survives a run that built no certificate at all
verdict.self_contained	whether the document can be replayed without trusting us
verdict.budget_exhausted	whether a budget stopped the run. Not in the payload: a budget-stopped run is a valid partial closure and the binary reports the stop through the stall's exit reason, so the worker is what knows

The phases, briefly, so that decided_by reads as something:

Phase	What it does
0	Fast bounded CDCL: the system goes to CryptoMiniSat under a conflict budget, and the facts it settles and the XOR relations it learns come back.
1	Expansion of the linear constraints. Always on; it seeds the cascade.
1.5	Cross-multiplication of pivot rows, for early rank growth.
2	The cascade. Always on: it closes the system under multiplication by single variables until it reaches a fixpoint.
3	Border basis prolongation, for systems the degree-2 cascade cannot finish. The only phase that enumerates a variety, so max_roots above 1 needs it.
4	Condensation and fast exhaustive search over a small residual: whatever Phase 3 leaves undecided, when both run. Phases 3 and 4 are sequential stages of one endgame, and either or both may be enabled.

When there is no verdict

A verdict is only as good as the compilation it was reached over. A line of the policy the compiler did not understand is a rule the equations do not contain, and a missing rule reads as a bypass, or as a pass, that means nothing. So:

• Where a line the compiler could not read lies inside the question's reach (the part of the policy that can influence the action), there is no verdict: the job is refused as colang_unread_in_cone, or colang2_construct_unsupported for a Colang 2 construct, naming the line.
• Where such lines all lie outside that reach, the verdict stands, because they cannot change whether the action fires.
• Where the compile cannot place an unread line at all, the verdict is void: verdict_void is true and verdict.status is absent. A void verdict is not a weaker verdict; it is not a verdict, and it must not be quoted. The client reports status as None for it.

Every condition the compiler reports reaches the job as a diagnostic, each with its code:

Code	Meaning
parse_incomplete	lines of the policy were not understood. The circuit is missing whatever they expressed and a missing edge reports no bypass, so a non-zero count marks the verdict void
permissive_by_default	flows refuse on enumerated conditions and then leave an action reachable at flow level, so any context matching none of them reaches it. No reachability question surfaces this
policy_defects	the circuit is faithful and the file is the problem, so no verdict is reported at all
nonconforming	the certificate carries nothing a consumer can check. The run produced a payload and the binary still exits non-zero, so this is the case where reading the exit code as the verdict reports a failure over a successful job
unclassified	a defect line this service could not parse, carried with its text. Never dropped: the alternative reports a policy as shippable because we could not read the sentence saying it is not
patch_file_absent	the run proposed a corrective action and wrote no patch file. The binary emits one only where the action reduces to a guard over named variables, and says so in a console note otherwise, so this is reported rather than a patch invented to fill the gap

Two things are reported but void nothing. A policy warning, such as a flow that refuses on listed conditions and then lets everything else through (permissive_by_default), is a criticism of a file that compiled faithfully: worth a review, and no reason to discard the verdict. A pin naming a variable the policy does not have constrains nothing, so a check against it passes trivially; a property table counts such a row in structural_no_ops and fails it (chapter 11).

The limits

• UNSAT proves the one obligation asked, under its pins. It is not a statement about the policy as a whole, and it is not a statement that the contexts are set truthfully at run time.
• SAT is a combination the policy admits, not one your systems produce. Check it against what can really happen.
• STALL on the guardrail side is acted on as a bypass; on the random forest side it concludes nothing.
• A void verdict, or a refusal over unread lines, is no verdict, whatever the status field of an earlier run said.