Skip to content

3 · Concepts

This chapter defines the words the rest of the guide uses for verification, one paragraph each. After this chapter each word means exactly what it says here, and a page that uses one links back.

Policy

A policy is the file of rules a guardrail runs: which actions a conversation may reach, and under what conditions. Verification reads policies written in Colang 1.0, the language of NeMo Guardrails, and a declared subset of Colang 2.x. A rule sheet is the same kind of rules written as YAML (chapter 41), compiled into the same form before anything reads it.

Rulebook

A rulebook is a policy as an agent runs under it: the rules every tool call is checked against. An agent's rulebook: is a Colang file or a rule sheet, and the service compiles it into the record the tool check enforces (chapter 45).

Action

An action is something a policy lets a conversation make happen: a bot message, or a tool call such as execute_transfer_funds. Verification asks about one action at a time.

Context

A context is a fact about the conversation a policy consults before it acts, written as a variable: $is_authenticated, $supervisor_approved. The policy reads it; something outside the policy, such as your systems of record, sets it. Verification treats every context as free to take either value, which is what lets one answer cover every situation at once.

Obligation

An obligation is the question verification answers: can this action fire while this context is false? It is a pair, an action and the context it must never fire without, such as execute_transfer_funds and is_authenticated. A run decides one obligation, and nothing else (chapter 4).

Pin

A pin fixes a variable to 0 or 1 for the question, so the obligation is asked only in the situations it is about. A high-risk answer must carry a risk warning, for this kind of product is the obligation respond with high risk answer / risk_warning_given, with the pin product_is_nmmi=1. A conditional obligation asked without its pin asks about situations the rule never covered, and the answer means nothing (chapter 4).

Verdict

A verdict is the answer, and it is one of three:

  • UNSAT: no situation makes the action fire with the context false. The obligation holds, over every combination of inputs at once.
  • SAT: a situation exists, and the verdict names it. The obligation is broken.
  • STALL: the run could not decide. On the guardrail side it is acted on as SAT; on the random forest side it concludes nothing.

What each one does not mean is in chapter 6.

Certificate

A certificate is a JSON document that records why the equations of a question have no solution, step by step, so that anyone can check it without our software. It comes with an UNSAT verdict where the profile builds one (chapter 7).

Patch

A patch is the repair the engine proposes for a broken or undecided obligation: one condition, written in the policy's own names, added to every flow that reaches the action. It comes with a proof that the repaired policy rules the outcome out (chapter 8).

Profile

A profile is a named setting of the engine, chosen per request. It decides which phases run and, therefore, what the answer is allowed to claim: fast decides in about a quarter of a second and builds no certificate; patch builds a repair and a certificate; proof, enumerate and forest serve the purposes their names give (chapter 10).

Budget

A budget is the time a run may spend: one on the whole solve, and one on the search for a repair. A run that exhausts its budget says so, and what it still returns is said in chapter 10.

Diagnostics

Diagnostics are what the compiler says about a policy it could not fully read: a line it skipped, a construct it does not handle. A verdict over a policy with parse diagnostics in the question's reach is void (chapter 6).

Job, mode and operands

Every verification is a job: a request to POST /v1/solves naming a mode (guardrail, batch, graph, hunt, forest and the rest), its input files and its operands, the fields that are not files, such as the action and the context. A job runs on our servers and is read, streamed or cancelled by its id (chapter 9). The modes are listed in the generated reference.