ExMaude

Elixir bindings for the Maude formal verification system

Installation | Quick Start | Documentation

---

Overview

ExMaude provides a high-level Elixir API for interacting with Maude, a formal specification language based on rewriting logic. Use ExMaude for:

• Term Reduction - Simplify expressions using equational logic
• State Space Search - Explore reachable states in system models
• Formal Verification - Verify properties of concurrent and distributed systems
• IoT Rule Conflict Detection - Detect conflicts in physical-IoT automation rules
• AI Rule Conflict Detection - Verify multi-tenant agent policies, capability grants, sovereignty, authority levels, and approval gates

---

Features

Feature	Description
Port-based IPC	Efficient communication via Erlang Ports
Worker Pool	Concurrent operations via Poolboy
High-level API	reduce/3, rewrite/3, search/4, load_file/1
Output Parsing	Structured parsing of Maude results
Telemetry	Built-in observability events
IoT Module	Formal conflict detection for physical-IoT automation rules
AI Module	Formal conflict detection for AI agent policies (capability, sovereignty, authority, approval)

---

Installation

Requirements

• Elixir ~> 1.17
• Erlang/OTP 27+

Add ex_maude to your dependencies in mix.exs:

def deps do
  [
    {:ex_maude, "~> 0.3.0"}
  ]
end

Then install the Maude binary (the hex package ships only MIT-licensed Elixir/Rust/C sources — Maude itself is GPL-licensed and installed separately):

mix deps.get
mix maude.install

Already have Maude on your system? Skip the install task and either keep it on your PATH or point the library at it:

config :ex_maude, maude_path: "/usr/local/bin/maude"

---

Quick Start

# In your application supervision tree:
children = [
  ExMaude.Pool.child_spec(pool_size: 4)
]

# Reduce a term to normal form
{:ok, "6"} = ExMaude.reduce("NAT", "1 + 2 + 3")

# Search state space
{:ok, solutions} = ExMaude.search("MY-MODULE", "initial", "goal", max_depth: 10)

# Load a custom module
:ok = ExMaude.load_file("/path/to/my-module.maude")

---

Configuration

config :ex_maude,
  backend: :port,                      # :port | :cnode | :nif
  maude_path: nil,                     # config/env/installed binary/PATH resolution
  pool_size: 4,                        # Number of worker processes
  pool_max_overflow: 2,                # Extra workers under load
  timeout: 5_000,                      # Default command timeout (ms)
  use_pty: false                       # PTY wrapper opt-in (Port backend only)

Configuration Options

Option	Type	Default	Description
backend	atom()	:port	Communication backend (:port, :cnode, :nif)
maude_path	String.t()	nil	Path to Maude; otherwise use MAUDE_PATH, an installed local binary, or PATH
pool_size	integer()	4	Number of Maude worker processes
pool_max_overflow	integer()	2	Extra workers allowed under load
timeout	integer()	5000	Default command timeout in ms
use_pty	boolean()	false	Wrap Maude in a PTY instead of pipes with -interactive

ExMaude is a library application: it starts no processes automatically. Add ExMaude.Pool.child_spec/1 wherever the pool belongs in your supervision tree. Pass :name when you need multiple independent pools, then select one with the :pool option accepted by ExMaude.Pool operations and ExMaude.execute/2.

By default the Port backend talks to maude -interactive over plain pipes — the same mode the C-Node and NIF backends use, and it needs no extra tooling. Set use_pty: true to wrap Maude in a PTY (script/unbuffer) instead.

Backend Selection

The Hex package does not contain Maude. Install it with mix maude.install, provide MAUDE_PATH, or keep maude on PATH.

# Check available backends
ExMaude.Backend.available_backends()
#=> [:port]  # plus :cnode if maude_bridge is compiled, :nif if the precompiled NIF loaded

# Configure before the pool starts
config :ex_maude, backend: :cnode

Changing :backend does not replace workers already running in the pool. Restart the ExMaude supervision tree after changing it.

---

API Reference

Term Operations

# Reduce using equations (deterministic)
ExMaude.reduce(module, term, opts \\ [])

# Rewrite using rules and equations
ExMaude.rewrite(module, term, opts \\ [])

# Search state space
ExMaude.search(module, initial, pattern, opts \\ [])

Module Loading

# Load from file
ExMaude.load_file("/path/to/module.maude")

# Load from string
ExMaude.load_module("""
fmod MY-NAT is
  sort MyNat .
  op zero : -> MyNat .
  op s : MyNat -> MyNat .
endfm
""")

Direct Execution

# Execute raw Maude commands
{:ok, output} = ExMaude.execute("show modules .")

