4 · Asking the right question

A verification answers exactly the question it is asked. This chapter is about asking the one you mean: an obligation stated as a pair, the pins that scope it, how to find the candidates in a policy you did not write, and why one run settles one proposition and no more.

An obligation is a pair

Verification does not check a policy. It checks a proposition about one:

Can this action fire while this context is false?

You name both. For a transfer service the obligation might be the action execute_transfer_funds and the context is_authenticated, and the question is whether any conversation, in any situation, makes a transfer happen for a user who is not signed in. A guardrail job carries the pair as its two required operands:

result = client.verify_guardrail("transfers.co", "execute_transfer_funds", "is_authenticated")
print(result.status, result.decided_by)

The answer quantifies over every situation at once. A policy with 48 contexts has 2⁴⁸ combinations of them, and an UNSAT settles all of them, which is what no number of test conversations can do.

Asking about one rail

A context can be qualified by where the policy consults it: risk_warning_given@output. The phase is input, output or dialog. The unqualified context asks whether the obligation is met anywhere, which is the weaker question; a check placed at the wrong end of the pipeline is not the control it resembles. Where the policy never consults the variable on the rail you name, the question is refused rather than answered, and the refusal names the rails the variable is consulted on.

The pins say when the obligation applies

Most rules are conditional. A high-risk investment answer must carry a risk warning applies to one kind of product; an investment recommendation needs the advising permission applies when a recommendation is personal. Asked without its condition, the question covers situations the rule never meant to govern, and its answer is about the wrong thing:

• too few pins and a policy that is correct can come back STALL or SAT over situations the rule does not cover. Acting on that answer patches a policy that was right, which is the one case where a repair makes the product worse;
• too many pins and the question is narrower than the rule: a clean answer then says less than it appears to.

A pin fixes one variable to 0 or 1 for the question. Name the conditions the rule names, no more and no fewer:

result = client.verify_guardrail(
    "gemini.co",
    "respond with permitted investment answer",
    "has_advising_permission",
    pins={"personal_recommendation": 1},  # the rule applies to a personal recommendation
    profile="patch",                      # and asks for a repair if it does not hold
)
print(result.status)
print(result.corrective_action["guardrail_patch"])

Pins come from the rule you are enforcing, not from the policy, and they are the part of the question a reviewer must read. Chapter 12 shows how to have the engine compute the weakest pins under which an obligation holds, which turns writing the pins into checking them.

Finding the questions

The question the engine cannot answer for you is what counts as an unwanted outcome: that is a judgement about your business and its rules. The question it can answer is which of them the policy already encodes as a guard. The enumerate_properties mode reads the policy, walks back from each action to every context that can influence it, and proposes each pair as a candidate. It runs no solve, so it costs less than one verification:

proposed = client.enumerate_properties("transfers.co")
for row in proposed.records:
    print(row["action"], row["context"], row["guarded"], row["derived_pins"])

Each candidate row carries what the policy already says about the pair:

• guarded: true and derived_pins: [{}]: the policy requires the context before the action under no further condition. The strongest form.
• derived_pins listing conditions, such as [{"product_is_nmmi": 1}]: the policy requires the context under those conditions. Two entries are two separate conditions, and each is a row of its own if you keep it.
• derived_pins: [], an empty list: the variable is on a route to the action, but never as something the action requires. That is a prohibition, not an obligation, and asking whether the action can fire without it asks the question the wrong way round.
• guarded: false: the action depends on the context and no branch of the policy mentions it. This is what an omission looks like from inside, and it is the row to read first.

reads_as spells each row out in words, and guard_paths names the flows and lines that guard it.

A candidate has no id, no expect and no gate: an enumeration is a proposal. Promoting a row into the table you commit is a person's decision, and the step that matters is setting expect to what the obligation should return, not to what it returns today. A row written to match today's behaviour cannot fail, and a table of rows that cannot fail proves nothing (chapter 11).

What enumeration cannot find

An obligation the rule requires and the policy never mentions has no variable, reaches no action and is absent from the list. That is the bypass by omission, and no reading of the policy can find it. The enumeration says so in its own output (enumeration.covers): a clean sweep over its rows proves the policy enforces what it claims, not that it claims enough.

One run proves one proposition

Proving that a high-risk answer cannot be given without a risk warning says nothing about whether it can be given without a compensation-scheme warning, or about any other action in the file. A policy with twelve unwanted outcomes is twelve questions. Run them as a committed table, so that a change to the policy re-asks all of them (chapter 11), and keep the table beside the policy, where whoever signs the rules off can read it.

The limits

• An answer is about the question asked: the action, the context and the pins. It is not about the policy as a whole.
• The list of questions is yours. The engine proposes the obligations a policy encodes; it cannot propose one the policy omits.
• Pins state the scope of an obligation, and a wrong pin gives a correct answer to the wrong question. Nothing inside the engine can tell you which pins your rule meant.