Formally verify a Rego policy rule
rego_verifyFormally verify properties of Rego rules (always_true, never_true, satisfiable) by checking all possible inputs using SMT solving. Returns counterexamples if property fails, or proves it holds.
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, and other unsupported constructs.
Input Schema
| Name | Required | Description | Default |
|---|---|---|---|
| source | Yes | Rego source to verify. | |
| rule | Yes | Name of the rule to verify (e.g. "allow", "deny"). | |
| 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) |