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 powerful 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

Installation

Requirements

• Elixir ~> 1.17
• Erlang/OTP 26+

Add ex_maude to your dependencies in mix.exs:

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

Then install the Maude binary:

mix deps.get
mix maude.install

Quick Start

# Start the worker pool
{:ok, _} = ExMaude.Pool.start_link()

# 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,                     # nil = auto-detect bundled binary
  pool_size: 4,                        # Number of worker processes
  pool_max_overflow: 2,                # Extra workers under load
  timeout: 5_000,                      # Default command timeout (ms)
  start_pool: false,                   # Auto-start pool on application start
  use_pty: true                        # Use PTY wrapper (Port backend only)

Configuration Options

Set use_pty: false if you encounter script: openpty: Device not configured errors (common in Docker/CI environments).

Backend Selection

ExMaude bundles Maude binaries for common platforms. No installation step needed for most users.

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

# Switch backend at runtime (for testing)
Application.put_env(:ex_maude, :backend, :cnode)

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 module implementing formal conflict detection for IoT automation rules, based on the AutoIoT paper.

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

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

AI Rule Conflict Detection

ExMaude includes a Maude module for verifying AI-generated automation rules over Agents, Capabilities, ToolInvocations, and richer predicates (capability ontology, budget intervals, sovereignty, authority levels, approval gates). Use it to catch unsafe agent policies before they ship.

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

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.

Unverifiable predicates

:contains and :matches (regex / string search) are not decidable in Maude's equational fragment. The validator returns {:error, "...unverifiable..."} for these — route them to a separate string-match safety net (sandbox, regex matcher, LLM-as-judge) rather than encoding them into the Maude template.

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

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
        │                     │                     │
        ▼                     ▼                     ▼
   PTY + Maude CLI    Erlang Distribution    Direct libmaude
                      + maude_bridge          via Rustler

Module Overview

ExMaude
    ├── ExMaude.Backend    Backend behaviour and selection
    ├── ExMaude.Binary     Binary lookup, platform detection, bundled binaries
    ├── ExMaude.Maude      High-level command builders (reduce, rewrite, search)
    ├── ExMaude.Pool       Poolboy worker pool management
    ├── ExMaude.Server     Per-worker GenServer wrapping a backend session
    ├── 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     # Backend benchmarks (Port backend only)
mix bench.backends.all # Backend benchmarks (All backends: Port + C-Node)

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 comprehensive benchmarks to help you understand performance characteristics and choose the right backend for your workload.

Benchmark Results

• bench/output/benchmarks.md - Parser and Maude integration benchmarks
• bench/output/backend_comparison.md - Port vs C-Node backend comparison

Key Takeaways

Latency figures are reduce in NAT : 1 + 1 on Apple Silicon (M-series), averaged over 200 warm iterations. Run the benchmarks locally for your hardware.

Recommendation: Start with Port backend, switch to C-Node if benchmarks show communication overhead is a bottleneck.

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.