Skip to main content
Glama
OrygnsCode

opa-mcp-server

by OrygnsCode
OverviewSchemaSourceRelated ServersDiscussionsAdmin
TypeScript
Local

Formally verify a Rego policy rule

rego_verify
Read-onlyIdempotent

Formally verify a Rego rule's property with SMT solving, checking all inputs and returning counterexamples.

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

TableJSON Schema
NameRequiredDescriptionDefault
kindYesProperty 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)
ruleYesName of the rule to verify (e.g. "allow", "deny").
sourceYesRego source to verify.
v0CompatibleNoRead the policy as Rego v0 (`--v0-compatible`), the syntax OPA used before 1.0: rules without `if`, partial sets as `deny[msg] { ... }`. Needed for a policy that has not been migrated, which OPA 1.x otherwise refuses to load. Where the tool also takes a query, the query is read as v0 too, with the future keywords imported so `in`, `every` and `some x in` still work in it.

Schema Changelog

Changes observed during successful MCP inspections.

  1. Changed1 schema field changedv0.8.0
    • addedInput schema / properties / v0Compatible
      Added value: +{
+  "description": "Read the policy as Rego v0 (`--v0-compatible`), the syntax OPA used before 1.0: rules without `if`, partial sets as `deny[msg] { ... }`. Needed for a policy that has not been migrated, which OPA 1.x otherwise refuses to load. Where the tool also takes a query, the query is read as v0 too, with the future keywords imported so `in`, `every` and `some x in` still work in it.",
+  "type": "boolean"
+}
  2. Addedv0.1.13

TDQS

A4.5/5.0
Behavior5/5

Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?

Goes well beyond the read-only/idempotent annotations by disclosing supported patterns, INCONCLUSIVE conditions (negation-as-failure, comprehensions, partial rules, functions, else chains, unencodable operands), and the subtle undefined-vs-true empty-input semantics with a concrete counterexample. This is exactly the behavioral context an agent needs to interpret results.

Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.

Conciseness5/5

Is the description appropriately sized, front-loaded, and free of redundancy?

Front-loaded with the core capability, then dense but purposeful detail; every sentence adds verification-relevant information rather than restating the name. No filler.

Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.

Completeness5/5

Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?

With no output schema, the description carries the burden of return semantics and does so completely: prove-vs-counterexample behavior, INCONCLUSIVE cases, and the empty-input edge case are all covered.

Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.

Parameters3/5

Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?

Schema description coverage is 100%, so kind, rule, source, and v0Compatible are already fully documented in the schema, making the baseline 3 appropriate. The description adds interpretive context (e.g. undefined fields and the {} counterexample) but no syntax or format detail beyond the schema.

Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.

Purpose5/5

Does the description clearly state what the tool does and how it differs from similar tools?

States a specific verb and resource ('Formally verify a property about a Rego rule using SMT solving') and immediately anchors the mechanism (Microsoft Z3). It explicitly distinguishes itself from testing and other evaluation siblings by noting it checks ALL possible inputs and returns a counterexample.

Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.

Usage Guidelines4/5

Does the description explain when to use this tool, when not to, or what alternatives exist?

Gives clear usage context via contrast ('Unlike testing, this checks ALL possible inputs'), which selects it over rego_test/rego_eval, and enumerates when it returns INCONCLUSIVE. It does not name a specific alternative sibling tool, so routing is by implication rather than explicit reference.

Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.

Deploy Server

Other Tools