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

Why Maude Instead of Native Erlang?

Maude isn't "better Erlang"; it solves a different problem.

Erlang is excellent for building concurrent, fault-tolerant applications. Maude is special because it treats your system as mathematics: states are terms, behavior is expressed as rewrite rules, and properties can be explored systematically.

For ExMaude's IoT use case, Maude provides:

• Declarative rules - Describe what transitions mean instead of writing control flow
• Equational reasoning - Automatically normalize values using equations, including reasoning modulo properties such as associativity and commutativity
• State-space search - Explore many possible rule applications and execution orders, not merely one execution
• Formal verification - Check reachability, invariants, deadlocks, and potentially model-check temporal properties
• Executable specifications - Run and analyze the same formal model

For AI rules, ExMaude provides a deterministic safety envelope around probabilistic AI behavior. An AI model may propose different actions, while Maude checks each structured rule or action for capability, authority, sovereignty, approval, and cross-rule conflicts. It can explore nondeterministic execution paths—what could happen—without estimating how probable each path is. Probability and model-confidence scoring remain outside the current AI-rule module.

You could implement the conflict detector in native Erlang, but you would also need to implement—and trust—your own term-rewriting engine, canonicalization rules, nondeterministic search, cycle detection, and possibly a model checker. That becomes a substantial verification project by itself.

Maude's biggest advantage is when the question is:

Can this happen under any valid sequence of rule applications?

Native Erlang is generally preferable when the question is simply:

Please execute this known application workflow efficiently.

There are costs: an external process, serialization and parsing overhead, another language to maintain, and a less familiar ecosystem. Maude earns its place where formal reasoning and nondeterministic exploration are central; ordinary application behavior should remain in Elixir/Erlang.

Features

Installation

Requirements

• Elixir ~> 1.17
• Erlang/OTP 27+

Add ex_maude to your dependencies in mix.exs:

def deps do
  [
    {:ex_maude, "~> 0.4.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

The installer verifies the SHA-256 digest published by GitHub and fails closed when a release asset has no valid digest. Official stable installers are available for macOS arm64/x64 and Linux x64. On Linux arm64, configure a system-provided Maude executable instead.

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)
  max_response_bytes: 16_777_216,      # Per-command output ceiling (16 MiB)
  use_pty: false,                      # PTY wrapper opt-in (Port backend only)
  preload_modules: [],                 # Modules loaded when workers start
  telemetry_include_commands: false   # Keep command text out of telemetry

Configuration Options

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 the high-level API. Runtime module preloads are tracked independently for each named pool.

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 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 or reload from a file immediately on every worker
ExMaude.load_file("/path/to/module.maude", pool: :verification_pool)

# Idempotent loading for paths reached concurrently at runtime
ExMaude.ensure_file_loaded("/path/to/module.maude", pool: :verification_pool)

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

Use preload_modules for modules known when the pool starts. For dynamic paths, ensure_file_loaded/2 serializes the first pool-wide load and remembers the loaded content for replacement workers; load_file/2 deliberately broadcasts every call and is appropriate when an explicit reload is required.

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

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

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

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)
• command_bytes - UTF-8 byte size of a backend command

Metadata

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

Raw command text is absent by default because Maude terms may contain credentials or policy data. Set telemetry_include_commands: true only after reviewing that risk; opted-in text is truncated to 100 characters.

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:

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:

The notebooks form a learning path — follow them in order for a gradual introduction to Maude and formal verification:

Notebook	Description	Livebook
Quick Start	First contact: reduce, parse, modules, error handling
Term Rewriting	Equations vs rules, search, and your first verification
Advanced Usage	IoT rule-conflict detection, custom modules, pooling, telemetry
AI Rules	Conflict detection for AI agent policies
Benchmarks	Latency, concurrency, and how verification cost scales

Documentation

• GitHub - Documentation and source code
• Usage Rules - Integration and operational patterns

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.