ExMaude AI Rule Conflict Detection

Mix.install(
  [
    {:ex_maude, path: Path.join(__DIR__, ".."), env: :dev}
  ],
  config_path: :ex_maude,
  lockfile: :ex_maude,
  config: [
    ex_maude: [start_pool: true, use_pty: false]
  ]
)

Introduction

ExMaude.AI is the companion to ExMaude.IoT for verifying AI-generated automation rules over Agents, Capabilities, and ToolInvocations.

Where ExMaude.IoT models physical-IoT rules (Things, Properties, Actions), ExMaude.AI adds:

• Capability ontology — typed, shape-versioned capability grants
• Tool invocations — structured tool calls with argument maps
• Tenant scoping — {tenant_id, agent_name} identifiers
• Sovereignty — jurisdiction-bound invocations
• Authority levels — required-vs-granted authority tracking
• Approval gates — explicit gates before high-impact actions
• Budget intervals — symbolic arithmetic over budget envelopes

Both modules target the same Maude verification core. They can ship in the same application — the templates and APIs are independent.

Rule Vocabulary

Predicates (triggers)

# Property-style (carry-over from IoT rules)
{:prop_eq, "key", value}
{:prop_gt, "key", value}
{:prop_lt, "key", value}
{:prop_gte, "key", value}
{:prop_lte, "key", value}

# Capability ontology
{:capability_required, "name"}
{:capability_granted, "name"}

# Quantitative (interval-based, sound symbolic reasoning)
{:budget_within, "scope", {:interval, 0, 50_000}}

# Authority levels
{:authority_at_least, 2}
{:authority_required, 5}

# Sovereignty
{:jurisdiction_allowed, :eu}
{:jurisdiction_forbidden, :us}

# Latency budgets
{:latency_at_most, 2_000}

# Logical operators
{:always}
{:and, p1, p2}
{:or, p1, p2}
{:not, p}

Tool invocations

# Direct tool invocation
{:invoke_tool, "tool_name", %{"arg" => value}, "capability_required", :eu}

# Approval gate — must precede high_impact invocations
{:require_approval, "approval_class"}

Example 1: Sovereignty Violation

A US-routing search tool runs under a tenant that allows only EU/CH jurisdictions:

rules = [
  %{
    id: "us-search",
    agent_id: {"acme", "research-agent"},
    trigger: {:always},
    invocations: [
      {:invoke_tool, "search", %{"q" => "x"}, "internet_access", :us}
    ]
  }
]

ExMaude.AI.detect_conflicts(rules, jurisdictions: [:eu, :ch])

Expect a :sovereignty_violation conflict — the tool routes through a jurisdiction outside the tenant's allowed set.

Example 2: Approval Gate Bypass

A high-impact dosing invocation must be preceded by an approval gate:

# Without an approval gate — bypass is detected
without_approval = [
  %{
    id: "auto-dose",
    agent_id: {"acme", "ph-controller"},
    trigger: {:always},
    invocations: [
      {:invoke_tool, "dose", %{"ml" => 100}, "high_impact", :eu}
    ]
  }
]

ExMaude.AI.detect_conflicts(without_approval, jurisdictions: [:eu])

# Add the gate — bypass clears
with_approval = [
  %{
    id: "approve-then-dose",
    agent_id: {"acme", "ph-controller"},
    trigger: {:always},
    invocations: [
      {:require_approval, "dosing_high_delta"},
      {:invoke_tool, "dose", %{"ml" => 100}, "high_impact", :eu}
    ]
  }
]

ExMaude.AI.detect_conflicts(with_approval, jurisdictions: [:eu])

Example 3: Capability Shadowing

Two rules grant the same capability at equal priority within a tenant — the verifier flags this as :capability_shadowing (ambiguous activation):

rules = [
  %{
    id: "grant-search-a",
    agent_id: {"acme", "agent-a"},
    trigger: {:always},
    invocations: [],
    capability_grants: [{:cap, "web_search", "v1"}],
    priority: 1
  },
  %{
    id: "grant-search-b",
    agent_id: {"acme", "agent-b"},
    trigger: {:always},
    invocations: [],
    capability_grants: [{:cap, "web_search", "v1"}],
    priority: 1
  }
]

ExMaude.AI.detect_conflicts(rules)

Example 4: Pack Tool Composition Mismatch

The same capability name with mismatched shape signatures — typically two different versions of the same tool — is flagged as :pack_tool_composition_mismatch:

rules = [
  %{
    id: "grant-search-v1",
    agent_id: {"acme", "agent-a"},
    trigger: {:always},
    invocations: [],
    capability_grants: [{:cap, "web_search", "v1"}],
    priority: 1
  },
  %{
    id: "grant-search-v2",
    agent_id: {"acme", "agent-b"},
    trigger: {:always},
    invocations: [],
    capability_grants: [{:cap, "web_search", "v2"}],
    priority: 1
  }
]

ExMaude.AI.detect_conflicts(rules)

Validation Without Maude

validate_rule/1 and validate_rules/1 catch shape errors before any Maude round trip. Useful for fast feedback in editors or CI:

ExMaude.AI.validate_rule(%{
  id: "ok",
  agent_id: {"acme", "ag1"},
  trigger: {:always},
  invocations: []
})

ExMaude.AI.validate_rule(%{id: "broken"})

The validator also surfaces a contract for unverifiable predicates that the equational fragment of Maude cannot decide:

# Regex / string-search predicates are explicitly unverifiable
ExMaude.AI.Validator.validate_predicate({:contains, "subject", "needle"})

ExMaude.AI.Validator.validate_predicate({:matches, "subject", ~r/x/})

Route these to a separate string-match safety net (sandbox, regex matcher, LLM-as-judge) rather than trying to encode them into the Maude template.

Conflict-Type Cheatsheet

ExMaude.AI.ConflictParser

detect_pair_conflicts/2 runs only the pairwise checks; detect_single_rule_conflicts/2 runs only the single-rule checks; detect_conflicts/2 runs both.

Telemetry

ExMaude.AI.detect_conflicts/2 emits the same telemetry envelope as ExMaude.IoT.detect_conflicts/2, with metadata.template == :ai_rules so handlers can route on template:

:telemetry.attach(
  "ai-rules-logger",
  [:ex_maude, :ai, :detect_conflicts, :stop],
  fn _, %{duration: d, conflict_count: n}, %{result: r}, _ ->
    ms = System.convert_time_unit(d, :native, :millisecond)
    IO.puts("ai-rules: #{r}, #{n} conflicts in #{ms}ms")
  end,
  nil
)

ExMaude.AI.detect_conflicts(
  [
    %{
      id: "demo",
      agent_id: {"acme", "ag1"},
      trigger: {:always},
      invocations: []
    }
  ],
  jurisdictions: [:eu]
)

:telemetry.detach("ai-rules-logger")

Next Steps

• Quick Start - Basic Maude operations
• Advanced Usage - IoT conflict detection, custom modules, pooling
• Term Rewriting - Rewriting and search deep dive