ExMaude AI Rule Conflict Detection

app_root = Path.expand("..", __DIR__)

if File.exists?(Path.join(app_root, "mix.exs")) do
  # Running from a clone of the repository: use the local checkout,
  # which bundles the Maude interpreter under priv/.
  Mix.install(
    [{:ex_maude, path: app_root, env: :dev}],
    config_path: :ex_maude,
    lockfile: :ex_maude,
    config: [ex_maude: [use_pty: false]]
  )
else
  # Running standalone (e.g. via the "Run in Livebook" badge): use the
  # released package. This needs a `maude` binary on your PATH, or the
  # MAUDE_PATH env var set — see https://github.com/futhr/ex_maude#installation
  Mix.install(
    [{:ex_maude, "~> 0.4"}],
    config: [ex_maude: [use_pty: false]]
  )
end

{:ok, _pool_supervisor} =
  Supervisor.start_link([ExMaude.Pool.child_spec()], strategy: :one_for_one)

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 and follow the same detect → fix → prove clean workflow shown in the Advanced Usage notebook — read that first if you haven't. They can ship in the same application; the templates and APIs are independent.

Rule Vocabulary

The blocks in this section are reference material, not runnable cells — they show the shapes the rule maps are built from.

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 encoding)
{: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 rejects predicates that the current Maude model does not encode:

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

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

Evaluate these with application code or a dedicated regular-expression engine before passing rules to ExMaude.

Conflict-Type Cheatsheet

The full set of conflict types (parsed by 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