# Get Maude version
{:ok, version} = ExMaude.version()

---

IoT Rule Conflict Detection

ExMaude includes a Maude model for four useful IoT conflict categories. Its rule schema is inspired by the categories discussed in the AutoIoT paper, but it is a smaller custom model rather than an implementation of the paper's full system.

rules = [
  %{
    id: "motion-light",
    thing_id: "light-1",
    trigger: {:prop_eq, "motion", true},
    actions: [{:set_prop, "light-1", "state", "on"}],
    priority: 1
  },
  %{
    id: "night-mode",
    thing_id: "light-1",
    trigger: {:prop_gt, "time", 2300},
    actions: [{:set_prop, "light-1", "state", "off"}],
    priority: 1
  }
]

{:ok, conflicts} = ExMaude.IoT.detect_conflicts(rules)

Detected Conflict Types

Type	Description
State Conflict	Same device, incompatible state changes
Environment Conflict	Opposing environmental effects
State Cascading	Rule output triggers conflicting rule
State-Env Cascading	Combined cascading effects

See ExMaude.IoT for the full rule schema, trigger types, and action types.

---

AI Rule Conflict Detection

ExMaude includes a Maude module for checking a defined AI-rule schema over agents, capability grants, tool invocations, sovereignty, authority levels, and approval gates.

rules = [
  %{
    id: "approve-then-dose",
    agent_id: {"acme", "ph-controller"},
    trigger: {:prop_lt, "ph", {:int, 6}},
    invocations: [
      {:require_approval, "dosing_high_delta"},
      {:invoke_tool, "dose", %{"ml" => 50}, "high_impact", :eu}
    ],
    capability_grants: [{:cap, "ph_dosing", "v1"}],
    authority_required: 2,
    priority: 1
  },
  %{
    id: "auto-dose",
    agent_id: {"acme", "ph-controller"},
    trigger: {:prop_lt, "ph", {:int, 5}},
    invocations: [
      {:invoke_tool, "dose", %{"ml" => 100}, "high_impact", :eu}
    ],
    priority: 1
  }
]

{:ok, conflicts} = ExMaude.AI.detect_conflicts(rules, jurisdictions: [:eu, :ch])
# => [%{type: :approval_gate_bypass, rule1: "auto-dose", rule2: nil, ...}]

Detected Conflict Types

Type	Detection	Description
Tool Call Conflict	pairwise	Same agent, same tool, conflicting required arguments
Capability Shadowing	pairwise	Two rules grant the same capability at equal priority within a tenant
Pack Tool Composition Mismatch	pairwise	Same capability name, mismatched type-shape signatures
Authority Escalation	pairwise	Rule grants a capability another rule requires at higher authority
Agent Loop Cascade	pairwise	One rule's capability grants another rule's required capability
Sovereignty Violation	single-rule	Tool invocation routes through a forbidden jurisdiction
Approval Gate Bypass	single-rule	High-impact invocation reachable without an approval gate

When to choose AI rules over IoT rules

Use ExMaude.IoT for Things, Properties, and Actions in a single deployment (one building, one factory, one farm). Use ExMaude.AI for Agents with capability ontologies, tool-invocation arguments, tenant scoping, sovereignty, authority levels, or approval gates. Both can coexist — the templates and APIs are independent.

Unsupported predicates

:contains and :matches are not implemented by ai-rules.maude. The validator rejects them explicitly. Evaluate string or regex predicates in the component that owns their matching semantics.

See ExMaude.AI for the full rule schema, predicate vocabulary, and invocation types.

---

Telemetry

ExMaude emits telemetry events compatible with Prometheus, OpenTelemetry, and other exporters. All measurements use native time units for precision.

Events

Event	Description
[:ex_maude, :command, :start]	Command execution started
[:ex_maude, :command, :stop]	Command execution completed
[:ex_maude, :command, :exception]	Command raised an exception
[:ex_maude, :pool, :checkout, :start]	Pool checkout started
[:ex_maude, :pool, :checkout, :stop]	Pool checkout completed
[:ex_maude, :iot, :detect_conflicts, :start]	IoT conflict detection started
[:ex_maude, :iot, :detect_conflicts, :stop]	IoT conflict detection completed
[:ex_maude, :ai, :detect_conflicts, :start]	AI conflict detection started
[:ex_maude, :ai, :detect_conflicts, :stop]	AI conflict detection completed

Measurements

• duration - Time in native units (convert with System.convert_time_unit/3)
• system_time - Wall clock time when event started
• rule_count - Number of rules (IoT and AI events)
• conflict_count - Conflicts detected (IoT and AI events)

