Formally verify a Rego policy rule
rego_verifyFormally proves whether a Rego rule is always true, never true, or satisfiable; uses SMT solving to check all inputs and returns a counterexample when the property fails.
Instructions
Formally verify a property about a Rego rule using SMT solving (Microsoft Z3). Unlike testing, this checks ALL possible inputs and either proves the property holds or returns a concrete counterexample input that falsifies it. Supports equality, comparison, startswith, endswith, contains, and simple regex.match patterns (prefix: ^lit.*, suffix: .lit$, exact: ^lit$, contains: .lit., wildcard: .). Complex regex patterns (character classes, quantifiers, alternation) return INCONCLUSIVE. Also reports INCONCLUSIVE for negation-as-failure (not), comprehensions, partial set and object rules (deny contains msg), functions, else chains, and any operand it cannot encode. A body that reads an absent field is undefined rather than true, so always_true holds only if the rule is also true for an empty input: a rule requiring input.x will be answered with the counterexample {}.
Input Schema
| Name | Required | Description | Default |
|---|---|---|---|
| kind | Yes | Property to prove: always_true - rule is true for every possible input (finds inputs that violate this) never_true - rule is never true for any input (finds inputs that trigger it) satisfiable - at least one input exists where rule is true (returns a witness) | |
| rule | Yes | Name of the rule to verify (e.g. "allow", "deny"). | |
| source | Yes | Rego source to verify. |