Metadata

• operation - Command type (:reduce, :rewrite, :search, :execute, :parse)
• module - Maude module name
• result - :ok or :error
• template - Conflict-detection template in use (:iot_rules or :ai_rules)

Example: Prometheus Metrics

# In your application's telemetry module
defp metrics do
  [
    counter("ex_maude.command.stop.count", tags: [:operation, :result]),
    distribution("ex_maude.command.stop.duration",
      unit: {:native, :millisecond},
      tags: [:operation, :result]
    ),
    last_value("ex_maude.iot.detect_conflicts.stop.conflict_count")
  ]
end

Example: Custom Handler

:telemetry.attach(
  "my-logger",
  [:ex_maude, :command, :stop],
  fn _, %{duration: d}, %{operation: op, result: r}, _ ->
    ms = System.convert_time_unit(d, :native, :millisecond)
    Logger.info("ExMaude #{op}: #{r} in #{ms}ms")
  end,
  nil
)

For complete event documentation, see ExMaude.Telemetry.

---

Architecture

ExMaude uses a pluggable backend architecture, allowing different communication strategies:

                        ExMaude (Public API)
                              │
                    ExMaude.Backend (Behaviour)
                              │
        ┌─────────────────────┼─────────────────────┐
        │                     │                     │
        ▼                     ▼                     ▼
ExMaude.Backend.Port   ExMaude.Backend.CNode   ExMaude.Backend.NIF
        │                     │                     │
        ▼                     ▼                     ▼
  Pipes + Maude CLI   Erlang Distribution    Rust-managed Maude
                      + maude_bridge         subprocess via Rustler

All three backends run Maude as a separate OS process — a Maude crash never takes down the BEAM. They differ in transport and in how much native code runs inside the BEAM itself:

Backend	Transport	Notes
Port	Erlang Port over pipes	Default; no ExMaude native extension required
C-Node	Erlang distribution to a C bridge	Requires epmd and the compiled bridge
NIF	Rustler NIF driving subprocess pipes	Rust runs in-BEAM; a native crash can crash the VM

Module Overview

ExMaude
    ├── ExMaude.Backend    Backend behaviour and selection
    ├── ExMaude.Binary     Binary lookup and platform detection
    ├── ExMaude.Maude      High-level command builders (reduce, rewrite, search)
    ├── ExMaude.Pool       Poolboy worker pool management
    ├── ExMaude.Server     Dispatches calls to each worker's backend
    ├── ExMaude.Parser     Output parsing utilities
    ├── ExMaude.Telemetry  Telemetry events and helpers
    ├── ExMaude.IoT        IoT rule conflict detection (Things, Properties, Actions)
    └── ExMaude.AI         AI rule conflict detection (Agents, Capabilities, Invocations)

---

Development

mix setup # Setup
mix test  # Run tests
mix check # Run all quality checks
mix docs  # Generate documentation

Running Benchmarks

mix bench              # Parser benchmarks
mix bench.backends     # Benchmark every backend available in this VM
mix bench.backends.all # Start distribution, then benchmark available backends

C-Node Testing:

mix test.cnode # Run C-Node integration tests

Note: C-Node requires:

1. Compiled binary: cd c_src && make
2. The mix bench.backends.all and mix test.cnode aliases automatically handle Erlang distribution

---

Performance

ExMaude includes local benchmarks for parser, pool, and backend behavior.

Benchmark Results

• bench/output/benchmarks.md - Parser and Maude integration benchmarks

Backend performance depends on the Maude model, response size, platform, and concurrency. mix bench.backends starts each available worker before timing and writes a local comparison to bench/output/backend_comparison.md. Start with Port and change backend only when a workload-specific benchmark supports the choice.

Running Benchmarks

See Development section for benchmark commands.

---

Interactive Notebooks

Explore ExMaude interactively with Livebook:

Notebook	Description	Livebook
Quick Start	Basic usage and examples
Advanced Usage	IoT conflicts, custom modules, pooling
AI Rules	AI agent policy conflict detection
Term Rewriting	Rewriting and search deep dive
Benchmarks	Performance metrics

---

Documentation

• GitHub - Documentation and source code
• AGENTS.md - AI agent integration guide

---

References

• Maude System - Official Maude website
• Maude Manual - Complete documentation
• AutoIoT Paper - IoT conflict detection research
• Haskell Maude Bindings - Reference implementation

---

Contributing

Contributions are welcome! Please see CONTRIBUTING.md for guidelines.

---

License

ExMaude is released under the MIT License. See LICENSE for details.